Exact repair of a head with a latent conditional tail

Repair the deterministic pair (f a, a) and attach the original tail law conditioned on a to both pair distributions. This construction preserves the arbitrary correlation of the latent state with its tail. The repaired tuple's distance is exactly the distance of the old and new head marginals.

theorem Algebraic.Cutwidth.Extractor.Internal.exists_prepend_replacement {α : Type u_1} {Ω : Type u_2} [Fintype α] [Fintype Ω] (t : ℕ) (w : α → ℝ) (tail : α → (Fin t → Ω) → ℝ) (f : α → Ω) (target : Ω → ℝ) (hw : IsProbabilityWeight w) (htail : ∀ (a : α), IsProbabilityWeight (tail a)) (htarget : IsProbabilityWeight target) : ∃ (c : Ω × α → ℝ) (r : (Fin (t + 1) → Ω) → ℝ), IsProbabilityWeight c ∧ IsProbabilityWeight r ∧ (∀ (h : Ω), ∑ a : α, c (h, a) = target h) ∧ mapWeight (fun (z : Fin (t + 1) → Ω) => z 0) r = target ∧ (∀ (h : Ω) (z : Fin t → Ω), r (Fin.cons h z) = ∑ a : α, c (h, a) * tail a z) ∧ weightDist (mapWeight (fun (az : α × (Fin t → Ω)) => Fin.cons (f az.1) az.2) fun (az : α × (Fin t → Ω)) => w az.1 * tail az.1 az.2) r = weightDist (mapWeight f w) target