The actual advice-generated seed in the first affine phase

The first masked extraction supplies an approximately uniform seed to the actual advice correlation breaker with the original right source as input. The source envelope pays for every first right observation. The resulting second seed is close to uniform given the original left state and one actual tampered second seed, without an intermediate security premise.

This is the advice step of Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Theorem 6.1, printed p.23: https://arxiv.org/abs/2110.12652. It supplies a pairwise seed guarantee; the final extraction and the later subset-doubling argument are separate.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneSecondSeedWeight_eq_alternating (n d t L₀ e₀ L₁ e₁ : ℕ) {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) (advice : Option (Fin t) → List Bool) (i : Fin t) : affinePhaseOneSecondSeedWeight n d t L₀ e₀ L₁ e₁ w l r x mask ys advice i = alternatingAdviceWeight d (matchedBlockOutputBits 64 L₀) L₁ e₁ 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) (fun (z : Z × AffinePhaseOneRightMessage t L₀) (a : A) => affinePhaseOneFirstLeft n t L₀ e₀ x z a (some i)) (fun (z : Z) (b : B) => ys z b none) (fun (z : Z) (b : B) => ys z b (some i)) (advice none) (advice (some i))

The actual second-seed law equals the observed advice call on the original source.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneSecondSeedWeight_probability (n d t L₀ e₀ L₁ e₁ : ℕ) {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) (advice : Option (Fin t) → List Bool) (i : Fin t) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affinePhaseOneSecondSeedWeight n d t L₀ e₀ L₁ e₁ w l r x mask ys advice i)

The two actual advice outputs and retained original states form a probability law.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOne_second_seed_dist_le (n d t L₀ e₀ L₁ target : ℕ) {Z A B : Type u} [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) (advice : Option (Fin t) → List Bool) (i : Fin t) (μ : Z → ℝ) (length : Nat.clog 2 (n + 1) ≤ L₀) (room : 64 ≤ L₀) (error : e₀ + 64 + 2 ≤ L₀) (size : matchedBlockSeedBits L₀ ≤ d) (guard : FlipFlopSizeGuard d (matchedBlockOutputBits 64 L₀) L₁ (adviceErrorExponent (advice none).length target)) (output_size : matchedBlockOutputBits 64 L₁ ≤ matchedBlockOutputBits 64 L₀) (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)) (advice_length : (advice none).length = (advice (some i)).length) (different : advice none ≠ advice (some i)) (source_budget : 2 ^ 150 * ((advice none).length + 1) * L₁ + (t + 1) * (matchedBlockSeedBits L₀ + matchedBlockOutputBits 64 L₀) ≤ d) (seed_width : 2 ^ 150 * ((advice none).length + 1) * L₁ ≤ matchedBlockOutputBits 64 L₀) : have e₁ := adviceErrorExponent (advice none).length target; have actual := affinePhaseOneSecondSeedWeight n d t L₀ e₀ L₁ e₁ w l r x mask ys advice i; weightDist actual (uniformSecondWeight actual) ≤ (2 ^ e₀)⁻¹ + 2 ^ (2 ^ 142 * L₀) * ∑ z : Z, μ z + (2 ^ target)⁻¹

Original source hypotheses imply the actual pairwise second-seed bound.