Ternary Treatment and Outcome Sharp Bounds

Abstract

A three-level treatment, three-level outcome structural response model has closed-form sharp bounds with primal and dual witnesses.

The exogenous response type has four states. Its first bit records whether treatment zero produces outcome zero, and its second bit records whether treatment two produces outcome two.

Treatment one produces the neutral outcome one. The endpoint joint counterfactual query is therefore the true-true response cell, while the two endpoint interventional probabilities are its Boolean marginals.

A cap on endpoint disagreement is a linear cross-world dependence restriction. The generic finite coupling theorem supplies both the dual certificate and an exogenous law attaining every point of the interval.

Theorem 1.1 (The ternary endpoint model inherits the coupling certificate).

$\forall ma ss \in R es p o n se T y p e \to R e a l, zero T a r g e tM a r g ina l \in R e a l, tw o T a r g e tM a r g ina l \in R e a l, d i s a g ree m e n tC a p \in R e a l, IsEndpointModel (ma ss, zero T a r g e tM a r g ina l, tw o T a r g e tM a r g ina l, d i s a g ree m e n tC a p) \Rightarrow EventCouplingDualCertificate (ma ss, zero T a r g e tM a r g ina l, tw o T a r g e tM a r g ina l, d i s a g ree m e n tC a p)$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Causal/TernaryTreatmentOutcomeSharpBounds.endpoint_model_dual_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every endpoint model unfolds to a feasible two-event coupling plus the disagreement constraint. Its marginal rows therefore carry the same exact dual-slack certificate.

Theorem 1.2 (The ternary endpoint joint query has an exact sharp interval).

$\forall zero T a r g e tM a r g ina l \in R e a l, tw o T a r g e tM a r g ina l \in R e a l, d i s a g ree m e n tC a p \in R e a l, t a r g e t \in R e a l, (max (max (0, zero T a r g e tM a r g ina l + tw o T a r g e tM a r g ina l - 1), \frac{zero T a r g e tM a r g ina l + tw o T a r g e tM a r g ina l - d i s a g ree m e n tC a p}{2}) \leq t a r g e t \land t a r g e t \leq min (zero T a r g e tM a r g ina l, tw o T a r g e tM a r g ina l)) \Leftrightarrow (\exists ma ss \in R es p o n se T y p e \to R e a l, IsEndpointModel (ma ss, zero T a r g e tM a r g ina l, tw o T a r g e tM a r g ina l, d i s a g ree m e n tC a p) \land endpointJointQuery (ma ss) = t a r g e t)$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Causal/TernaryTreatmentOutcomeSharpBounds.ternary_endpoint_joint_query_sharp_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed interval is necessary by certificate replay and sufficient by an explicit four-state exogenous response law. Both endpoints and every interior value are attained.

References

Truth anchor: D5/S3/ConceptDynamics/Causal/TernaryTreatmentOutcomeSharpBounds.endpoint_model_dual_certificate
Truth anchor: D5/S3/ConceptDynamics/Causal/TernaryTreatmentOutcomeSharpBounds.ternary_endpoint_joint_query_sharp_iff
Dependency: D5/S3/ConceptDynamics/Causal/FiniteEventCouplingSharpBounds

Keyboard shortcuts

trureturing Blueprint

Ternary Treatment and Outcome Sharp Bounds

Abstract

References