Carrying a joint approximation through one condense-then-split level

Average the block-condensation comparisons over earlier seeds, retaining the fresh seed inside each comparison. Splitting contracts this error and adds its own per-block cost. A previous joint approximation also contracts through the full retained-seed step, so all three errors add.

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededCondenser_condenseSplit {Earlier : Type u_1} {Fresh : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype Earlier] [Nonempty Earlier] [Fintype Fresh] [Fintype α] [Fintype β] {C : α → Fresh → β × β} {Kin k : ℕ} {ε : ℝ} (cond : WeightedStrongSeededCondenser C Kin (2 ^ k) ε) {t m s e : ℕ} {η : ℝ} (p : Earlier → (Fin t → α) → ℝ) (actual : Earlier × (Fin t → α) → ℝ) (source : ∀ (y : Earlier), IsBlockSource (p y) Kin) (close : weightDist actual (seedFamilyWeight p) ≤ η) (card : Fintype.card β = 2 ^ m) (width : s ≤ m) (entropy : m + s + e ≤ k) : ∃ (q : Earlier × Fresh → (Fin (2 * t) → β) → ℝ), (∀ (sy : Earlier × Fresh), IsBlockSource (q sy) (2 ^ s)) ∧ weightDist (retainedSeedStep (fun (x : Earlier) => condenseSplitMap C t) actual) (seedFamilyWeight q) ≤ η + ↑t * (ε + (2 ^ e)⁻¹)