[Question] Introduce a minimal potential-response core

[bocowgill]

Motivation

Introduce a deliberately small potential-outcomes foundation for shared use in results about randomized experiments, observational studies, instrumental variables, regression discontinuity, principal stratification, mediation, longitudinal treatment, and related designs.

Proposed declarations

Add one generic representation of potential responses:

abbrev PotentialResponse
    (Intervention : Type*) (Unit : Type*) (Value : Type*) :=
  Intervention → Unit → Value

Here Intervention is deliberately arbitrary. It may be a treatment value, complete allocation vector, instrument–treatment pair, treatment history, or policy. Unit may represent a finite-population unit or a superpopulation state.

Add two pointwise operations:

namespace PotentialResponse

variable {Intervention : Type*} {Unit : Type*} {Value : Type*}
  {Index : Type*} {Source : Type*}

def select
    (response : PotentialResponse Intervention Unit Value)
    (intervention : Unit → Intervention) :
    Unit → Value :=
  fun u ↦ response (intervention u) u

select evaluates each unit's response at a supplied intervention. It is only the theoretical map u ↦ response (intervention u) u; it neither introduces a recorded observed-outcome variable nor asserts consistency. If intervention is the realized treatment assignment, identifying this map with a recorded outcome requires a separate consistency assumption such as $Y^{\mathrm{obs}}(u)=response,(intervention,u),u$.

def comp
    (response : PotentialResponse Intervention Unit Value)
    (intervention :
      PotentialResponse Index Unit Intervention) :
    PotentialResponse Index Unit Value :=
  fun index u ↦ response (intervention index u) u

comp performs same-unit substitution, not ordinary function composition. In response.comp intervention index u, the outer response and the substituted intervention response are evaluated using the same unit u. It will later support constructions such as Y(z, D(z)) in IV and Y(a, M(a′)) in mediation.

Add the corresponding application lemmas and the elementary identity and associativity laws for same-unit substitution:

@[simp] theorem select_apply
    (response : PotentialResponse Intervention Unit Value)
    (intervention : Unit → Intervention)
    (u : Unit) :
    response.select intervention u =
      response (intervention u) u := rfl

@[simp] theorem comp_apply
    (response : PotentialResponse Intervention Unit Value)
    (intervention :
      PotentialResponse Index Unit Intervention)
    (index : Index)
    (u : Unit) :
    response.comp intervention index u =
      response (intervention index u) u := rfl

@[simp] theorem comp_id
    (response : PotentialResponse Intervention Unit Value) :
    response.comp (fun intervention _ ↦ intervention) = response := rfl

@[simp] theorem id_comp
    (response : PotentialResponse Intervention Unit Value) :
    comp (fun value _ ↦ value) response = response := rfl

theorem comp_assoc
    (response : PotentialResponse Intervention Unit Value)
    (intervention : PotentialResponse Index Unit Intervention)
    (source : PotentialResponse Source Unit Index) :
    (response.comp intervention).comp source =
      response.comp (intervention.comp source) := rfl

end PotentialResponse

Implementation

Create Statlib/Causal/PotentialResponse.lean containing these declarations and module documentation, and import it from Statlib.lean. The new module must pass the project build and linter.

Scope

No new structure or causal-assumption predicate is needed in this PR. In particular, it will not require measurable-space instances or add probability measures, measurability or integrability predicates, assignment mechanisms, covariates, recorded observed outcomes, consistency, no-interference, ignorability, positivity, exclusion, monotonicity, estimands, identification theorems, estimators, or inference.

Using a full allocation vector as Intervention permits interference; using an individual treatment value is a later specialization. Thus the core does not silently assume SUTVA.

Longitudinal treatments

For a fixed time horizon, the type of complete treatment paths can be used as Intervention. A later dynamic-regime layer may define time-indexed histories and policies mapping available past histories to actions, then recursively construct counterfactual paths under a policy. Adaptivity, nonanticipation, and related conditions belong in that later layer rather than in PotentialResponse.

Relationship to structural and graphical models

This issue defines only the potential-response layer; it does not propose a single foundation subsuming potential outcomes, structural equation models, and causal DAGs. The potential-response core should not depend on a structural or graphical API, and structural or graphical development is not a prerequisite for this PR. Each base API should remain usable without importing an optional bridge.

A node's one-step-ahead counterfactual can later be represented as a potential response indexed by assignments to its parents, with Unit carrying the unit or exogenous state. comp provides the same-unit recursive substitution needed to construct downstream and nested counterfactuals.

