Shared-seed block condensation by head/tail induction

Condition on the original head and first correct the conditional tails. Repairing the head while preserving the latent original value then keeps the corrected tails as block sources. Exact conditional distance averaging adds one condenser error per source block.

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededCondenser_block {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] {C : α → Seed → Ω} {Kin Kout : ℕ} {ε : ℝ} (cond : WeightedStrongSeededCondenser C Kin Kout ε) {t : ℕ} {p : (Fin t → α) → ℝ} (source : IsBlockSource p Kin) : ∃ (q : Seed → (Fin t → Ω) → ℝ), (∀ (y : Seed), IsBlockSource (q y) Kout) ∧ weightDist (weightedSeededOutput p fun (x : Fin t → α) (y : Seed) (i : Fin t) => C (x i) y) (seedFamilyWeight q) ≤ ↑t * ε