UnknownCouplingFairMediation

Abstract

Optimize both independent source laws exactly in the fair complete-mediation model with only mediator marginals supplied.

M is an arbitrary finite type with decidable equality. control and treated are normalized rational FiniteResponseLaw values on M. coupling is a law on M times M; law is a law on complete tables M to Bool. HasMediatorMarginals and FairCompleteOutcome are the existing original causal predicates. Independent mechanisms and the no-direct-effect equation are built into completeMediatorBenefit. target is rational; table and best are Boolean functions on the whole M carrier.

Definition 1.1 (Combined selected mediator mass).

$\forall M, co n t ro l, t re a t e d, t ab l e, (partitionWeight (co n t ro l, t re a t e d, t ab l e)) = ((linearObjective (λi, ite (table (i), 1, 0), mass (co n t ro l))) + (linearObjective (λi, ite (table (i), 1, 0), mass (t re a t e d))))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/UnknownCouplingFairMediation.partitionWeight (✓ std3).

Source. Repository-derived.

Commentary.

This is the sum of control(i)+treated(i) over the selected original mediator states. Its full-carrier total is two.

Definition 1.2 (Crossing score of one partition).

$\forall M, co n t ro l, t re a t e d, t ab l e, (partitionScore (co n t ro l, t re a t e d, t ab l e)) = ((1) - (∣(partitionWeight (co n t ro l, t re a t e d, t ab l e)) - (1)∣))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/UnknownCouplingFairMediation.partitionScore (✓ std3).

Source. Repository-derived.

Commentary.

Only the combined marginal weights enter this score. They do not specify an independent mediator coupling.

Theorem 1.3 (Bound all compatible mediator couplings).

$\forall M, co u pl in g, co n t ro l, t re a t e d, t ab l e, (HasMediatorMarginals (co u pl in g, co n t ro l, t re a t e d)) \Rightarrow ((mediatorCutMass (co u pl in g, t ab l e)) \leq (partitionScore (co n t ro l, t re a t e d, t ab l e)))$

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

Source. Repository-derived.

Commentary.

The pointwise crossing indicator is bounded both by the sum of endpoint labels and by its complement. All original marginal equalities are retained.

Theorem 1.4 (Construct an attaining original mediator law).

$\forall M, co n t ro l, t re a t e d, t ab l e, \exists co u pl in g, (HasMediatorMarginals (co u pl in g, co n t ro l, t re a t e d)) \land ((mediatorCutMass (co u pl in g, t ab l e)) = (partitionScore (co n t ro l, t re a t e d, t ab l e)))$

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

Source. Repository-derived.

Commentary.

The existing Boolean Frechet law supplies a maximal-crossing coarse plan. The exact lift returns every individual original marginal and the same cut expectation, including null partitions.

Theorem 1.5 (Complete identified interval with both laws unknown).

$\forall M, co n t ro l, t re a t e d, \exists b es t, (\forall t ab l e, (partitionScore (co n t ro l, t re a t e d, t ab l e)) \leq (partitionScore (co n t ro l, t re a t e d, b es t))) \land (\forall t a r g e t, (\exists co u pl in g, l a w, (HasMediatorMarginals (co u pl in g, co n t ro l, t re a t e d)) \land (FairCompleteOutcome (l a w)) \land ((completeMediatorBenefit (co u pl in g, l a w)) = (t a r g e t))) \Leftrightarrow (((0) \leq (t a r g e t)) \land ((t a r g e t) \leq (\frac{partitionScore ( co n t ro l , t re a t e d , b es t )}{2}))))$

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

Source. Repository-derived.

Commentary.

The optimal partition is obtained over the full finite carrier. One constructed mediator coupling already attains all intermediate targets through the existing fixed-coupling outcome-mixture theorem. No optimal coupling is assumed.

Theorem 1.6 (Exact one-half saturation criterion).

$\forall M, co n t ro l, t re a t e d, (\exists co u pl in g, l a w, (HasMediatorMarginals (co u pl in g, co n t ro l, t re a t e d)) \land (FairCompleteOutcome (l a w)) \land ((completeMediatorBenefit (co u pl in g, l a w)) = (\frac{1}{2}))) \Leftrightarrow (\exists t ab l e, (partitionWeight (co n t ro l, t re a t e d, t ab l e)) = (1))$

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

Source. Repository-derived.

Commentary.

This is an exact subset-partition condition on the combined mediator marginals. It is not a claim that generic nonfair or additionally restricted models have the same optimum.

trureturing — Discovering truth

UnknownCouplingFairMediation

Abstract

References

Keyboard shortcuts

trureturing — Discovering truth

UnknownCouplingFairMediation

Abstract

References