Block-source caps after exact head repair

The repaired tuple is a nonnegative mixture of the original conditional tail laws at each head. Its head marginal has the requested cap, so the prepend criterion supplies every block-source inequality.

theorem Algebraic.Cutwidth.Extractor.Internal.exists_block_tail_replacement {α : Type u_1} {Ω : Type u_2} [Fintype α] [Fintype Ω] (t K : ℕ) (w : α → ℝ) (tail : α → (Fin t → Ω) → ℝ) (f : α → Ω) (target : Ω → ℝ) (hw : IsProbabilityWeight w) (htail : ∀ (a : α), IsBlockSource (tail a) K) (htarget : IsProbabilityWeight target) (cap : CappedWeight target K) : ∃ (r : (Fin (t + 1) → Ω) → ℝ), IsBlockSource r K ∧ mapWeight (fun (z : Fin (t + 1) → Ω) => z 0) r = target ∧ 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