Simultaneous response-cell attainment

Abstract

One complete outcome mechanism attains every pairwise upper cell at once; another attains every lower cell. This is the constructive prerequisite for an exact mediator transport reduction.

Mediator is any finite type with decidable equality. Complete outcome tables have type Bool times Mediator to Bool. Both interventions evaluate the same table. The notation thresholdOutcomeLaw includes its positive-denominator proof argument hN. All probabilities and expectations are rational.

Definition 1.1 (One finite disturbance).

$$\forall N,hN,u,(\mathrm{mass}(\mathrm{uniformThresholdLaw}(N,hN),u))=(\frac{1}{N})$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.uniformThresholdLaw (✓ std3).

Source. Repository-derived.

Commentary.

N is a natural number, hN proves N is positive, and u ranges over Fin N. The defining structure proves nonnegativity and normalization.

Theorem 1.2 (Exact prefix probability).

$$\forall N,K,hN,hK,(\mathrm{linearObjective}(\mathrm{prefixIndicator}(K),\mathrm{mass}(\mathrm{uniformThresholdLaw}(N,hN))))=(\frac{K}{N})$$

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

Source. Repository-derived.

Commentary.

hN proves 0<N and hK proves K<=N. prefixIndicator(K)(u) is one exactly when the natural value of u is smaller than K. The proof counts this entire prefix, not a sample.

Definition 1.3 (Actual success expectation).

$$\forall law,a,m,(\mathrm{outcomeSuccess}(law,a,m))=(\mathrm{linearObjective}(\mathrm{successIndicator}(a,m),\mathrm{mass}(law)))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.outcomeSuccess (✓ std3).

Source. Repository-derived.

Commentary.

successIndicator(a,m)(table) is one exactly when table(a,m) is true. law is a normalized FiniteResponseLaw on complete outcome tables.

Definition 1.4 (A cross-world benefit cell).

$$\forall law,m0,m1,(\mathrm{outcomeBenefitCell}(law,m0,m1))=(\mathrm{linearObjective}(\mathrm{benefitIndicator}(m0,m1),\mathrm{mass}(law)))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.outcomeBenefitCell (✓ std3).

Source. Repository-derived.

Commentary.

benefitIndicator(m0,m1)(table) is one exactly when table(false,m0) is false and table(true,m1) is true. This uses two entries of one table law.

Definition 1.5 (Two explicit shared-threshold mechanisms).

Lean statement: D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.thresholdOutcomeLaw

Formalization. D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.thresholdOutcomeLaw (✓ std3).

Source. Repository-derived.

Commentary.

Push uniformThresholdLaw through the complete table readout. The lower witness reads u<count(a,m) in both worlds. The upper witness reads the complement of u<N-count(false,m) in the control world and u<count(true,m) in the treated world. The flag chooses a witness, not an assumption on every admissible outcome mechanism.

Theorem 1.6 (Both mechanisms match all success rows).

$$\forall N,hN,count,upper,a,m,(((0)<(N))\wedge (\forall index,(\mathrm{count}(index))\le (N)))\Rightarrow ((\mathrm{outcomeSuccess}(\mathrm{thresholdOutcomeLaw}(N,hN,count,upper),a,m))=(\frac{\mathrm{count}((a,m))}{N}))$$

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

Source. Repository-derived.

Commentary.

The statement holds for every mediator value and either witness flag, including probability zero and one.

Theorem 1.7 (All upper cells from one law).

$$\forall N,hN,count,m0,m1,(((0)<(N))\wedge (\forall index,(\mathrm{count}(index))\le (N)))\Rightarrow ((\mathrm{outcomeBenefitCell}(\mathrm{thresholdOutcomeLaw}(N,hN,count,true),m0,m1))=(\min ((1)-(\frac{\mathrm{count}((false,m0))}{N}),\frac{\mathrm{count}((true,m1))}{N})))$$

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

Source. Repository-derived.

Commentary.

The two favourable threshold events are nested prefixes of the same disturbance. Their intersection has the smaller mass, simultaneously for every m0,m1.

Theorem 1.8 (All lower cells from one law).

$$\forall N,hN,count,m0,m1,(((0)<(N))\wedge (\forall index,(\mathrm{count}(index))\le (N)))\Rightarrow ((\mathrm{outcomeBenefitCell}(\mathrm{thresholdOutcomeLaw}(N,hN,count,false),m0,m1))=(\max (0,(\frac{\mathrm{count}((true,m1))}{N})-(\frac{\mathrm{count}((false,m0))}{N}))))$$

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

Source. Repository-derived.

Commentary.

Subtracting the common-prefix intersection computes every lower cell. No independent disturbance is introduced per mediator pair.

Theorem 1.9 (Bounds for every complete outcome mechanism).

$$\forall law,m0,m1,((\max (0,(\mathrm{outcomeSuccess}(law,true,m1))-(\mathrm{outcomeSuccess}(law,false,m0))))\le (\mathrm{outcomeBenefitCell}(law,m0,m1)))\wedge ((\mathrm{outcomeBenefitCell}(law,m0,m1))\le (\min ((1)-(\mathrm{outcomeSuccess}(law,false,m0)),\mathrm{outcomeSuccess}(law,true,m1))))$$

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

Source. Repository-derived.

Commentary.

Only nonnegative normalization and the actual Boolean response entries are used for necessity.

Theorem 1.10 (All finite rational kernels have simultaneous endpoint mechanisms).

$$\forall probability,(\forall index,((0)\le (\mathrm{probability}(index)))\wedge ((\mathrm{probability}(index))\le (1)))\Rightarrow (\exists lower,upper,(\forall a,m,(\mathrm{outcomeSuccess}(lower,a,m))=(\mathrm{probability}((a,m))))\wedge (\forall a,m,(\mathrm{outcomeSuccess}(upper,a,m))=(\mathrm{probability}((a,m))))\wedge (\forall m0,m1,(\mathrm{outcomeBenefitCell}(lower,m0,m1))=(\max (0,(\mathrm{probability}((true,m1)))-(\mathrm{probability}((false,m0))))))\wedge (\forall m0,m1,(\mathrm{outcomeBenefitCell}(upper,m0,m1))=(\min ((1)-(\mathrm{probability}((false,m0))),\mathrm{probability}((true,m1))))))$$

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

Source. Repository-derived.

Commentary.

The proof first derives a common positive denominator for the entire finite rational kernel. It then constructs the two actual finite laws. The existential laws precede the universal mediator-pair quantifiers.

References

• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.outcomeBenefitCell
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.outcomeBenefitCell_bounds
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.outcomeSuccess
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.simultaneous_frechet_outcome_laws
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.thresholdOutcomeLaw
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.thresholdOutcomeLaw_lower_cells
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.thresholdOutcomeLaw_success
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.thresholdOutcomeLaw_upper_cells
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.uniformThresholdLaw
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/SharedThresholdResponseCoupling.uniformThreshold_prefix
• Dependency: D5/S3/ConceptDynamics/CausalMoments/FiniteMomentSparseLaw