FiniteCouplingPushforwardLift

Abstract

Lift a coarse rational coupling to the original carriers while preserving every original marginal and every paired-readout query.

X, Y, A and B are finite types, with decidable equality on A and B. left and right are FiniteResponseLaw values on X and Y. f : X to A, g : Y to B, and joint is a law on A times B. The parameters hl and hr denote exactly the two displayed coarse-marginal equalities. The lifted result is a law on X times Y. All scalar operations are rational, including total division by zero; validity on null fibers is proved separately.

Definition 1.1 (Explicit disaggregation weights).

$$\forall X,Y,A,B,left,right,f,g,joint,x,y,(\mathrm{liftedCouplingMass}(left,right,f,g,joint,\mathrm{pair}(x,y)))=(((\mathrm{mass}(joint,\mathrm{pair}(\mathrm{apply}(f,x),\mathrm{apply}(g,y))))\cdot (\frac{\mathrm{mass}(left,x)}{\mathrm{mass}(\mathrm{pushforwardResponseLaw}(left,f),\mathrm{apply}(f,x))}))\cdot (\frac{\mathrm{mass}(right,y)}{\mathrm{mass}(\mathrm{pushforwardResponseLaw}(right,g),\mathrm{apply}(g,y))}))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/FiniteCouplingPushforwardLift.liftedCouplingMass (✓ std3).

Source. Repository-derived.

Commentary.

Each original atom receives its coarse cell mass times its two within-fiber shares. Null coarse marginals force the corresponding coarse cells to vanish.

Definition 1.2 (Normalize the original-carrier law).

$$\forall X,Y,A,B,left,right,f,g,joint,hl,hr,((\forall a,(\mathrm{leftResponseMarginal}(\mathrm{mass}(joint),a))=(\mathrm{mass}(\mathrm{pushforwardResponseLaw}(left,f),a)))\wedge (\forall b,(\mathrm{rightResponseMarginal}(\mathrm{mass}(joint),b))=(\mathrm{mass}(\mathrm{pushforwardResponseLaw}(right,g),b))))\Rightarrow ((\mathrm{mass}(\mathrm{liftCoarseCoupling}(left,right,f,g,joint,hl,hr)))=(\mathrm{liftedCouplingMass}(left,right,f,g,joint)))$$

Formalization. D5/S3/ConceptDynamics/CausalMoments/FiniteCouplingPushforwardLift.liftCoarseCoupling (✓ std3).

Source. Repository-derived.

Commentary.

The definition supplies nonnegativity and total mass one from the exact two coarse-marginal contracts, without a strict-positivity premise.

Theorem 1.3 (Preserve every original probability).

$$\forall X,Y,A,B,left,right,f,g,joint,hl,hr,((\forall a,(\mathrm{leftResponseMarginal}(\mathrm{mass}(joint),a))=(\mathrm{mass}(\mathrm{pushforwardResponseLaw}(left,f),a)))\wedge (\forall b,(\mathrm{rightResponseMarginal}(\mathrm{mass}(joint),b))=(\mathrm{mass}(\mathrm{pushforwardResponseLaw}(right,g),b))))\Rightarrow ((\forall x,(\mathrm{leftResponseMarginal}(\mathrm{mass}(\mathrm{liftCoarseCoupling}(left,right,f,g,joint,hl,hr)),x))=(\mathrm{mass}(left,x)))\wedge (\forall y,(\mathrm{rightResponseMarginal}(\mathrm{mass}(\mathrm{liftCoarseCoupling}(left,right,f,g,joint,hl,hr)),y))=(\mathrm{mass}(right,y))))$$

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

Source. Repository-derived.

Commentary.

The entire original marginal vectors are retained, including zero-probability states.

Theorem 1.4 (Preserve all paired-readout expectations).

$$\forall X,Y,A,B,left,right,f,g,joint,hl,hr,query,((\forall a,(\mathrm{leftResponseMarginal}(\mathrm{mass}(joint),a))=(\mathrm{mass}(\mathrm{pushforwardResponseLaw}(left,f),a)))\wedge (\forall b,(\mathrm{rightResponseMarginal}(\mathrm{mass}(joint),b))=(\mathrm{mass}(\mathrm{pushforwardResponseLaw}(right,g),b))))\Rightarrow ((\mathrm{linearObjective}(\lambda pair,\mathrm{apply}(query,\mathrm{pair}(\mathrm{apply}(f,\mathrm{fst}(pair)),\mathrm{apply}(g,\mathrm{snd}(pair)))),\mathrm{mass}(\mathrm{liftCoarseCoupling}(left,right,f,g,joint,hl,hr))))=(\mathrm{linearObjective}(query,\mathrm{mass}(joint))))$$

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

Source. Repository-derived.

Commentary.

query is an arbitrary rational function on A times B, chosen after the lift. Its expectation equals that under the supplied coarse coupling.

References

• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/FiniteCouplingPushforwardLift.liftCoarseCoupling
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/FiniteCouplingPushforwardLift.liftCoarseCoupling_expectation
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/FiniteCouplingPushforwardLift.liftCoarseCoupling_marginals
• Truth anchor: D5/S3/ConceptDynamics/CausalMoments/FiniteCouplingPushforwardLift.liftedCouplingMass
• Dependency: D5/S3/ConceptDynamics/CausalMoments/FiniteMomentSparseLaw