Depending on the intended theorem, a future bridge may require independently defined graph and parent structure, structural assignments or stochastic kernels, intervention semantics, exogenous-state or probability structure, and explicit assumptions such as autonomy, Markov conditions, independent errors, or cross-world restrictions. If concrete applications later motivate such translations, separate bridge modules may state the corresponding constructions or theorems. Such bridges are neither part of this PR nor a prerequisite or required stage of the potential-outcomes roadmap.

Textbooks and papers consulted

• Peng Ding, A First Course in Causal Inference
• Guido Imbens and Donald Rubin, Causal Inference for Statistics, Social, and Biomedical Sciences
• Linbo Wang, Thomas Richardson, and James Robins, Causal Inference: A Tale of Three Frameworks, arXiv:2511.21516

Direction for the second PR

Add generic definitions for comparing responses under two interventions and averaging that comparison over a finite target population. The second PR should define unit-level contrasts and finite-population average treatment effects. It should not yet introduce assumptions connecting potential responses to recorded data, identification theorems, estimators, or statistical inference.

Probability-distributed superpopulation estimands should follow in a separate measurable and probabilistic layer. That layer should take measurable structures and probability measures explicitly and keep measurability and integrability conditions separate from PotentialResponse. Its design must distinguish sectionwise from joint measurability. Joint measurability of the response together with measurability of the intervention map gives a natural sufficient condition for select to be measurable; the exact predicate API is deferred.

General roadmap

1. Potential-response representation, selection, and same-unit-substitution laws (this PR).
2. Contrasts and finite-population estimands.
3. Measurability, integrability, and probability-distributed superpopulation estimands.
4. Allocations, assignment mechanisms, recorded outcomes, and consistency.
5. Causal assumptions and identification theorems.
6. Estimators and statistical inference.

Dynamic treatment regimes are a later domain layer. Structural and graphical base APIs may proceed independently; optional bridge modules may be added in response to concrete applications.

[rajarshi-mukherjee24]

1. regarding select, can we update its documentation to distinguish the selected potential response from the recorded observed outcome. Mathematically, one can think of response.select assignment is the function $(u \mapsto Y(assignment(u),u))$. indeed, if assignment is the realized treatment (A), identifying this function with the recorded outcome $(Y^{\mathrm{obs}})$ requires the separate consistency assertion $(Y^{\mathrm{obs}}(u)=Y(A(u),u))$. Could we explicitly say that select neither introduces an observed-outcome variable nor asserts consistency?
2. Could we describe comp explicitly as “same-unit substitution,” rather than ordinary function composition? Its defining feature is $(R \mathbin{\star} S)(j,u)=R(S(j,u),u),$ where the same unit (u) is there for both responses. Can we also add elementary identity and associativity lemmas (e.g. below), since these can provide algebraic validity behind recursive counterfactual constructions:
   $R^{\star} \mathrm{id}=R, \mathrm{id}\star S=S,(R\star S)\star T=R\star(S\star T).$
   These should be very short proofs now, but they will make later IV, mediation, and longitudinal constructions easier to reason about.
3. It makes sense to keep PotentialResponse purely functional in this PR, without requiring measurable spaces or a probability measure. It may nevertheless be useful to mention a future measurability layer in the roadmap. There are two distinct notions:
   (i) Sectionwise measurability: for every fixed intervention $i$, the function response $i : Unit \to Value$ is measurable.
   (ii) Joint measurability: the function$ (i, u) \to response i u$ on $Intervention × Unit$ is measurable.
   The distinction can matter for select. Maybe we can keep the current definition unchanged and later introduce separate predicates such as PotentialResponse.IsSectionMeasurable and PotentialResponse.IsJointlyMeasurable, together with measurability-preservation results for select and comp.
4. Can we provide more details on how to handle dynamic treatment regimes in this framework?
5. I think the roadmap should clarify what additional structure is needed to connect it to structural and graphical identification theory.

[bocowgill]

Thanks, @rajarshi-mukherjee24. These are helpful and largely reinforce the intended separation between the foundational representation and later causal or probabilistic structure.

1. regarding select, can we update its documentation to distinguish the selected potential response from the recorded observed outcome. Mathematically, one can think of response.select assignment is the function $(u \mapsto Y(assignment(u),u))$. indeed, if assignment is the realized treatment (A), identifying this function with the recorded outcome $(Y^{\mathrm{obs}})$ requires the separate consistency assertion $(Y^{\mathrm{obs}}(u)=Y(A(u),u))$. Could we explicitly say that select neither introduces an observed-outcome variable nor asserts consistency?

