Complete mediation, weighted cuts and exact pricing

Abstract

Complete mediation uses one response table in both treatment worlds. For a fixed mediator coupling, fair response marginals yield an exact weighted-cut interval and attaining independent-noise models.

Mediator is an arbitrary finite type with decidable equality. coupling is an existing normalized nonnegative rational law on Mediator times Mediator; law is such a law on Mediator to Bool. table and best are complete Boolean response assignments, multiplier maps mediator states to rationals, and target is rational. All sums use the full finite carriers. The set Values displayed by setOf is the actual image of all fair laws under completeMediatorBenefit. The final two entries specialize Mediator to Fin 3.

Definition 1.1 (Embed the no-direct-effect mechanism).

$$\forall Mediator,law,(\mathrm{completeOutcomeLaw}(law))=(\mathrm{pushforwardResponseLaw}(law,(\lambda table\mapsto (\lambda index\mapsto \mathrm{table}(\mathrm{snd}(index))))))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.completeOutcomeLaw (✓ std3).

Source. Repository-derived.

Commentary.

Both treatment coordinates read the same original response-table entry. This enforces equality of coordinates, rather than only equality of their means.

Theorem 1.2 (Recover the actual success kernel).

$$\forall Mediator,law,a,m,(\mathrm{outcomeSuccess}(\mathrm{completeOutcomeLaw}(law),a,m))=(\mathrm{linearObjective}((\lambda table\mapsto \mathrm{ite}(\mathrm{apply}(table,m),1,0)),\mathrm{mass}(law)))$$

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

Source. Repository-derived.

Commentary.

The existing pushforward expectation theorem identifies each intervention success probability.

Definition 1.3 (Fair response coordinates).

$$\forall Mediator,law,(\mathrm{FairCompleteOutcome}(law))\iff (\forall m,(\mathrm{linearObjective}((\lambda table\mapsto \mathrm{ite}(\mathrm{apply}(table,m),1,0)),\mathrm{mass}(law)))=(\frac{1}{2}))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.FairCompleteOutcome (✓ std3).

Source. Repository-derived.

Commentary.

Each mediator-indexed outcome response has probability one half. Dependence between different coordinates remains unrestricted.

Theorem 1.4 (Bind fairness to the mediator kernel API).

$$\forall Mediator,law,(\mathrm{FairCompleteOutcome}(law))\Rightarrow (\mathrm{HasOutcomeKernel}(\mathrm{completeOutcomeLaw}(law),(\lambda index\mapsto \frac{1}{2})))$$

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

Source. Repository-derived.

Commentary.

The input condition is transported to the existing full treatment/mediator success-kernel predicate.

Definition 1.5 (Use the original independent source query).

$$\forall Mediator,coupling,law,(\mathrm{completeMediatorBenefit}(coupling,law))=(\mathrm{partialMediatorBenefit}(coupling,\mathrm{completeOutcomeLaw}(law)))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.completeMediatorBenefit (✓ std3).

Source. Repository-derived.

Commentary.

The mediator coupling stays fixed and the lifted outcome disturbance is combined with it by the existing product semantics.

Theorem 1.6 (Identify the actual benefit response cell).

$$\forall Mediator,coupling,law,(\mathrm{completeMediatorBenefit}(coupling,law))=(\mathrm{benefitResponseMass}(\mathrm{mass}(\mathrm{partialMediatorResponseLaw}(coupling,\mathrm{completeOutcomeLaw}(law)))))$$

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

Source. Repository-derived.

Commentary.

The query is tied to the original two-world response pushforward and its existing benefit cell.

Definition 1.7 (Directed weight crossing a Boolean cut).

$$\forall Mediator,coupling,table,(\mathrm{mediatorCutMass}(coupling,table))=(\mathrm{linearObjective}((\lambda pair\mapsto \mathrm{ite}((\mathrm{table}(\mathrm{fst}(pair)))\ne (\mathrm{table}(\mathrm{snd}(pair))),1,0)),\mathrm{mass}(coupling)))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.mediatorCutMass (✓ std3).

Source. Repository-derived.

Commentary.

Each directed pair contributes its own weight. Symmetry is not assumed; loops never cross a cut.

Theorem 1.8 (Retain the complete mean-drift identity).

$$\forall Mediator,coupling,law,((2)\cdot (\mathrm{completeMediatorBenefit}(coupling,law)))=((\mathrm{linearObjective}((\lambda table\mapsto \mathrm{mediatorCutMass}(coupling,table)),\mathrm{mass}(law)))+(\sum _{pair}((\mathrm{mass}(coupling,pair))\cdot ((\mathrm{linearObjective}((\lambda table\mapsto \mathrm{ite}(\mathrm{apply}(table,\mathrm{snd}(pair)),1,0)),\mathrm{mass}(law)))-(\mathrm{linearObjective}((\lambda table\mapsto \mathrm{ite}(\mathrm{apply}(table,\mathrm{fst}(pair)),1,0)),\mathrm{mass}(law)))))))$$

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

