BipartiteMediatorPricing

Abstract

Actual complete-mediator pricing is reduced to a checked minimum cut, and the same certificate closes the full outcome-marginal master problem.

Mediator is an arbitrary finite type with decidable equality. coupling is the existing normalized rational law on Mediator times Mediator. color and table map Mediator to Bool; multiplier and probability map Mediator to Q; law and candidate are existing FiniteResponseLaw values on complete Boolean tables. certificate is the existing STCutCertificate. All formula quantifiers carry these types; finite sums cover every indicated carrier. The selected graph condition concerns the off-diagonal support of coupling.

Definition 1.1 (Color the actual off-diagonal support).

$\forall M e d ia t or, co u pl in g, co l or, (OffDiagonalBipartite (co u pl in g, co l or)) \Leftrightarrow (\forall i, j, (((i) \neq = (j)) \land ((mass (co u pl in g, pair (i, j))) \neq = (0))) \Rightarrow ((color (i)) \neq = (color (j))))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.OffDiagonalBipartite (✓ std3).

Source. Repository-derived.

Commentary.

The graph is the cross-world mediator coupling support, not the causal DAG. Diagonal mass is allowed.

Definition 1.2 (A bijective color-class flip).

$\forall M e d ia t or, co l or, t ab l e, i, (flipTable (co l or, t ab l e, i)) = (ite (color (i), not (table (i)), table (i)))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.flipTable (✓ std3).

Source. Repository-derived.

Commentary.

Each complete table remains an actual response table after the deterministic flip.

Theorem 1.3 (Recover every original column).

$\forall M e d ia t or, co l or, t ab l e, (flipTable (co l or, flipTable (co l or, t ab l e))) = (t ab l e)$

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

Source. Repository-derived.

Commentary.

The involution ensures the cut optimization covers all original columns.

Definition 1.4 (Remove harmless loop mass).

$\forall M e d ia t or, co u pl in g, (offDiagonalMass (co u pl in g)) = (p ai r \sum (ite ((fst (p ai r)) \neq = (snd (p ai r)), mass (co u pl in g, p ai r), 0)))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.offDiagonalMass (✓ std3).

Source. Repository-derived.

Commentary.

Loops never generate benefit and must not be included in the constant cut offset.

Definition 1.5 (Retain the full vertex field).

$\forall M e d ia t or, co u pl in g, m u lt i pl i er, i, (pricingField (co u pl in g, m u lt i pl i er, i)) = (((rightResponseMarginal (mass (co u pl in g), i)) - (leftResponseMarginal (mass (co u pl in g), i))) - ((2) \cdot (multiplier (i))))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.pricingField (✓ std3).

Source. Repository-derived.

Commentary.

This is the actual field in the previously proved pricing identity, with no stationarity assumption.

Definition 1.6 (Signed field after the flip).

$\forall M e d ia t or, co u pl in g, co l or, m u lt i pl i er, i, (switchedField (co u pl in g, co l or, m u lt i pl i er, i)) = (ite (color (i), (0) - (pricingField (co u pl in g, m u lt i pl i er, i)), pricingField (co u pl in g, m u lt i pl i er, i)))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.switchedField (✓ std3).

Source. Repository-derived.

Commentary.

The color class changes the sign of its vertex field.

Definition 1.7 (Nonnegative internal capacities).

$\forall M e d ia t or, co u pl in g, i, j, (pricingCapacity (co u pl in g, i, j)) = ((mass (co u pl in g, pair (i, j))) + (mass (co u pl in g, pair (j, i))))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.pricingCapacity (✓ std3).

Source. Repository-derived.

Commentary.

Both directions are retained. Each actual cut counts only the direction crossing from true to false.

Definition 1.8 (Source terminal capacity).

$\forall M e d ia t or, co u pl in g, co l or, m u lt i pl i er, i, (pricingSourceCapacity (co u pl in g, co l or, m u lt i pl i er, i)) = (max (0, switchedField (co u pl in g, co l or, m u lt i pl i er, i)))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.pricingSourceCapacity (✓ std3).

Source. Repository-derived.

Commentary.

The positive switched field penalizes placement on the sink side.

