From f2884ed1f5fc8064f42a39f1287f48724ecb3d73 Mon Sep 17 00:00:00 2001 From: Bo Cowgill Date: Fri, 28 Aug 2026 16:15:58 -0600 Subject: [PATCH 1/4] Add potential-response core --- Statlib.lean | 1 + Statlib/Causal/PotentialResponse.lean | 65 +++++++++++++++++++++++++++ 2 files changed, 66 insertions(+) create mode 100644 Statlib/Causal/PotentialResponse.lean diff --git a/Statlib.lean b/Statlib.lean index 2f08ecf..707dba3 100644 --- a/Statlib.lean +++ b/Statlib.lean @@ -1,3 +1,4 @@ +import Statlib.Causal.PotentialResponse import Statlib.EValues.DPI import Statlib.EValues.EVariable import Statlib.EValues.Utility.Basic diff --git a/Statlib/Causal/PotentialResponse.lean b/Statlib/Causal/PotentialResponse.lean new file mode 100644 index 0000000..364f63f --- /dev/null +++ b/Statlib/Causal/PotentialResponse.lean @@ -0,0 +1,65 @@ +/- +Copyright (c) 2026 Bo Cowgill. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bo Cowgill +-/ + +module + +public import Mathlib.Init + +/-! +# Potential Responses + +This module supplies an assumption-free functional representation of potential responses. + +`PotentialResponse.select` produces a theoretical selected response, not a recorded outcome. +`PotentialResponse.comp` performs same-unit substitution. + +Causal assumptions, estimands, estimators, probability structure, and statistical inference are +deferred to later modules. +-/ + +@[expose] public section + +/-- A potential response assigns a value to each intervention and unit. -/ +abbrev PotentialResponse + (Intervention : Type*) (Unit : Type*) (Value : Type*) := + Intervention → Unit → Value + +namespace PotentialResponse + +variable {Intervention : Type*} {Unit : Type*} {Value : Type*} {Index : Type*} + +/-- Selects each unit's response at the intervention supplied for that unit. -/ +def select + (response : PotentialResponse Intervention Unit Value) + (intervention : Unit → Intervention) : + Unit → Value := + fun u ↦ response (intervention u) u + +/-- Substitutes an intervention response into a response, evaluating both at the same unit. -/ +def comp + (response : PotentialResponse Intervention Unit Value) + (intervention : + PotentialResponse Index Unit Intervention) : + PotentialResponse Index Unit Value := + fun index u ↦ response (intervention index u) u + +@[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 + +end PotentialResponse From ef06f4bec50c971f8d7808787b3c21c62c6fa217 Mon Sep 17 00:00:00 2001 From: Bo Cowgill Date: Fri, 28 Aug 2026 16:18:50 -0600 Subject: [PATCH 2/4] Add same-unit substitution laws --- Statlib/Causal/PotentialResponse.lean | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/Statlib/Causal/PotentialResponse.lean b/Statlib/Causal/PotentialResponse.lean index 364f63f..5b17f6b 100644 --- a/Statlib/Causal/PotentialResponse.lean +++ b/Statlib/Causal/PotentialResponse.lean @@ -29,7 +29,8 @@ abbrev PotentialResponse namespace PotentialResponse -variable {Intervention : Type*} {Unit : Type*} {Value : Type*} {Index : Type*} +variable {Intervention : Type*} {Unit : Type*} {Value : Type*} + {Index : Type*} {Source : Type*} /-- Selects each unit's response at the intervention supplied for that unit. -/ def select @@ -62,4 +63,19 @@ def comp 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 From b9f24e2eca1bc727a87470b7a8a335f143873f8f Mon Sep 17 00:00:00 2001 From: Bo Cowgill Date: Wed, 9 Sep 2026 17:02:01 -0400 Subject: [PATCH 3/4] Add identity potential response --- Statlib/Causal/PotentialResponse.lean | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/Statlib/Causal/PotentialResponse.lean b/Statlib/Causal/PotentialResponse.lean index 5b17f6b..4c08e4f 100644 --- a/Statlib/Causal/PotentialResponse.lean +++ b/Statlib/Causal/PotentialResponse.lean @@ -13,6 +13,7 @@ public import Mathlib.Init This module supplies an assumption-free functional representation of potential responses. +`PotentialResponse.id` is the identity for same-unit substitution. `PotentialResponse.select` produces a theoretical selected response, not a recorded outcome. `PotentialResponse.comp` performs same-unit substitution. @@ -32,6 +33,10 @@ namespace PotentialResponse variable {Intervention : Type*} {Unit : Type*} {Value : Type*} {Index : Type*} {Source : Type*} +/-- The identity potential response returns its intervention and ignores the unit. -/ +def id : PotentialResponse Intervention Unit Intervention := + fun intervention _ ↦ intervention + /-- Selects each unit's response at the intervention supplied for that unit. -/ def select (response : PotentialResponse Intervention Unit Value) @@ -47,6 +52,9 @@ def comp PotentialResponse Index Unit Value := fun index u ↦ response (intervention index u) u +@[simp] theorem id_apply (intervention : Intervention) (u : Unit) : + (id : PotentialResponse Intervention Unit Intervention) intervention u = intervention := rfl + @[simp] theorem select_apply (response : PotentialResponse Intervention Unit Value) (intervention : Unit → Intervention) @@ -65,11 +73,11 @@ def comp @[simp] theorem comp_id (response : PotentialResponse Intervention Unit Value) : - response.comp (fun intervention _ ↦ intervention) = response := rfl + response.comp id = response := rfl @[simp] theorem id_comp (response : PotentialResponse Intervention Unit Value) : - comp (fun value _ ↦ value) response = response := rfl + id.comp response = response := rfl theorem comp_assoc (response : PotentialResponse Intervention Unit Value) From 2d9a3a20d1da07471f9ec46371104b501ad55a48 Mon Sep 17 00:00:00 2001 From: Bo Cowgill Date: Fri, 11 Sep 2026 18:35:32 -0400 Subject: [PATCH 4/4] Document nested potential-response composition --- Statlib/Causal/PotentialResponse.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Statlib/Causal/PotentialResponse.lean b/Statlib/Causal/PotentialResponse.lean index 4c08e4f..d92bb3f 100644 --- a/Statlib/Causal/PotentialResponse.lean +++ b/Statlib/Causal/PotentialResponse.lean @@ -17,6 +17,17 @@ This module supplies an assumption-free functional representation of potential r `PotentialResponse.select` produces a theoretical selected response, not a recorded outcome. `PotentialResponse.comp` performs same-unit substitution. +For example, given `mediator : PotentialResponse Treatment Unit Mediator` and +`outcome : PotentialResponse (Treatment × Mediator) Unit Outcome`, the response + +```lean +outcome.comp (fun (treatment, mediatorTreatment) unit ↦ + (treatment, mediator mediatorTreatment unit)) +``` + +evaluated at `(a, a')` and `u` is `outcome (a, mediator a' u) u`, representing the nested +response $Y(a, M(a'))$. The mediator and outcome responses are evaluated at the same unit `u`. + Causal assumptions, estimands, estimators, probability structure, and statistical inference are deferred to later modules. -/