Exact partial-mediator transport reduction

Abstract

For binary treatment and outcome with a finite mediator and independent mechanism disturbances, one transportation matrix and two linear inequalities characterize every attainable rational benefit target.

Mediator is any finite type with decidable equality. control and treated are FiniteResponseLaw values on Mediator; coupling is such a law on Mediator times Mediator; outcome is such a law on complete tables Bool times Mediator to Bool. probability is a rational success kernel. Expectations below use the existing linearObjective. The direct treatment-to-outcome edge is allowed; there is no exclusion restriction equating the two treatment rows.

Definition 1.1 (One mediator transport matrix).

$\forall co u pl in g, co n t ro l, t re a t e d, (HasMediatorMarginals (co u pl in g, co n t ro l, t re a t e d)) \Leftrightarrow ((\forall m, (leftResponseMarginal (mass (co u pl in g), m)) = (mass (co n t ro l, m))) \land (\forall m, (rightResponseMarginal (mass (co u pl in g), m)) = (mass (t re a t e d, m))))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.HasMediatorMarginals (✓ std3).

Source. Repository-derived.

Commentary.

Nonnegative normalization is supplied by FiniteResponseLaw. All row and column equations constrain the same matrix, rather than separate cellwise maximizers.

Definition 1.2 (Prescribed outcome mechanism kernel).

$\forall o u t co m e, p ro babi l i t y, (HasOutcomeKernel (o u t co m e, p ro babi l i t y)) \Leftrightarrow (\forall a, m, (outcomeSuccess (o u t co m e, a, m)) = (probability ((a, m))))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.HasOutcomeKernel (✓ std3).

Source. Repository-derived.

Commentary.

The kernel consists of intervention success probabilities. Observational identification and zero-probability parent cells require separate assumptions.

Definition 1.3 (Actual common-source counterfactual law).

$\forall co u pl in g, o u t co m e, (partialMediatorResponseLaw (co u pl in g, o u t co m e)) = (pushforwardResponseLaw (productResponseLaw (co u pl in g, o u t co m e), res p o n se M a p))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.partialMediatorResponseLaw (✓ std3).

Source. Repository-derived.

Commentary.

responseMap((m0,m1),table) is (table(false,m0),table(true,m1)). Both worlds read the same mediator pair and the same outcome table. The product law makes only the two mechanisms independent.

Definition 1.4 (Benefit under the independent source law).

$\forall co u pl in g, o u t co m e, (partialMediatorBenefit (co u pl in g, o u t co m e)) = (linearObjective (b e n e f i tE v e n t, mass (productResponseLaw (co u pl in g, o u t co m e))))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.partialMediatorBenefit (✓ std3).

Source. Repository-derived.

Commentary.

benefitEvent is the indicator that responseMap is (false,true). It is evaluated on the complete product source, not declared to equal a transport objective.

Theorem 1.5 (Bind to the existing causal benefit readout).

