Repairing a distinguished coordinate while preserving the factored law

The checked correlated marginal-replacement construction applies to each already normalized right kernel, including kernels under zero-mass transcripts. Exact distance averages then recover the global retained coordinate discrepancy with the unchanged left kernel.

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

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