Initial security for all left-row subsets of size at most one

The law is the old-left-row law at the complete actual first-phase transcript. For any subset of one tampering, an exact projection drops only the original right state and unwanted tampered outputs from the checked pair law. Consequently the pairwise error is also the error for every empty or singleton subset, without an additional statistical loss.

The security theorems assume a positive number of tamperings, so the empty subset can use a genuine pair index. They consume only original source and advice hypotheses; the selected-parameter theorem discharges every numerical guard. This initializes the subset invariant in the first phase of Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1: https://arxiv.org/abs/2110.12652.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneLeftRowsWeight_eq_map_pair (n d t h L₀ e₀ L₁ e₁ er : ℕ) {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) (S : Finset (Fin t)) (i : Fin t) (selected : S ⊆ {i}) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : affinePhaseOneLeftRowsWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice S = mapWeight (fun (p : ((AffinePhaseOneTranscript Z t L₀ L₁ × B) × (Fin (matchedBlockOutputBits h L₁) → Bool)) × (Fin (matchedBlockOutputBits h L₁) → Bool)) => ((p.1.1.1, fun (x : ↥S) => p.1.2), p.2)) (affinePhaseOneLeftPairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i)

The actual subset law is a projection of any pair whose index contains the subset.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneLeftRowsWeight_dist_le_pair (n d t h L₀ e₀ L₁ e₁ er : ℕ) {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) (S : Finset (Fin t)) (i : Fin t) (selected : S ⊆ {i}) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : weightDist (affinePhaseOneLeftRowsWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice S) (uniformSecondWeight (affinePhaseOneLeftRowsWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice S)) ≤ weightDist (affinePhaseOneLeftPairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i) (uniformSecondWeight (affinePhaseOneLeftPairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i))

Discarding the original right state and extra selected output cannot increase distance.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneLeftRowsWeight_probability (n d t h L₀ e₀ L₁ e₁ er : ℕ) {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) (S : Finset (Fin t)) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affinePhaseOneLeftRowsWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice S)

Normalized original factors induce a normalized first-phase subset law.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOne_left_subset_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) (S : Finset (Fin t)) (μ : Z → ℝ) (positive : 0 < t) (small : S.card ≤ 1) (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 : ∀ (i : Fin t), (advice none).length = (advice (some i)).length) (different : ∀ (i : Fin t), 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 := affinePhaseOneLeftRowsWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice S; weightDist actual (uniformSecondWeight actual) ≤ affinePhaseOneError t h L₀ e₀ L₁ target er (∑ z : Z, μ z)

Original source assumptions initialize every empty or singleton left-row subset.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOne_left_subset_parameters_dist_le (n t a 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 (affinePhaseOneRightBits n t a target)) (advice : Option (Fin t) → List Bool) (S : Finset (Fin t)) (μ : Z → ℝ) (positive : 0 < t) (small : S.card ≤ 1) (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 (affinePhaseOneRightBits n t a target) → Bool)) (honest_length : (advice none).length = a) (tampered_length : ∀ (i : Fin t), (advice (some i)).length = a) (different : ∀ (i : Fin t), advice none ≠ advice (some i)) (source : ∑ z : Z, μ z ≤ (2 ^ affinePhaseOneSourceEntropy n t a target)⁻¹) : let d := affinePhaseOneRightBits n t a target; have h := growingMatchedBlockDepth t; have L₀ := affinePhaseOneInitialScale n t a target; have L₁ := affinePhaseOneScale n t a target; have e := affinePhaseOneLocalError target; have actual := affinePhaseOneLeftRowsWeight n d t h L₀ e L₁ (adviceErrorExponent a e) e w l r x mask ys advice S; weightDist actual (uniformSecondWeight actual) ≤ (2 ^ target)⁻¹

The finite chooser gives error 2^-target for every initial subset of size at most one.