Step-kernel cost transport across the countable-factor lift

Step 4 of the step-approximation programme (#107 remains open).

• cutNormDiff_pullback_prod_factor — exact cost transport: the coupling cost of two pulled-back step kernels under any coupling that pushes to the factor law equals the quotient step-kernel cost under the factor law itself. Pure composition: pullback functoriality rewrites both costs as pullbacks along the factor-pair map, and the cross-carrier cut-norm isometry (cutNormDiff_pullback_eq_measurePreserving) collapses that map.
• measurePreserving_prodMap_countableFactorLift and the fst/snd companions — the step-3 exact-pushforward theorems packaged as MeasurePreserving witnesses for the lift.
• cutNormDiff_pullback_countableFactorLift — the cost transport instantiated at the countable-factor lift: quotient step-kernel cost under lam equals pulled-back step-kernel cost under countableFactorLift lam, exactly. The probability instance on the lift is a binder discharged by isProbabilityMeasure_countableFactorLift.
• abs_cutNormDiff_pullback_sub_stepCost_le — the approximation bound step 5 consumes: the coupling cost of two graphons differs from the quotient step-kernel cost by at most the sum of the two carrier-side step-approximation errors.

Deliberately not here: existence of step approximations, finite coupling gluing, and the triangle assembly — later units of the programme.

theorem Graphon.cutNormDiff_pullback_prod_factor {γ₁ : Type u_1} {γ₂ : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₁] [MeasurableSpace γ₂] [MeasurableSpace ι₁] [MeasurableSpace ι₂] {μ₁ : MeasureTheory.Measure γ₁} {μ₂ : MeasureTheory.Measure γ₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {ν₁ : MeasureTheory.Measure ι₁} {ν₂ : MeasureTheory.Measure ι₂} [MeasureTheory.IsProbabilityMeasure ν₁] [MeasureTheory.IsProbabilityMeasure ν₂] {q₁ : γ₁ → ι₁} {q₂ : γ₂ → ι₂} {lam : MeasureTheory.Measure (ι₁ × ι₂)} [MeasureTheory.IsProbabilityMeasure lam] (π : MeasureTheory.Measure (γ₁ × γ₂)) [MeasureTheory.IsProbabilityMeasure π] (K₁ : Graphon ι₁ ν₁) (K₂ : Graphon ι₂ ν₂) (hq₁mp : MeasureTheory.MeasurePreserving q₁ μ₁ ν₁) (hq₂mp : MeasureTheory.MeasurePreserving q₂ μ₂ ν₂) (hΦ : MeasureTheory.MeasurePreserving (Prod.map q₁ q₂) π lam) (hfstπ : MeasureTheory.MeasurePreserving Prod.fst π μ₁) (hsndπ : MeasureTheory.MeasurePreserving Prod.snd π μ₂) (hfstlam : MeasureTheory.MeasurePreserving Prod.fst lam ν₁) (hsndlam : MeasureTheory.MeasurePreserving Prod.snd lam ν₂) : ((K₁.pullback q₁ hq₁mp).pullback Prod.fst hfstπ).cutNormDiff ((K₂.pullback q₂ hq₂mp).pullback Prod.snd hsndπ) = (K₁.pullback Prod.fst hfstlam).cutNormDiff (K₂.pullback Prod.snd hsndlam)

Exact cost transport: for any coupling π of the carriers that pushes to the factor law lam under the factor-pair map, the coupling cost of the pulled-back step kernels under π equals the quotient step-kernel cost under lam — an equality, not an estimate.

theorem Graphon.measurePreserving_prodMap_countableFactorLift {γ₁ : Type u_1} {γ₂ : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₁] [MeasurableSpace γ₂] [MeasurableSpace ι₁] [MeasurableSpace ι₂] {μ₁ : MeasureTheory.Measure γ₁} {μ₂ : MeasureTheory.Measure γ₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {ν₁ : MeasureTheory.Measure ι₁} {ν₂ : MeasureTheory.Measure ι₂} {q₁ : γ₁ → ι₁} {q₂ : γ₂ → ι₂} {lam : MeasureTheory.Measure (ι₁ × ι₂)} [Countable ι₁] [MeasurableSingletonClass ι₁] [Countable ι₂] [MeasurableSingletonClass ι₂] (hq₁mp : MeasureTheory.MeasurePreserving q₁ μ₁ ν₁) (hq₂mp : MeasureTheory.MeasurePreserving q₂ μ₂ ν₂) (hfst : MeasureTheory.Measure.map Prod.fst lam = ν₁) (hsnd : MeasureTheory.Measure.map Prod.snd lam = ν₂) : MeasureTheory.MeasurePreserving (Prod.map q₁ q₂) (MeasureTheory.countableFactorLift μ₁ μ₂ q₁ q₂ lam) lam

The factor-pair map is measure-preserving from the countable-factor lift to the factor law — the step-3 round-trip packaged as a MeasurePreserving witness.

theorem Graphon.measurePreserving_fst_countableFactorLift {γ₁ : Type u_1} {γ₂ : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₁] [MeasurableSpace γ₂] [MeasurableSpace ι₁] [MeasurableSpace ι₂] {μ₁ : MeasureTheory.Measure γ₁} {μ₂ : MeasureTheory.Measure γ₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {ν₁ : MeasureTheory.Measure ι₁} {ν₂ : MeasureTheory.Measure ι₂} {q₁ : γ₁ → ι₁} {q₂ : γ₂ → ι₂} {lam : MeasureTheory.Measure (ι₁ × ι₂)} [Countable ι₁] [MeasurableSingletonClass ι₁] [Countable ι₂] [MeasurableSingletonClass ι₂] (hq₁mp : MeasureTheory.MeasurePreserving q₁ μ₁ ν₁) (hq₂mp : MeasureTheory.MeasurePreserving q₂ μ₂ ν₂) (hfst : MeasureTheory.Measure.map Prod.fst lam = ν₁) (hsnd : MeasureTheory.Measure.map Prod.snd lam = ν₂) : MeasureTheory.MeasurePreserving Prod.fst (MeasureTheory.countableFactorLift μ₁ μ₂ q₁ q₂ lam) μ₁

The first projection is measure-preserving from the countable-factor lift to the first carrier — the step-3 exact first marginal packaged as a MeasurePreserving witness.

theorem Graphon.measurePreserving_snd_countableFactorLift {γ₁ : Type u_1} {γ₂ : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₁] [MeasurableSpace γ₂] [MeasurableSpace ι₁] [MeasurableSpace ι₂] {μ₁ : MeasureTheory.Measure γ₁} {μ₂ : MeasureTheory.Measure γ₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {ν₁ : MeasureTheory.Measure ι₁} {ν₂ : MeasureTheory.Measure ι₂} {q₁ : γ₁ → ι₁} {q₂ : γ₂ → ι₂} {lam : MeasureTheory.Measure (ι₁ × ι₂)} [Countable ι₁] [MeasurableSingletonClass ι₁] [Countable ι₂] [MeasurableSingletonClass ι₂] (hq₁mp : MeasureTheory.MeasurePreserving q₁ μ₁ ν₁) (hq₂mp : MeasureTheory.MeasurePreserving q₂ μ₂ ν₂) (hfst : MeasureTheory.Measure.map Prod.fst lam = ν₁) (hsnd : MeasureTheory.Measure.map Prod.snd lam = ν₂) : MeasureTheory.MeasurePreserving Prod.snd (MeasureTheory.countableFactorLift μ₁ μ₂ q₁ q₂ lam) μ₂

The second projection is measure-preserving from the countable-factor lift to the second carrier — the step-3 exact second marginal packaged as a MeasurePreserving witness.

theorem Graphon.cutNormDiff_pullback_countableFactorLift {γ₁ : Type u_1} {γ₂ : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₁] [MeasurableSpace γ₂] [MeasurableSpace ι₁] [MeasurableSpace ι₂] {μ₁ : MeasureTheory.Measure γ₁} {μ₂ : MeasureTheory.Measure γ₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {ν₁ : MeasureTheory.Measure ι₁} {ν₂ : MeasureTheory.Measure ι₂} [MeasureTheory.IsProbabilityMeasure ν₁] [MeasureTheory.IsProbabilityMeasure ν₂] {q₁ : γ₁ → ι₁} {q₂ : γ₂ → ι₂} {lam : MeasureTheory.Measure (ι₁ × ι₂)} [MeasureTheory.IsProbabilityMeasure lam] [Countable ι₁] [MeasurableSingletonClass ι₁] [Countable ι₂] [MeasurableSingletonClass ι₂] [MeasureTheory.IsProbabilityMeasure (MeasureTheory.countableFactorLift μ₁ μ₂ q₁ q₂ lam)] (K₁ : Graphon ι₁ ν₁) (K₂ : Graphon ι₂ ν₂) (hq₁mp : MeasureTheory.MeasurePreserving q₁ μ₁ ν₁) (hq₂mp : MeasureTheory.MeasurePreserving q₂ μ₂ ν₂) (hfst : MeasureTheory.Measure.map Prod.fst lam = ν₁) (hsnd : MeasureTheory.Measure.map Prod.snd lam = ν₂) : ((K₁.pullback q₁ hq₁mp).pullback Prod.fst ⋯).cutNormDiff ((K₂.pullback q₂ hq₂mp).pullback Prod.snd ⋯) = (K₁.pullback Prod.fst ⋯).cutNormDiff (K₂.pullback Prod.snd ⋯)

Cost transport at the countable-factor lift: the quotient step-kernel cost under the factor law lam equals the pulled-back step-kernel cost under countableFactorLift lam, exactly. The probability instance on the lift is discharged by isProbabilityMeasure_countableFactorLift.

theorem Graphon.abs_cutNormDiff_pullback_sub_stepCost_le {γ₁ : Type u_1} {γ₂ : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₁] [MeasurableSpace γ₂] [MeasurableSpace ι₁] [MeasurableSpace ι₂] {μ₁ : MeasureTheory.Measure γ₁} {μ₂ : MeasureTheory.Measure γ₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {ν₁ : MeasureTheory.Measure ι₁} {ν₂ : MeasureTheory.Measure ι₂} [MeasureTheory.IsProbabilityMeasure ν₁] [MeasureTheory.IsProbabilityMeasure ν₂] {q₁ : γ₁ → ι₁} {q₂ : γ₂ → ι₂} {lam : MeasureTheory.Measure (ι₁ × ι₂)} [MeasureTheory.IsProbabilityMeasure lam] (π : MeasureTheory.Measure (γ₁ × γ₂)) [MeasureTheory.IsProbabilityMeasure π] (U₁ : Graphon γ₁ μ₁) (U₂ : Graphon γ₂ μ₂) (K₁ : Graphon ι₁ ν₁) (K₂ : Graphon ι₂ ν₂) (hq₁mp : MeasureTheory.MeasurePreserving q₁ μ₁ ν₁) (hq₂mp : MeasureTheory.MeasurePreserving q₂ μ₂ ν₂) (hΦ : MeasureTheory.MeasurePreserving (Prod.map q₁ q₂) π lam) (hfstπ : MeasureTheory.MeasurePreserving Prod.fst π μ₁) (hsndπ : MeasureTheory.MeasurePreserving Prod.snd π μ₂) (hfstlam : MeasureTheory.MeasurePreserving Prod.fst lam ν₁) (hsndlam : MeasureTheory.MeasurePreserving Prod.snd lam ν₂) : |(U₁.pullback Prod.fst hfstπ).cutNormDiff (U₂.pullback Prod.snd hsndπ) - (K₁.pullback Prod.fst hfstlam).cutNormDiff (K₂.pullback Prod.snd hsndlam)| ≤ U₁.cutNormDiff (K₁.pullback q₁ hq₁mp) + U₂.cutNormDiff (K₂.pullback q₂ hq₂mp)

The approximation bound step 5 consumes: under any coupling π pushing to the factor law, the coupling cost of two graphons differs from the quotient step-kernel cost under the factor law by at most the sum of the two carrier-side step-approximation errors. Lipschitz stability replaces each graphon by its pulled-back step kernel; exact cost transport replaces the resulting cost by the quotient cost.