Definition 1.9 (Sink terminal capacity).

$\forall M e d ia t or, co u pl in g, co l or, m u lt i pl i er, i, (pricingSinkCapacity (co u pl in g, co l or, m u lt i pl i er, i)) = (max (0, (0) - (switchedField (co u pl in g, co l or, m u lt i pl i er, i))))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.pricingSinkCapacity (✓ std3).

Source. Repository-derived.

Commentary.

The negative switched field penalizes placement on the source side.

Definition 1.10 (All additive constants).

$\forall M e d ia t or, co u pl in g, co l or, m u lt i pl i er, (pricingOffset (co u pl in g, co l or, m u lt i pl i er)) = (((offDiagonalMass (co u pl in g)) + (i \sum (ite (color (i), pricingField (co u pl in g, m u lt i pl i er, i), 0)))) + (i \sum (pricingSourceCapacity (co u pl in g, co l or, m u lt i pl i er, i))))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.pricingOffset (✓ std3).

Source. Repository-derived.

Commentary.

Retaining these constants is essential to compute the original reduced cost, including its factor of two.

Theorem 1.11 (Original pricing equals offset minus cut).

$\forall M e d ia t or, co u pl in g, co l or, t ab l e, m u lt i pl i er, (OffDiagonalBipartite (co u pl in g, co l or)) \Rightarrow (((2) \cdot (completeMediatorPricingScore (co u pl in g, m u lt i pl i er, flipTable (co l or, t ab l e)))) = ((pricingOffset (co u pl in g, co l or, m u lt i pl i er)) - (stCutValue (pricingCapacity (co u pl in g), pricingSourceCapacity (co u pl in g, co l or, m u lt i pl i er), pricingSinkCapacity (co u pl in g, co l or, m u lt i pl i er), t ab l e))))$

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

Source. Repository-derived.

Commentary.

The equality holds on every complete table. It retains asymmetric mediator masses, arbitrary dual multipliers and loop handling.

Definition 1.12 (Check the graph contract and optimal flow).

$\forall M e d ia t or, co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e, (checkBipartitePricing (co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e)) = (and (decide (OffDiagonalBipartite (co u pl in g, co l or)), checkSTCutCertificate (pricingCapacity (co u pl in g), pricingSourceCapacity (co u pl in g, co l or, m u lt i pl i er), pricingSinkCapacity (co u pl in g, co l or, m u lt i pl i er), cer t i f i c a t e)))$

Formalization. D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.checkBipartitePricing (✓ std3).

Source. Repository-derived.

Commentary.

Both tests are on the actual input; a claimed bipartite shape or solver optimality status is insufficient.

Definition 1.13 (Return to the original scale).

$\forall M e d ia t or, co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e, (certifiedPricingValue (co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e)) = (\frac{( pricingOffset ( co u pl in g , co l or , m u lt i pl i er )) - ( flowValue ( cer t i f i c a t e ))}{2})$

Formalization. D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.certifiedPricingValue (✓ std3).

Source. Repository-derived.

Commentary.

The value is recomputed from the checked flow and the original coefficient offset.

Theorem 1.14 (A real column and a global maximum).

$\forall M e d ia t or, co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e, ((checkBipartitePricing (co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e)) = (t r u e)) \Rightarrow (((completeMediatorPricingScore (co u pl in g, m u lt i pl i er, flipTable (co l or, side (cer t i f i c a t e)))) = (certifiedPricingValue (co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e))) \land (IsGreatest (range (completeMediatorPricingScore (co u pl in g, m u lt i pl i er)), certifiedPricingValue (co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e))))$

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

Source. Repository-derived.

Commentary.

The flipped cut realizes the global price bound. The conclusion covers every Boolean column, without enumerating them in the checker.

Theorem 1.15 (Exact stopping criterion).

$\forall M e d ia t or, co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e, n or ma l i z a t i o n M u lt i pl i er, ((checkBipartitePricing (co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e)) = (t r u e)) \Rightarrow ((\forall t ab l e, (completeMediatorPricingScore (co u pl in g, m u lt i pl i er, t ab l e)) \leq (n or ma l i z a t i o n M u lt i pl i er)) \Leftrightarrow ((certifiedPricingValue (co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e)) \leq (n or ma l i z a t i o n M u lt i pl i er)))$

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

