Repairing a left coordinate while keeping the entire original left state

Swap the latent sides to apply the checked rowwise uniform-coordinate coupling, then swap back. The original left marginal is preserved on every row, including null transcript rows. Therefore all actual prefixes and tampered coordinates, as functions of that latent variable, remain unchanged.

theorem Algebraic.Cutwidth.Extractor.Internal.smooth_factored_left_lift {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) : factoredWeight w (rightCoordinateLift l x) r = mapWeight (fun (p : (Z × B) × A) => (p.1, p.2, x p.1.1 p.2)) (factoredWeight w l r)

theorem Algebraic.Cutwidth.Extractor.Internal.smooth_factored_forget_left {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} [Fintype Z] [Fintype A] [Fintype B] [Fintype X] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (l' : Z → A × X → ℝ) (first : ∀ (z : Z), mapWeight Prod.fst (l' z) = l z) : mapWeight (fun (p : (Z × B) × A × X) => (p.1, p.2.1)) (factoredWeight w l' r) = factoredWeight w l r

theorem Algebraic.Cutwidth.Extractor.Internal.smooth_exists_uniform_left_repair {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} [Fintype Z] [Fintype A] [Fintype B] [Fintype X] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : ∃ (l' : Z → A × X → ℝ), (∀ (z : Z), IsProbabilityWeight (l' z)) ∧ (∀ (z : Z), mapWeight Prod.fst (l' z) = l z) ∧ (∀ (z : Z), mapWeight Prod.snd (l' z) = uniformWeight X) ∧ weightDist (factoredWeight w (rightCoordinateLift l x) r) (factoredWeight w l' r) ≤ weightDist (retainedSeedWeight w l x) (uniformSecondWeight (retainedSeedWeight w l x))