Actual final seeds from the original right source

The actual short-row guarantee seeds a second extraction on the original right word. Its envelope accounts for every prior right observation, while the retained law records all actual short rows and the selected tampered final seeds. This is the recovery call in Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1: https://arxiv.org/abs/2110.12652.

theorem Algebraic.Cutwidth.Extractor.affineRoundFinalSeed_dist_le (d h t L e : ℕ) (length : Nat.clog 2 (d + 1) ≤ L) (room : 64 ≤ L) (error : e + 24 + 2 ≤ L) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (S : Finset (Fin t)) (ν : Z → ℝ) {δ : ℝ} (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (z : Z), 0 ≤ ν z) (cap : ∀ (z : Z) (y₀ : Fin d → Bool), w z * mapWeight (fun (b : B) => ys z b none) (r z) y₀ ≤ ν z) (seed : weightDist (affineRoundMiddleSeedInputWeight d h t L e w l r wl wr ys S) (uniformSecondWeight (affineRoundMiddleSeedInputWeight d h t L e w l r wl wr ys S)) ≤ δ) : weightDist (affineRoundFinalSeedWeight d h t L e w l r wl wr ys S) (uniformSecondWeight (affineRoundFinalSeedWeight d h t L e w l r wl wr ys S)) ≤ (2 ^ e)⁻¹ + δ + 2 ^ (2 ^ 62 * L) * ↑(Fintype.card (Fin (matchedBlockSeedBits L) → Bool)) ^ S.card * ↑(Fintype.card (AffineRoundShortMessages t L)) ^ 3 * ∑ z : Z, ν z

The actual short-row guarantee and original right envelope control the executed final seed.