Source. Repository-derived.

Commentary.

This is the full no-positive-reduced-cost condition, not a test only on already generated columns.

Theorem 1.16 (Rejoin the original causal objective).

$\forall M e d ia t or, co u pl in g, m u lt i pl i er, l a w, (completeMediatorBenefit (co u pl in g, l a w)) = ((linearObjective (completeMediatorPricingScore (co u pl in g, m u lt i pl i er), mass (l a w))) + (i \sum ((multiplier (i)) \cdot (linearObjective (λ t ab l e, ite (apply (t ab l e, i), 1, 0), mass (l a w))))))$

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

Source. Repository-derived.

Commentary.

This expectation identity holds on any fixed coupling, with no bipartite or fair-marginal premise.

Theorem 1.17 (Bound every canonical outcome law).

$\forall M e d ia t or, co u pl in g, m u lt i pl i er, p ro babi l i t y, b o u n d, l a w, ((\forall t ab l e, (completeMediatorPricingScore (co u pl in g, m u lt i pl i er, t ab l e)) \leq (b o u n d)) \land (\forall i, (linearObjective (λ t ab l e, ite (apply (t ab l e, i), 1, 0), mass (l a w))) = (probability (i)))) \Rightarrow ((completeMediatorBenefit (co u pl in g, l a w)) \leq ((b o u n d) + (i \sum ((multiplier (i)) \cdot (probability (i))))))$

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

Source. Repository-derived.

Commentary.

Normalization and the original marginal rows transport the global column bound to a causal upper bound.

Theorem 1.18 (Certify the full sharp endpoint).

$\forall M e d ia t or, co u pl in g, co l or, m u lt i pl i er, p ro babi l i t y, n or ma l i z a t i o n M u lt i pl i er, cer t i f i c a t e, c an d i d a t e, (((checkBipartitePricing (co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e)) = (t r u e)) \land ((certifiedPricingValue (co u pl in g, co l or, m u lt i pl i er, cer t i f i c a t e)) \leq (n or ma l i z a t i o n M u lt i pl i er)) \land (\forall i, (linearObjective (λ t ab l e, ite (apply (t ab l e, i), 1, 0), mass (c an d i d a t e))) = (probability (i))) \land ((completeMediatorBenefit (co u pl in g, c an d i d a t e)) = ((n or ma l i z a t i o n M u lt i pl i er) + (i \sum ((multiplier (i)) \cdot (probability (i))))))) \Rightarrow (IsGreatest (setOf (λ v a l u e, \exists l a w, (\forall i, (linearObjective (λ t ab l e, ite (apply (t ab l e, i), 1, 0), mass (l a w))) = (probability (i))) \land ((completeMediatorBenefit (co u pl in g, l a w)) = (v a l u e))), completeMediatorBenefit (co u pl in g, c an d i d a t e)))$

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

Source. Repository-derived.

Commentary.

A feasible restricted-master candidate with exact primal/dual equality becomes an attaining law for the full canonical problem when the global pricing check passes. The mediator coupling is fixed throughout.

References

Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.OffDiagonalBipartite
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.certifiedPricingValue
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.checkBipartitePricing
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.checked_no_improving_column_iff
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.checked_pricing_isGreatest
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.checked_restricted_master_isGreatest
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.completeMediatorBenefit_eq_pricing_expectation
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.flipTable
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.flipTable_involutive
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.offDiagonalMass
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.pricingCapacity
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.pricingField
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.pricingOffset
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.pricingSinkCapacity
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.pricingSourceCapacity
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.pricing_bound_implies_causal_bound
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.pricing_cut_identity
Truth anchor: D5/S3/ConceptDynamics/CausalMoments/BipartiteMediatorPricing.switchedField
Dependency: D5/S0/Certificates/RationalSTCutCertificate
Dependency: D5/S3/ConceptDynamics/CausalMoments/CompleteMediatorCutSharpBounds

Keyboard shortcuts

trureturing Blueprint

BipartiteMediatorPricing

Abstract

References