Two-round extraction after repairing a nearly uniform right state

The right coordinate is repaired inside its full correlated state; the left law and all original right marginals are kept. The generic look-ahead theorem then has an exact uniform state envelope and an exact uniform initial seed. Deterministic continuation and comparison with the actual retained marginal charge twice the original repair distance. The program itself is unchanged.

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_lookAhead_uniformState_dist_le {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Mid : Type u_7} [Fintype Z] [Fintype A] [Fintype B] [Fintype X] [Fintype Q] [Fintype Seed] [Fintype Mid] [Nonempty Seed] [Nonempty Mid] {W : X → Seed → Mid} {QExt : Q → Mid → Seed} {K J : ℕ} {ε η ρ : ℝ} (first : WeightedStrongSeededExtractor W K ε) (first_error : 0 ≤ ε) (second : WeightedStrongSeededExtractor QExt J η) (second_error : 0 ≤ η) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → X) (q q' : Z → B → Q) (initialSeed : Q → Seed) (μ : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (z : Z), 0 ≤ μ z) (cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (balanced : mapWeight initialSeed (uniformWeight Q) = uniformWeight Seed) (state : weightDist (retainedSeedWeight w r q) (uniformSecondWeight (retainedSeedWeight w r q)) ≤ ρ) : weightDist (lookAheadExtractionWeight w l r x x' q q' initialSeed W QExt) (uniformSecondWeight (lookAheadExtractionWeight w l r x x' q q' initialSeed W QExt)) ≤ 2 * ε + η + 2 * ρ + ↑K * (1 + ↑(Fintype.card (Mid × Mid))) * ∑ z : Z, μ z + ↑J * ↑(Fintype.card (Seed × Seed)) / ↑(Fintype.card Q)