The initial seed of the actual affine phase

A uniform original right input supplies the balanced prefix used by the first linear extractor. Its actual masked output is close to uniform even after retaining every tampered prefix and first mask contribution. The bound uses only the original source's point-mass envelope; it assumes no intermediate seed certificate or execution witness.

This supplies the first extraction in Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Theorem 6.1, printed p.23: https://arxiv.org/abs/2110.12652. The subsequent advice call and extraction, and the later independence-merging rounds, require further proofs.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneFirstSeed_uniform (d L₀ : ℕ) (size : matchedBlockSeedBits L₀ ≤ d) : mapWeight (affinePhaseOneFirstSeed d L₀) (uniformWeight (Fin d → Bool)) = uniformWeight (Fin (matchedBlockSeedBits L₀) → Bool)

A sufficiently long uniform right input has a uniform first seed prefix.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOne_initial_seed_dist_le (n d t L₀ e₀ : ℕ) (length : Nat.clog 2 (n + 1) ≤ L₀) (room : 64 ≤ L₀) (error : e₀ + 64 + 2 ≤ L₀) (size : matchedBlockSeedBits L₀ ≤ d) {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 → ℝ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (μ : 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₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (uniform : ∀ (z : Z), mapWeight (fun (b : B) => ys z b none) (r z) = uniformWeight (Fin d → Bool)) : have actual := alternatingSeedWeight w l r (affinePhaseOneRightMessage n d t L₀ e₀ mask ys) fun (z : Z × AffinePhaseOneRightMessage t L₀) (a : A) => affinePhaseOneFirstLeft n t L₀ e₀ x z a none; weightDist actual (uniformSecondWeight actual) ≤ (2 ^ e₀)⁻¹ + 2 ^ (2 ^ 142 * L₀) * ∑ z : Z, μ z

The actual initial extraction retains all first right messages at no additional cost.