MediatorPricingRestriction

Abstract

Original causal pricing is preserved exactly under finite response-coordinate restriction.

M is finite with decidable equality. coupling is the existing normalized rational law on M times M; K is a Finset M; branch maps the subtype K to Bool; table and color map M to Bool; multiplier maps M to Q. All sums are over the whole M carrier.

Definition 1.1 (Extend the selected response assignment).

$$\forall M,K,branch,i,(\mathrm{pinTable}(K,branch,i))=(\mathrm{ite}((i)\in (K),\mathrm{branch}(i),false))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.pinTable (✓ std3).

Source. Repository-derived.

Commentary.

The branch is defined on the finite subtype K. The application branch(i) on membership uses the corresponding subtype witness; all other coordinates are false.

Definition 1.2 (Reassemble an original response column).

$$\forall M,K,branch,table,i,(\mathrm{clampTable}(K,branch,table,i))=(\mathrm{ite}((i)\in (K),\mathrm{apply}(\mathrm{pinTable}(K,branch),i),\mathrm{table}(i)))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.clampTable (✓ std3).

Source. Repository-derived.

Commentary.

Fixed coordinates use the selected branch and all free coordinates retain the supplied original table values.

Theorem 1.3 (Every original column has a branch).

$$\forall M,K,table,(\mathrm{clampTable}(K,\lambda i,\mathrm{table}(i),table))=(table)$$

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

Source. Repository-derived.

Commentary.

Here i in the restriction lambda ranges over K, with its underlying mediator value used by table. No original complete table is excluded.

Definition 1.4 (Redirect removed mass to the diagonal).

$$\forall M,K,pair,(\mathrm{absorbPair}(K,pair))=(\mathrm{ite}((\mathrm{not}((\mathrm{fst}(pair))\in (K)))\wedge (\mathrm{not}((\mathrm{snd}(pair))\in (K))),pair,\mathrm{pair}(\mathrm{fst}(pair),\mathrm{fst}(pair))))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.absorbPair (✓ std3).

Source. Repository-derived.

Commentary.

Free/free pairs are unchanged. All other pairs retain their mass on a diagonal pair. This is a computational map, not conditioning the mediator law.

Definition 1.5 (Keep the normalized response-law API).

$$\forall M,coupling,K,(\mathrm{residualCoupling}(coupling,K))=(\mathrm{pushforwardResponseLaw}(coupling,\mathrm{absorbPair}(K)))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.residualCoupling (✓ std3).

Source. Repository-derived.

Commentary.

The deterministic pushforward stays on the full mediator-pair carrier and preserves normalization and nonnegativity. Its changed marginal values are not substituted into the original data constraints.

Theorem 1.6 (Compute the residual off-diagonal coefficients).

$$\forall M,coupling,K,i,j,((i)\ne (j))\Rightarrow ((\mathrm{mass}(\mathrm{residualCoupling}(coupling,K),\mathrm{pair}(i,j)))=(\mathrm{ite}((\mathrm{not}((i)\in (K)))\wedge (\mathrm{not}((j)\in (K))),\mathrm{mass}(coupling,\mathrm{pair}(i,j)),0)))$$

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

Source. Repository-derived.

Commentary.

Outside the diagonal, the residual keeps exactly the original coefficients with both endpoints free.

Theorem 1.7 (Identify the exact graph condition).

$$\forall M,coupling,K,color,(\mathrm{OffDiagonalBipartite}(\mathrm{residualCoupling}(coupling,K),color))\iff (\forall i,j,((\mathrm{not}((i)\in (K)))\wedge (\mathrm{not}((j)\in (K)))\wedge ((i)\ne (j))\wedge ((\mathrm{mass}(coupling,\mathrm{pair}(i,j)))\ne (0)))\Rightarrow ((\mathrm{color}(i))\ne (\mathrm{color}(j))))$$

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

Source. Repository-derived.

Commentary.

Bipartiteness concerns the original support after removing K, including both directed orientations. Original self-loops impose no condition.

Definition 1.8 (Retain both oriented boundary contributions).

$$\forall M,coupling,K,branch,multiplier,i,(\mathrm{branchMultiplier}(coupling,K,branch,multiplier,i))=(((\mathrm{ite}((i)\in (K),0,\mathrm{multiplier}(i)))+(\sum _j(\mathrm{ite}((\mathrm{not}((i)\in (K)))\wedge ((j)\in (K))\wedge ((\mathrm{apply}(\mathrm{pinTable}(K,branch),j))=(true)),\mathrm{mass}(coupling,\mathrm{pair}(i,j)),0))))-(\sum _j(\mathrm{ite}(((j)\in (K))\wedge (\mathrm{not}((i)\in (K)))\wedge ((\mathrm{apply}(\mathrm{pinTable}(K,branch),j))=(false)),\mathrm{mass}(coupling,\mathrm{pair}(j,i)),0))))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.branchMultiplier (✓ std3).

Source. Repository-derived.

Commentary.

Free-to-fixed-one edges add to the multiplier; fixed-zero-to-free edges subtract. Fixed-coordinate multipliers become zero in the residual problem and stay in the branch offset.

Definition 1.9 (Compute the constant in the original objective).

$$\forall M,coupling,K,branch,multiplier,(\mathrm{branchOffset}(coupling,K,branch,multiplier))=(\mathrm{completeMediatorPricingScore}(coupling,multiplier,\mathrm{pinTable}(K,branch)))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.branchOffset (✓ std3).

Source. Repository-derived.

Commentary.

The offset includes fixed/fixed benefit, free-zero/fixed-one benefit and all original fixed-coordinate multiplier contributions.

Theorem 1.10 (Exact original-to-residual pricing equality).

$$\forall M,coupling,K,branch,multiplier,table,(\mathrm{completeMediatorPricingScore}(coupling,multiplier,\mathrm{clampTable}(K,branch,table)))=((\mathrm{branchOffset}(coupling,K,branch,multiplier))+(\mathrm{completeMediatorPricingScore}(\mathrm{residualCoupling}(coupling,K),\mathrm{branchMultiplier}(coupling,K,branch,multiplier),table)))$$

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

Source. Repository-derived.

Commentary.

This equality holds before any bipartite assumption. No removed mass is renormalized, and reassembly gives one actual original outcome-response table.

References

• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.absorbPair
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.branchMultiplier
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.branchOffset
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.clampTable
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.clampTable_restrict
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.pinTable
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.pricing_restriction_identity
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.residualCoupling
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.residualCoupling_bipartite_iff
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction.residualCoupling_offDiagonal
• Dependency: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing