Finite Event Coupling Sharp Bounds

Abstract

A two-event coupling polytope has an explicit primal witness, replayable dual-slack certificate, and exact sharp projection bounds.

The feasible object is a normalized nonnegative law on two Boolean event indicators with two prescribed marginals. Its target coordinate is the true-true intersection cell.

Normalization and the two marginal rows produce exact slack identities for the Fréchet lower plane and the two upper planes. An additional linear cap on disagreement contributes a fourth lower plane.

The explicit four-cell coupling realizes every target in the resulting closed interval. The necessity proof replays the certificate, while the sufficiency proof constructs the primal witness.

Theorem 1.1 (Marginal rows generate a replayable dual-slack certificate).

$\forall ma ss \in Prod (B oo l, B oo l) \to R e a l, l e f tM a r g ina l \in R e a l, r i g h 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, IsEventCoupling (ma ss, l e f tM a r g ina l, r i g h tM a r g ina l) \Rightarrow EventCouplingDualCertificate (ma ss, l e f tM a r g ina l, r i g h 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/FiniteEventCouplingSharpBounds.event_coupling_dual_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every feasible coupling and every proposed disagreement cap, the four exact slack identities hold. Nonnegativity and the cap can then be checked separately when the certificate is replayed.

Theorem 1.2 (The disagreement-constrained interval is exactly sharp).

$\forall l e f tM a r g ina l \in R e a l, r i g h 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, l e f tM a r g ina l + r i g h tM a r g ina l - 1), \frac{l e f tM a r g ina l + r i g h 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 (l e f tM a r g ina l, r i g h tM a r g ina l)) \Leftrightarrow (\exists ma ss \in Prod (B oo l, B oo l) \to R e a l, IsEventCoupling (ma ss, l e f tM a r g ina l, r i g h tM a r g ina l) \land (disagreementMass (ma ss) \leq d i s a g ree m e n tC a p \land ma ss (pair (t r u e, t r u e)) = t a r g e t))$

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

Source. Repository-derived.

Commentary.

A real target lies in the displayed interval exactly when some normalized nonnegative coupling has the required marginals, obeys the disagreement cap, and realizes that target.

References

Truth anchor: D5/S3/ConceptDynamics/Causal/FiniteEventCouplingSharpBounds.event_coupling_dual_certificate
Truth anchor: D5/S3/ConceptDynamics/Causal/FiniteEventCouplingSharpBounds.event_coupling_target_feasible_with_disagreement_cap_iff
Dependency: D5/S3/ConceptDynamics/Causal/BenefitProbabilityBounds

Keyboard shortcuts

trureturing Blueprint

Finite Event Coupling Sharp Bounds

Abstract

References