Source. Repository-derived.

Commentary.

The pointwise Boolean identity is averaged under the actual source law. Fairness is not needed for this identity.

Definition 1.9 (Actual outcome-column reduced cost).

$$\forall Mediator,coupling,multiplier,table,(\mathrm{completeMediatorPricingScore}(coupling,multiplier,table))=((\mathrm{linearObjective}((\lambda pair\mapsto \mathrm{ite}(((\mathrm{table}(\mathrm{fst}(pair)))=(false))\wedge ((\mathrm{table}(\mathrm{snd}(pair)))=(true)),1,0)),\mathrm{mass}(coupling)))-(\sum _m((\mathrm{multiplier}(m))\cdot (\mathrm{ite}(\mathrm{apply}(table,m),1,0)))))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.completeMediatorPricingScore (✓ std3).

Source. Repository-derived.

Commentary.

This subtracts the outcome-marginal dual terms from the actual deterministic benefit column. The separate constant normalization multiplier is omitted because it cannot affect the maximizing assignment.

Theorem 1.10 (Expose cut plus vertex-field pricing).

$$\forall Mediator,coupling,multiplier,table,((2)\cdot (\mathrm{completeMediatorPricingScore}(coupling,multiplier,table)))=((\mathrm{mediatorCutMass}(coupling,table))+(\sum _m((((\mathrm{rightResponseMarginal}(\mathrm{mass}(coupling),m))-(\mathrm{leftResponseMarginal}(\mathrm{mass}(coupling),m)))-((2)\cdot (\mathrm{multiplier}(m))))\cdot (\mathrm{ite}(\mathrm{apply}(table,m),1,0)))))$$

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

Source. Repository-derived.

Commentary.

The identity retains incoming and outgoing mediator masses and every rational dual multiplier. It is exact for arbitrary directed couplings and does not assert an efficient generic graph solver.

Theorem 1.11 (Cancel drift using the fair kernel).

$$\forall Mediator,coupling,law,(\mathrm{FairCompleteOutcome}(law))\Rightarrow ((\mathrm{completeMediatorBenefit}(coupling,law))=(\frac{\mathrm{linearObjective}((\lambda table\mapsto \mathrm{mediatorCutMass}(coupling,table)),\mathrm{mass}(law))}{2}))$$

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

Source. Repository-derived.

Commentary.

Equal coordinate success probabilities cancel every signed mean difference, leaving half the expected weighted cut.

Definition 1.12 (One fair disturbance selects an assignment or its complement).

$$\forall Mediator,table,(\mathrm{complementOutcomeLaw}(table))=(\mathrm{pushforwardResponseLaw}(\mathrm{uniformThresholdLaw}(2),(\lambda bit\mapsto \mathrm{ite}((bit)=(0),table,(\lambda m\mapsto \mathrm{not}(\mathrm{table}(m)))))))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.complementOutcomeLaw (✓ std3).

Source. Repository-derived.

Commentary.

The positive-denominator proof is implicit in the displayed two-point uniform law. The same one-bit disturbance controls all response coordinates.

Theorem 1.13 (Simultaneous fairness of all coordinates).

$$\forall Mediator,table,\mathrm{FairCompleteOutcome}(\mathrm{complementOutcomeLaw}(table))$$

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

Source. Repository-derived.

Commentary.

The two complementary complete assignments jointly realize the prescribed success probability at every mediator value.

Theorem 1.14 (Whole-table complementation preserves the cut).

$$\forall Mediator,coupling,table,(\mathrm{mediatorCutMass}(coupling,(\lambda m\mapsto \mathrm{not}(\mathrm{table}(m)))))=(\mathrm{mediatorCutMass}(coupling,table))$$

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

Source. Repository-derived.

Commentary.

Every edge has unchanged disagreement status after both endpoints are complemented.

Theorem 1.15 (Realize every deterministic cut value).

$$\forall Mediator,coupling,table,(\mathrm{completeMediatorBenefit}(coupling,\mathrm{complementOutcomeLaw}(table)))=(\frac{\mathrm{mediatorCutMass}(coupling,table)}{2})$$

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

Source. Repository-derived.

Commentary.

The actual no-direct-effect model attains half the chosen cut mass, using one shared outcome disturbance independent of the mediator disturbance.

Theorem 1.16 (Obtain a maximizing cut and an attaining causal maximum).

$$\forall Mediator,coupling,\exists best,(\forall table,(\mathrm{mediatorCutMass}(coupling,table))\le (\mathrm{mediatorCutMass}(coupling,best)))\wedge (\mathrm{IsGreatest}(\mathrm{setOf}((\lambda value\mapsto \exists law,(\mathrm{FairCompleteOutcome}(law))\wedge ((\mathrm{completeMediatorBenefit}(coupling,law))=(value)))),\frac{\mathrm{mediatorCutMass}(coupling,best)}{2}))$$

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

Source. Repository-derived.

Commentary.

Finite.exists_max chooses from the full Boolean assignment carrier. A complement pair attains the bound; every fair law is bounded by the maximum cut.

Theorem 1.17 (Exact image for every rational target).

$$\forall Mediator,coupling,\exists best,(\forall table,(\mathrm{mediatorCutMass}(coupling,table))\le (\mathrm{mediatorCutMass}(coupling,best)))\wedge (\forall target,(\exists law,(\mathrm{FairCompleteOutcome}(law))\wedge ((\mathrm{completeMediatorBenefit}(coupling,law))=(target)))\iff (((0)\le (target))\wedge ((target)\le (\frac{\mathrm{mediatorCutMass}(coupling,best)}{2}))))$$

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

Source. Repository-derived.

Commentary.

The lower witness uses two constant assignments. Mixing it with the maximizing complement law fills the entire interval within one outcome mechanism and leaves the mediator coupling unchanged.

Theorem 1.18 (Full cut mass is a simultaneous support condition).

$$\forall Mediator,coupling,table,((\mathrm{mediatorCutMass}(coupling,table))=(1))\iff (\forall pair,((\mathrm{mass}(coupling,pair))\ne (0))\Rightarrow ((\mathrm{table}(\mathrm{fst}(pair)))\ne (\mathrm{table}(\mathrm{snd}(pair)))))$$

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

Source. Repository-derived.

Commentary.

Nonnegative missed-edge masses sum to zero exactly when no positive mediator pair remains unseparated.

Theorem 1.19 (Characterize saturation by a single two-coloring).

$$\forall Mediator,coupling,(\exists law,(\mathrm{FairCompleteOutcome}(law))\wedge ((\mathrm{completeMediatorBenefit}(coupling,law))=(\frac{1}{2})))\iff (\exists table,\forall pair,((\mathrm{mass}(coupling,pair))\ne (0))\Rightarrow ((\mathrm{table}(\mathrm{fst}(pair)))\ne (\mathrm{table}(\mathrm{snd}(pair)))))$$

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

Source. Repository-derived.

Commentary.

This is a full iff on the positive directed-pair support. It treats loops and odd cycles through the actual Boolean separation condition.

Definition 1.20 (Normalized directed three-cycle instance).

$$\forall pair,(\mathrm{mass}(\mathrm{threeCycleCoupling}(),pair))=(\mathrm{ite}(((pair)=(\mathrm{pair}(0,1)))\vee (((pair)=(\mathrm{pair}(1,2)))\vee ((pair)=(\mathrm{pair}(2,0)))),\frac{1}{3},0))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.threeCycleCoupling (✓ std3).

Source. Repository-derived.

Commentary.

The complete mediator law has three equally weighted directed edges. The source supplies nonnegativity and normalization, with no estimated edge weights.

Theorem 1.21 (Exact one-third endpoint on the odd cycle).

$$\mathrm{IsGreatest}(\mathrm{setOf}((\lambda value\mapsto \exists law,(\mathrm{FairCompleteOutcome}(law))\wedge ((\mathrm{completeMediatorBenefit}(\mathrm{threeCycleCoupling}(),law))=(value)))),\frac{1}{3})$$

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

Source. Repository-derived.

Commentary.

Every Boolean labeling cuts at most two of the three cycle edges. The assignment 001 and its complement give an actual fair attaining outcome law. The cellwise half bound is therefore strictly loose.

References

• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.FairCompleteOutcome
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.complementOutcomeLaw
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.complementOutcomeLaw_benefit
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.complementOutcomeLaw_fair
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.completeMediatorBenefit
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.completeMediatorBenefit_actual_response
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.completeMediatorBenefit_cut_identity
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.completeMediatorPricingScore
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.completeMediatorPricingScore_graph_identity
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.completeOutcomeLaw
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.completeOutcomeLaw_fair_kernel
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.completeOutcomeLaw_success
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.complete_mediator_cut_interval
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.complete_mediator_half_attainable_iff
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.complete_mediator_maxcut_sharp
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.fair_completeMediatorBenefit_eq_half_cut
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.mediatorCutMass
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.mediatorCutMass_complement
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.mediatorCutMass_eq_one_iff
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.threeCycleCoupling
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds.three_cycle_complete_mediation_sharp
• Dependency: D5/S3/ConceptDynamics/CausalMoments/PartialMediatorTransportReduction