Yes. The existing documentation intends this distinction, but I will make it explicit: response.select assignment is only the theoretical map

$$ u \mapsto response,(assignment,u),u. $$

It neither introduces a recorded observed-outcome variable nor asserts consistency. Relating it to recorded outcomes requires a separate assumption such as $Y^{\mathrm{obs}}(u)=Y(A(u),u)$.

2. Could we describe comp explicitly as “same-unit substitution,” rather than ordinary function composition? Its defining feature is $(R \mathbin{\star} S)(j,u)=R(S(j,u),u),$ where the same unit (u) is there for both responses. Can we also add elementary identity and associativity lemmas (e.g. below), since these can provide algebraic validity behind recursive counterfactual constructions:
   $R^{\star} \mathrm{id}=R, \mathrm{id}\star S=S,(R\star S)\star T=R\star(S\star T).$
   These should be very short proofs now, but they will make later IV, mediation, and longitudinal constructions easier to reason about.

Yes. “Same-unit substitution” is the intended interpretation of comp, and I will reinforce that wording. I also agree that the two identity laws and associativity are useful and small enough to include in PR1, using the identity response fun i _ ↦ i.

3. It makes sense to keep PotentialResponse purely functional in this PR, without requiring measurable spaces or a probability measure. It may nevertheless be useful to mention a future measurability layer in the roadmap. There are two distinct notions:
   (i) Sectionwise measurability: for every fixed intervention $i$, the function response $i : Unit \to Value$ is measurable.
   (ii) Joint measurability: the function$ (i, u) \to response i u$ on $Intervention × Unit$ is measurable.
   The distinction can matter for select. Maybe we can keep the current definition unchanged and later introduce separate predicates such as PotentialResponse.IsSectionMeasurable and PotentialResponse.IsJointlyMeasurable, together with measurability-preservation results for select and comp.

Agreed on keeping measurable spaces and probability measures out of this PR. I will mention a future measurability layer in the roadmap without committing to its exact API yet. One point that the later design will need to handle carefully is that sectionwise measurability alone generally does not establish measurability of select when the intervention varies by unit; joint measurability of the response together with measurability of the intervention map gives a natural sufficient condition.

4. Can we provide more details on how to handle dynamic treatment regimes in this framework?

For a fixed longitudinal treatment path, the path type can be used directly as Intervention. A later dynamic-regime layer can define histories and policies mapping past histories to actions, then recursively construct the counterfactual path under a policy. Adaptivity, nonanticipation, and related conditions would be separate predicates in that layer rather than fields of PotentialResponse.

5. I think the roadmap should clarify what additional structure is needed to connect it to structural and graphical identification theory.

On structural and graphical models, I want to distinguish compatibility from unification. Issue #40 does not propose a single foundation subsuming potential outcomes, SEMs, and DAGs. Those base APIs should remain independently usable and should not depend on one another. If concrete applications later create demand, separate bridge modules can state explicit translations or correspondence theorems under explicit assumptions. That possibility should neither block this PR nor be treated as a required stage of the potential-outcomes roadmap.

I’ll update #40 along these lines while keeping PR1 limited to the purely functional core, its documentation, and the elementary composition laws. I will then open the small implementation PR unless you see a remaining foundational objection.

[bocowgill]

Thanks again, @rajarshi-mukherjee24. I’ve updated the issue description to incorporate the points in your comment.

[rajarshi-mukherjee24]

@bocowgill This looks good. Just one last minor comment/question: could you let me know what you think is the best option? Specifically, should we define the identity response once, for example, PotentialResponse.id, by id(i,u)=i, rather than writing fun x _ ↦ x separately in comp_id and id_comp? I was wondering if this would let us write the laws more clearly as response.comp id = response and id.comp response = response, and the identity response may be useful later when working with repeated or recursive compositions. If you think this is not a big issue. I will approve and merge.

[bocowgill]

Thanks, @rajarshi-mukherjee24. Agreed—PotentialResponse.id is the better API. I added it to PR #41, together with a simp evaluation lemma, and rewrote the identity laws as response.comp id = response and id.comp response = response. The full local build, lint, and import-generation checks pass. The new GitHub Actions run is awaiting maintainer approval.