Sharp two-mechanism joint-benefit robustness

Abstract

The four intervention-marginal tolerances define a genuine bilinear comparison between two product-mechanism models. A three-corner envelope and original-carrier attaining models give its exact value.

All scalar variables are rational. The variables high and low are the existing MarkovianJointMechanismModel values: each contains two independent complete response laws on Bool times Bool. Potential outcomes within an individual law may remain dependent. The comparison is across all marginal locations, not about one fixed observed center.

Definition 1.1 (Four actual marginal comparisons).

$$\forall high,low,eta10,eta11,eta20,eta21,(\mathrm{JointMarginalTolerance}(high,low,eta10,eta11,eta20,eta21))\iff (((|(\mathrm{controlSuccessMarginal}(\mathrm{mass}(\mathrm{firstLaw}(high))))-(\mathrm{controlSuccessMarginal}(\mathrm{mass}(\mathrm{firstLaw}(low))))|)\le (eta10))\wedge (((|(\mathrm{treatmentSuccessMarginal}(\mathrm{mass}(\mathrm{firstLaw}(high))))-(\mathrm{treatmentSuccessMarginal}(\mathrm{mass}(\mathrm{firstLaw}(low))))|)\le (eta11))\wedge (((|(\mathrm{controlSuccessMarginal}(\mathrm{mass}(\mathrm{secondLaw}(high))))-(\mathrm{controlSuccessMarginal}(\mathrm{mass}(\mathrm{secondLaw}(low))))|)\le (eta20))\wedge ((|(\mathrm{treatmentSuccessMarginal}(\mathrm{mass}(\mathrm{secondLaw}(high))))-(\mathrm{treatmentSuccessMarginal}(\mathrm{mass}(\mathrm{secondLaw}(low))))|)\le (eta21)))))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/JointBenefitToleranceSharp.JointMarginalTolerance (✓ std3).

Source. Repository-derived.

Commentary.

These four inequalities concern the original response-law readouts. The product restriction is in the original model semantics, not imposed by a new joint-coupling relaxation.

Definition 1.2 (Three competing configurations).

$$\forall eta10,eta11,eta20,eta21,(\mathrm{jointBenefitAmbiguityValue}(eta10,eta11,eta20,eta21))=(\max (\max (\mathrm{benefitAmbiguityValue}(eta10,eta11),\mathrm{benefitAmbiguityValue}(eta20,eta21)),(1)-(((4)\cdot ((1)-(\mathrm{benefitAmbiguityValue}(eta10,eta11))))\cdot ((1)-(\mathrm{benefitAmbiguityValue}(eta20,eta21))))))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/JointBenefitToleranceSharp.jointBenefitAmbiguityValue (✓ std3).

Source. Repository-derived.

Commentary.

The first two candidates place ambiguity in one mechanism and hold the other at certain benefit. The third places both upper mechanisms at certain benefit and simultaneously reduces both lower benefits.

Theorem 1.3 (Global bound and attaining product models).

$$\forall eta10,eta11,eta20,eta21,(((0)\le (eta10))\wedge (((0)\le (eta11))\wedge (((0)\le (eta20))\wedge ((0)\le (eta21)))))\Rightarrow ((\forall high,low,(\mathrm{JointMarginalTolerance}(high,low,eta10,eta11,eta20,eta21))\Rightarrow ((|(\mathrm{jointMechanismBenefitMass}(\mathrm{markovianJointResponseMass}(high)))-(\mathrm{jointMechanismBenefitMass}(\mathrm{markovianJointResponseMass}(low)))|)\le (\mathrm{jointBenefitAmbiguityValue}(eta10,eta11,eta20,eta21))))\wedge (\exists high,low,(\mathrm{JointMarginalTolerance}(high,low,eta10,eta11,eta20,eta21))\wedge (((\mathrm{jointMechanismBenefitMass}(\mathrm{markovianJointResponseMass}(high)))-(\mathrm{jointMechanismBenefitMass}(\mathrm{markovianJointResponseMass}(low))))=(\mathrm{jointBenefitAmbiguityValue}(eta10,eta11,eta20,eta21)))))$$

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

Source. Repository-derived.

Commentary.

The proof first derives the endpoint-sensitive inequality 2 times the upper benefit minus 2 times the single-mechanism ambiguity is at most the lower benefit. A slice-slope argument bounds the bilinear product difference at three corners.

The first two corners reuse the existing one-mechanism sharpness theorem. The last corner uses explicitly normalized four-cell response laws. All four marginal tolerances and the actual joint-benefit query survive in the attaining pair.

This is an exact subfamily within the broader multi-component optimization research direction. It is not a complete column-generation method, a theorem for shared disturbances, or a claim of literature-wide novelty.

Theorem 1.4 (Equal-tolerance maximizing regime).

$$\forall eta10,eta11,eta20,eta21,s,(((0)\le (s))\wedge (((s)\le (1))\wedge ((((eta10)+(eta11))=(s))\wedge (((eta20)+(eta21))=(s)))))\Rightarrow ((\mathrm{jointBenefitAmbiguityValue}(eta10,eta11,eta20,eta21))=(\mathrm{ite}((s)\le (\frac{1}{2}),\frac{(1)+(s)}{2},((2)\cdot (s))-(s^2))))$$

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

Source. Repository-derived.

Commentary.

On 0 to 1, equal sums of the two within-mechanism tolerances yield (1+s)/2 through s=1/2, and 2s-s squared afterward. The algebraic formula needs the stated sum and s conditions; nonnegativity of each separate tolerance is supplied by the sharpness theorem when it is interpreted as a model guarantee.

References

• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/JointBenefitToleranceSharp.JointMarginalTolerance
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/JointBenefitToleranceSharp.equal_total_tolerance_regimes
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/JointBenefitToleranceSharp.jointBenefitAmbiguityValue
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/JointBenefitToleranceSharp.joint_benefit_marginal_tolerance_sharp
• Dependency: D5/S3/ConceptDynamics/CausalMoments/BenefitMarginalToleranceSharp
• Dependency: D5/S3/ConceptDynamics/CausalMoments/MarkovianJointMechanismBenefitSharpBounds