SeparatorMediatorPricing

Abstract

All separator branches are certified and reassembled into the original complete-mediator optimization.

M is finite with decidable equality. coupling is a normalized rational mediator-pair law; K is a Finset M. Branch variables range over the whole function type K to Bool. multiplier and probability map M to Q; threshold is rational. law and candidate are original FiniteResponseLaw values on M to Bool. Structure-field applications refer to the displayed raw certificate fields.

Definition 1.1 (A total family of branch certificates).

Lean statement: D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.SeparatorPricingCertificate

Formalization. D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.SeparatorPricingCertificate (✓ std3).

Source. Repository-derived.

Commentary.

The raw fields are color : M to Bool; flows : (K to Bool) to STCutCertificate M; winner : K to Bool. The total function covers all 2^card(K) assignments. There is no proof-valued field and no producer-selected branch sublist.

Definition 1.2 (Price one branch in original units).

$$\forall M,coupling,K,multiplier,certificate,branch,(\mathrm{branchValue}(coupling,K,multiplier,certificate,branch))=((\mathrm{branchOffset}(coupling,K,branch,multiplier))+(\mathrm{certifiedPricingValue}(\mathrm{residualCoupling}(coupling,K),\mathrm{color}(certificate),\mathrm{branchMultiplier}(coupling,K,branch,multiplier),\mathrm{flows}(certificate,branch))))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.branchValue (✓ std3).

Source. Repository-derived.

Commentary.

The value includes the original fixed-coordinate offset and the checked residual price.

Definition 1.3 (Check all branches and the proposed winner).

$$\forall M,coupling,K,multiplier,certificate,(\mathrm{checkSeparatorPricing}(coupling,K,multiplier,certificate))=(\mathrm{decide}((\forall branch,(\mathrm{checkBipartitePricing}(\mathrm{residualCoupling}(coupling,K),\mathrm{color}(certificate),\mathrm{branchMultiplier}(coupling,K,branch,multiplier),\mathrm{flows}(certificate,branch)))=(true))\wedge (\forall branch,(\mathrm{branchValue}(coupling,K,multiplier,certificate,branch))\le (\mathrm{branchValue}(coupling,K,multiplier,certificate,\mathrm{winner}(certificate))))))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.checkSeparatorPricing (✓ std3).

Source. Repository-derived.

Commentary.

Both universal tests range over every function from K to Bool, including the unique assignment for empty K. Every branch uses the actual residual coupling and corrected multipliers.

Definition 1.4 (Lift the winning cut to a causal response).

$$\forall M,K,certificate,(\mathrm{winningTable}(K,certificate))=(\mathrm{clampTable}(K,\mathrm{winner}(certificate),\mathrm{flipTable}(\mathrm{color}(certificate),\mathrm{side}(\mathrm{flows}(certificate,\mathrm{winner}(certificate))))))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.winningTable (✓ std3).

Source. Repository-derived.

Commentary.

The selected coordinates are restored after undoing the residual graph coloring. The result lies in the original full response-table carrier.

Theorem 1.5 (An attained global maximum over all original columns).

$$\forall M,coupling,K,multiplier,certificate,((\mathrm{checkSeparatorPricing}(coupling,K,multiplier,certificate))=(true))\Rightarrow (((\mathrm{completeMediatorPricingScore}(coupling,multiplier,\mathrm{winningTable}(K,certificate)))=(\mathrm{branchValue}(coupling,K,multiplier,certificate,\mathrm{winner}(certificate))))\wedge (\mathrm{IsGreatest}(\mathrm{range}(\mathrm{completeMediatorPricingScore}(coupling,multiplier)),\mathrm{branchValue}(coupling,K,multiplier,certificate,\mathrm{winner}(certificate)))))$$

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

Source. Repository-derived.

Commentary.

Each competitor is assigned to its own restriction on K. Its certified branch maximum is bounded by the proposed winner, so no unvisited original column can exceed the returned value.

Theorem 1.6 (Exact full-family stopping test).

$$\forall M,coupling,K,multiplier,certificate,threshold,((\mathrm{checkSeparatorPricing}(coupling,K,multiplier,certificate))=(true))\Rightarrow ((\forall table,(\mathrm{completeMediatorPricingScore}(coupling,multiplier,table))\le (threshold))\iff ((\mathrm{branchValue}(coupling,K,multiplier,certificate,\mathrm{winner}(certificate)))\le (threshold)))$$

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

Source. Repository-derived.

Commentary.

The normalization multiplier is compared to the certified maximum over all complete response columns, not only generated columns.

Theorem 1.7 (Bound every law with the original marginal rows).

$$\forall M,coupling,K,multiplier,probability,certificate,law,(((\mathrm{checkSeparatorPricing}(coupling,K,multiplier,certificate))=(true))\wedge (\forall i,(\mathrm{linearObjective}(\lambda table,\mathrm{ite}(\mathrm{table}(i),1,0),\mathrm{mass}(law)))=(\mathrm{probability}(i))))\Rightarrow ((\mathrm{completeMediatorBenefit}(coupling,law))\le ((\mathrm{branchValue}(coupling,K,multiplier,certificate,\mathrm{winner}(certificate)))+(\sum _i((\mathrm{multiplier}(i))\cdot (\mathrm{probability}(i))))))$$

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

Source. Repository-derived.

Commentary.

The existing expectation/dual bound is reused on the original coupling. This bound is valid before restricted-master optimality and does not require fair outcome marginals.

Theorem 1.8 (Certify the original sharp upper endpoint).

$$\forall M,coupling,K,multiplier,probability,certificate,threshold,candidate,(((\mathrm{checkSeparatorPricing}(coupling,K,multiplier,certificate))=(true))\wedge ((\mathrm{branchValue}(coupling,K,multiplier,certificate,\mathrm{winner}(certificate)))\le (threshold))\wedge (\forall i,(\mathrm{linearObjective}(\lambda table,\mathrm{ite}(\mathrm{table}(i),1,0),\mathrm{mass}(candidate)))=(\mathrm{probability}(i)))\wedge ((\mathrm{completeMediatorBenefit}(coupling,candidate))=((threshold)+(\sum _i((\mathrm{multiplier}(i))\cdot (\mathrm{probability}(i)))))))\Rightarrow (\mathrm{IsGreatest}(\mathrm{setOf}(\lambda value,\exists law,(\forall i,(\mathrm{linearObjective}(\lambda table,\mathrm{ite}(\mathrm{table}(i),1,0),\mathrm{mass}(law)))=(\mathrm{probability}(i)))\wedge ((\mathrm{completeMediatorBenefit}(coupling,law))=(value))),\mathrm{completeMediatorBenefit}(coupling,candidate)))$$

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

Source. Repository-derived.

Commentary.

An actual normalized nonnegative candidate law, all original marginal rows, exact primal/dual equality and the checked global stop certify the full endpoint. The original mediator coupling stays fixed.

References

• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.SeparatorPricingCertificate
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.branchValue
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.checkSeparatorPricing
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.checkSeparatorPricing_sound
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.checked_separator_causal_bound
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.checked_separator_master_isGreatest
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.checked_separator_stopping_iff
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SeparatorMediatorPricing.winningTable
• Dependency: D5/S3/ConceptDynamics/CausalMoments/MediatorPricingRestriction