$\forall co u pl in g, o u t co m e, (partialMediatorBenefit (co u pl in g, o u t co m e)) = (benefitResponseMass (mass (partialMediatorResponseLaw (co u pl in g, o u t co m e))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.partialMediatorBenefit_actual_response (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof uses the existing deterministic-pushforward expectation identity and the actual 01 response cell.

Theorem 1.6 (Derive the bilinear mechanism decomposition).

$\forall co u pl in g, o u t co m e, (partialMediatorBenefit (co u pl in g, o u t co m e)) = (p ai r \sum ((outcomeBenefitCell (o u t co m e, fst (p ai r), snd (p ai r))) \cdot (mass (co u pl in g, p ai r))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.partialMediatorBenefit_eq_cells (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite independent-product sum is expanded without discarding the common mediator coupling.

Definition 1.7 (Lower transport cost).

$\forall p ro babi l i t y, p ai r, (lowerTransportCost (p ro babi l i t y, p ai r)) = (max (0, (probability ((t r u e, snd (p ai r)))) - (probability ((f a l se, fst (p ai r))))))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.lowerTransportCost (✓ std3).

Source. Repository-derived.

Commentary.

This is the lower Boolean response-cell bound at the two mediator values.

Definition 1.8 (Upper transport cost).

$\forall p ro babi l i t y, p ai r, (upperTransportCost (p ro babi l i t y, p ai r)) = (min ((1) - (probability ((f a l se, fst (p ai r)))), probability ((t r u e, snd (p ai r)))))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.upperTransportCost (✓ std3).

Source. Repository-derived.

Commentary.

The cost is multiplied by one globally feasible transport matrix. There is no substitution of an independently maximized mediator cell.

Theorem 1.9 (Necessary bounds at the actual mediator law).

$\forall p ro babi l i t y, co u pl in g, o u t co m e, (HasOutcomeKernel (o u t co m e, p ro babi l i t y)) \Rightarrow (((linearObjective (lowerTransportCost (p ro babi l i t y), mass (co u pl in g))) \leq (partialMediatorBenefit (co u pl in g, o u t co m e))) \land ((partialMediatorBenefit (co u pl in g, o u t co m e)) \leq (linearObjective (upperTransportCost (p ro babi l i t y), mass (co u pl in g)))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.partialMediatorBenefit_transport_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

Weights are nonnegative and every outcome-law cell obeys the already proved bound.

Theorem 1.10 (Common mechanisms attain both costs).

$\forall p ro babi l i t y, (\forall in d e x, ((0) \leq (probability (in d e x))) \land ((probability (in d e x)) \leq (1))) \Rightarrow (\exists l o w er, u pp er, (HasOutcomeKernel (l o w er, p ro babi l i t y)) \land ((HasOutcomeKernel (u pp er, p ro babi l i t y)) \land (\forall co u pl in g, ((partialMediatorBenefit (co u pl in g, l o w er)) = (linearObjective (lowerTransportCost (p ro babi l i t y), mass (co u pl in g)))) \land ((partialMediatorBenefit (co u pl in g, u pp er)) = (linearObjective (upperTransportCost (p ro babi l i t y), mass (co u pl in g)))))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.simultaneous_transport_endpoint_mechanisms (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two outcome laws are selected before all mediator couplings. This discharges simultaneous attainability rather than assuming that individual cell bounds can be combined.

Theorem 1.11 (Full rational interval at one mediator coupling).

$\forall p ro babi l i t y, co u pl in g, t a r g e t, (\forall in d e x, ((0) \leq (probability (in d e x))) \land ((probability (in d e x)) \leq (1))) \Rightarrow ((\exists o u t co m e, (HasOutcomeKernel (o u t co m e, p ro babi l i t y)) \land ((partialMediatorBenefit (co u pl in g, o u t co m e)) = (t a r g e t))) \Leftrightarrow (((linearObjective (lowerTransportCost (p ro babi l i t y), mass (co u pl in g))) \leq (t a r g e t)) \land ((t a r g e t) \leq (linearObjective (upperTransportCost (p ro babi l i t y), mass (co u pl in g))))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.fixed_coupling_benefit_sharp_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

Interior targets mix only the two complete outcome laws, with the mediator law fixed. Rational interpolation covers endpoints and the zero-width case while retaining mechanism independence.

Theorem 1.12 (Exact transportation-LP characterization).

$\forall co n t ro l, t re a t e d, p ro babi l i t y, t a r g e t, (\forall in d e x, ((0) \leq (probability (in d e x))) \land ((probability (in d e x)) \leq (1))) \Rightarrow ((\exists co u pl in g, o u t co m e, (HasMediatorMarginals (co u pl in g, co n t ro l, t re a t e d)) \land ((HasOutcomeKernel (o u t co m e, p ro babi l i t y)) \land ((partialMediatorBenefit (co u pl in g, o u t co m e)) = (t a r g e t)))) \Leftrightarrow (\exists co u pl in g, (HasMediatorMarginals (co u pl in g, co n t ro l, t re a t e d)) \land (((linearObjective (lowerTransportCost (p ro babi l i t y), mass (co u pl in g))) \leq (t a r g e t)) \land ((t a r g e t) \leq (linearObjective (upperTransportCost (p ro babi l i t y), mass (co u pl in g)))))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.partial_mediator_target_iff_transport (✓ std3). ∎

Source. Repository-derived.

Commentary.

The right side has m-squared coupling variables and linear row, column and target conditions. No outcome-law optimization, independent pairwise witnesses, or optimizer-existence premise remains.

Theorem 1.13 (Transport optima give causal endpoint witnesses).

$\forall co n t ro l, t re a t e d, p ro babi l i t y, l o w er, u pp er, l o w er C o u pl in g, u pp er C o u pl in g, ((\forall in d e x, ((0) \leq (probability (in d e x))) \land ((probability (in d e x)) \leq (1))) \land ((HasMediatorMarginals (l o w er C o u pl in g, co n t ro l, t re a t e d)) \land ((HasMediatorMarginals (u pp er C o u pl in g, co n t ro l, t re a t e d)) \land (((linearObjective (lowerTransportCost (p ro babi l i t y), mass (l o w er C o u pl in g))) = (l o w er)) \land (((linearObjective (upperTransportCost (p ro babi l i t y), mass (u pp er C o u pl in g))) = (u pp er)) \land (\forall co u pl in g, (HasMediatorMarginals (co u pl in g, co n t ro l, t re a t e d)) \Rightarrow (((l o w er) \leq (linearObjective (lowerTransportCost (p ro babi l i t y), mass (co u pl in g)))) \land ((linearObjective (upperTransportCost (p ro babi l i t y), mass (co u pl in g))) \leq (u pp er))))))))) \Rightarrow ((\forall co u pl in g, o u t co m e, ((HasMediatorMarginals (co u pl in g, co n t ro l, t re a t e d)) \land (HasOutcomeKernel (o u t co m e, p ro babi l i t y))) \Rightarrow (((l o w er) \leq (partialMediatorBenefit (co u pl in g, o u t co m e))) \land ((partialMediatorBenefit (co u pl in g, o u t co m e)) \leq (u pp er)))) \land ((\exists o u t co m e, (HasOutcomeKernel (o u t co m e, p ro babi l i t y)) \land ((partialMediatorBenefit (l o w er C o u pl in g, o u t co m e)) = (l o w er))) \land (\exists o u t co m e, (HasOutcomeKernel (o u t co m e, p ro babi l i t y)) \land ((partialMediatorBenefit (u pp er C o u pl in g, o u t co m e)) = (u pp er)))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.transport_endpoints_are_causal_sharp (✓ std3). ∎

Source. Repository-derived.

Commentary.

lowerCoupling and upperCoupling are actual probability laws with the displayed marginals. The premise includes their transport objective values and universal transport bounds. The conclusion gives universal causal bounds and actual outcome mechanisms attaining both endpoints with those same couplings.

Theorem 1.14 (One-dimensional absolute-distance cost identities).

$\forall p ro babi l i t y, co u pl in g, (((2) \cdot (linearObjective (lowerTransportCost (p ro babi l i t y), mass (co u pl in g)))) = (((m e an 1) - (m e an 0)) + (d i s t an ce 01))) \land (((2) \cdot (linearObjective (upperTransportCost (p ro babi l i t y), mass (co u pl in g)))) = ((((1) - (m e an 0)) + (m e an 1)) - (d i s t an ce C o m pl e m e n t)))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.transport_cost_absolute_distance_identities (✓ std3). ∎

Source. Repository-derived.

Commentary.

mean0 and mean1 abbreviate coupling expectations of probability(false,pair.first) and probability(true,pair.second). distance01 is the expectation of their absolute difference. distanceComplement is the expectation of the absolute value of one minus their sum. These are aliases for the full displayed finite sums in Lean. The theorem itself does not certify a sorting algorithm or invoke a Wasserstein implementation.

References

Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.HasMediatorMarginals
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.HasOutcomeKernel
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.fixed_coupling_benefit_sharp_iff
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.lowerTransportCost
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.partialMediatorBenefit
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.partialMediatorBenefit_actual_response
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.partialMediatorBenefit_eq_cells
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.partialMediatorBenefit_transport_bounds
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.partialMediatorResponseLaw
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.partial_mediator_target_iff_transport
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.simultaneous_transport_endpoint_mechanisms
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.transport_cost_absolute_distance_identities
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.transport_endpoints_are_causal_sharp
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction.upperTransportCost
Dependency: D5/S3/ConceptDynamics/CausalMoments/ProductLawMomentSparsification
Dependency: D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling
Dependency: D5/S3/ConceptDynamics/PartialIdentification/MarkovianBenefitIdentificationBoundary

Keyboard shortcuts

trureturing Blueprint

Exact partial-mediator transport reduction

Abstract

References