Pairwise security of the actual first affine phase

The three actual calls give a pairwise guarantee from the original normalized source factors, a uniform honest right input, unequal advice, and finite numerical budgets. Both laws retain the complete executed transcript and original right state. The left-contribution guarantee is suited to subsequent merging; the masked-output guarantee concerns the actual program. Neither theorem assumes an intermediate seed certificate.

This proves the pairwise first phase of the standard-to-affine conversion in Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Theorem 6.1, printed p.23, for the displayed actual components and budgets: https://arxiv.org/abs/2110.12652. The later subset-doubling rounds are required to obtain joint security against all tamperings.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOne_left_pair_dist_le (n d t h L₀ e₀ L₁ target er : ℕ) {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₀) (final_length : Nat.clog 2 (n + 1) ≤ L₁) (final_error : er + h + 2 ≤ L₁) (final_budget : (h + 1) * (er + 2 * h + Nat.clog 2 (L₁ + 1) + 4) ≤ 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 := affinePhaseOneLeftPairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i; weightDist actual (uniformSecondWeight actual) ≤ affinePhaseOneError t h L₀ e₀ L₁ target er (∑ z : Z, μ z)

Original source assumptions bound the actual left contributions against one tampering.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOne_pair_dist_le (n d t h L₀ e₀ L₁ target er : ℕ) {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₀) (final_length : Nat.clog 2 (n + 1) ≤ L₁) (final_error : er + h + 2 ≤ L₁) (final_budget : (h + 1) * (er + 2 * h + Nat.clog 2 (L₁ + 1) + 4) ≤ 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 := affinePhaseOnePairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i; weightDist actual (uniformSecondWeight actual) ≤ affinePhaseOneError t h L₀ e₀ L₁ target er (∑ z : Z, μ z)

The complete actual masked first phase satisfies the pairwise strong guarantee.