Uniform-coordinate repair preserving the original source factors

A distinguished deterministic coordinate of the right source can be replaced by a coordinate uniform given the transcript. The original right marginal and the entire left kernel remain unchanged. The repaired coordinate may still be correlated with the original right state.

The full factored-law distance is exactly the original retained-coordinate discrepancy. Original source envelopes are therefore preserved, including at null transcript rows. The construction uses the checked correlated marginal-replacement coupling on normalized right kernels and averages its exact distance identities; no repair witness is assumed.

Deterministic continuation pays this distance once when its retained marginal is preserved. A comparison with an unrestricted actual retained marginal explicitly pays it twice. The transfer bounds also apply to arbitrary signed weights and empty alphabets.

The coupling is credited in Strong.Weighted.Coupling. This factored specialization supplies a finite repair needed when iterating the look-ahead argument of Chattopadhyay--Goyal--Li, Lemmas 6.5 and 6.8: https://arxiv.org/pdf/1505.00107. It does not assume that approximate uniformity itself gives a pointwise source-mass cap.

theorem Algebraic.Cutwidth.Extractor.rightCoordinateLift_probability {Z : Type u_1} {B : Type u_2} {Q : Type u_3} [Fintype B] [Fintype Q] (r : Z → B → ℝ) (q : Z → B → Q) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (z : Z) : IsProbabilityWeight (rightCoordinateLift r q z)

Appending the actual coordinate preserves normalization of each original right kernel.

theorem Algebraic.Cutwidth.Extractor.factoredWeight_rightCoordinateLift {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) : factoredWeight w l (rightCoordinateLift r q) = mapWeight (fun (p : (Z × B) × A) => ((p.1.1, p.1.2, q p.1.1 p.1.2), p.2)) (factoredWeight w l r)

The lifted factored law is exactly a deterministic image of the original joint law.

theorem Algebraic.Cutwidth.Extractor.rightCoordinateRepair_source_eq {Z : Type u_1} {B : Type u_2} {Q : Type u_3} {X : Type u_4} [Fintype B] [Fintype Q] (w : Z → ℝ) (r : Z → B → ℝ) (r' : Z → B × Q → ℝ) (same : ∀ (z : Z) (b : B), w z * mapWeight Prod.fst (r' z) b = w z * r z b) (x : Z → B → X) (z : Z) (x₀ : X) : w z * mapWeight (fun (bq : B × Q) => x z bq.1) (r' z) x₀ = w z * mapWeight (x z) (r z) x₀

Preserving the weighted right marginal preserves every original right-source envelope.

theorem Algebraic.Cutwidth.Extractor.factoredWeight_forget_right_eq {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 → ℝ) (r' : Z → B × Q → ℝ) (same : ∀ (z : Z) (b : B), w z * mapWeight Prod.fst (r' z) b = w z * r z b) : mapWeight (fun (p : (Z × B × Q) × A) => ((p.1.1, p.1.2.1), p.2)) (factoredWeight w l r') = factoredWeight w l r

Discarding the repaired coordinate recovers the entire original factored joint law.

theorem Algebraic.Cutwidth.Extractor.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))

A uniform coordinate repair preserves both original sources at exactly the joint seed error.

theorem Algebraic.Cutwidth.Extractor.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))

The same repair has the corresponding weighted marginal identities on every row.

theorem Algebraic.Cutwidth.Extractor.weightDist_uniformSecond_le_of_dist_of_same_first {Tag : Type u_1} {Out : Type u_2} [Fintype Tag] [Fintype Out] {p q : Tag × Out → ℝ} {ρ ε : ℝ} (near : weightDist p q ≤ ρ) (uniform : weightDist q (uniformSecondWeight q) ≤ ε) (same : firstWeight p = firstWeight q) : weightDist p (uniformSecondWeight p) ≤ ρ + ε

A repair preserving the retained marginal costs its total variation distance once.

theorem Algebraic.Cutwidth.Extractor.weightDist_uniformSecond_le_of_dist {Tag : Type u_1} {Out : Type u_2} [Fintype Tag] [Fintype Out] {p q : Tag × Out → ℝ} {ρ ε : ℝ} (near : weightDist p q ≤ ρ) (uniform : weightDist q (uniformSecondWeight q) ≤ ε) : weightDist p (uniformSecondWeight p) ≤ 2 * ρ + ε

An unrestricted repair costs at most twice its distance against the actual retained marginal.

theorem Algebraic.Cutwidth.Extractor.weightDist_uniformSecond_map_le_of_dist_of_same_first {α : Type u_1} {Tag : Type u_2} {Out : Type u_3} [Fintype α] [Fintype Tag] [Fintype Out] {p q : α → ℝ} {ρ ε : ℝ} (F : α → Tag × Out) (near : weightDist p q ≤ ρ) (uniform : weightDist (mapWeight F q) (uniformSecondWeight (mapWeight F q)) ≤ ε) (same : firstWeight (mapWeight F p) = firstWeight (mapWeight F q)) : weightDist (mapWeight F p) (uniformSecondWeight (mapWeight F p)) ≤ ρ + ε

Deterministic continuation pays once when its retained marginal is preserved.

theorem Algebraic.Cutwidth.Extractor.weightDist_uniformSecond_map_le_of_dist {α : Type u_1} {Tag : Type u_2} {Out : Type u_3} [Fintype α] [Fintype Tag] [Fintype Out] {p q : α → ℝ} {ρ ε : ℝ} (F : α → Tag × Out) (near : weightDist p q ≤ ρ) (uniform : weightDist (mapWeight F q) (uniformSecondWeight (mapWeight F q)) ≤ ε) : weightDist (mapWeight F p) (uniformSecondWeight (mapWeight F p)) ≤ 2 * ρ + ε

Deterministic continuation pays twice when its actual retained marginal may change.