The actual first phase initializes the complete affine iteration

The initializer packages the checked first-phase observations, original conditional sources, and output contributions. Its normalized factors, source envelopes, and old-row law agree exactly with the first-phase APIs. Following these with any finite number of rounds gives the actual complete affine correlation-breaker map, on the same original source variables.

The final law retains the executed transcript, full original right state, and every selected tampered output. These are exact algebraic identities and envelope accounting for Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1: https://arxiv.org/abs/2110.12652. Extraction errors and parameter reserves belong to the separate statistical iteration.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneIterationState_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) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : have s := affinePhaseOneIterationState n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice; IsProbabilityWeight s.weight ∧ (∀ (z : AffinePhaseOneTranscript Z t L₀ L₁), IsProbabilityWeight (s.left z)) ∧ ∀ (z : AffinePhaseOneTranscript Z t L₀ L₁), IsProbabilityWeight (s.right z)

The actual first phase supplies normalized initial factors.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneIterationState_factored (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) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : have s := affinePhaseOneIterationState n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice; mapWeight (affinePhaseOneIterationLift n d t L₀ e₀ L₁ e₁ x mask ys advice) (factoredWeight w l r) = factoredWeight s.weight s.left s.right

The initial factored law is the original law with its actual first-phase transcript.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneIterationState_rows_eq (n d t h L₀ e₀ L₁ e₁ er : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [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) (p : (Z × B) × A) (j : Option (Fin t)) : have s := affinePhaseOneIterationState n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice; have q := affinePhaseOneIterationLift n d t L₀ e₀ L₁ e₁ x mask ys advice p; (fun (k : Fin (matchedBlockOutputBits h L₁)) => s.leftRows q.1.1 q.2 j k ^^ s.rightRows q.1.1 q.1.2 j k) = affinePhaseOneOutput n d h L₀ e₀ L₁ e₁ er (fun (k : Fin n) => x p.1.1 p.2 k ^^ mask p.1.1 p.1.2 k) (ys p.1.1 p.1.2 j) (advice j)

The initial side contributions reconstruct each actual first-phase output.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneIterationState_leftRowsWeight_eq (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)) : have s := affinePhaseOneIterationState n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice; affineRoundLeftRowsWeight h t L₁ s.weight s.left s.leftRows S = affinePhaseOneLeftRowsWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice S

The initial old-left-row law is precisely the checked first-phase subset law.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneIterationState_left_envelope (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) (μ : 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) : have s := affinePhaseOneIterationState n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice; have envelope := affinePhaseOneTranscriptLeftEnvelope n d t L₀ e₀ L₁ e₁ μ r mask ys advice; (∀ (z : AffinePhaseOneTranscript Z t L₀ L₁), 0 ≤ envelope z) ∧ (∀ (z : AffinePhaseOneTranscript Z t L₀ L₁) (x₀ : Fin n → Bool), s.weight z * mapWeight (s.source z) (s.left z) x₀ ≤ envelope z) ∧ ∑ z : AffinePhaseOneTranscript Z t L₀ L₁, envelope z = ↑(Fintype.card (AffinePhaseOneCopies t (matchedBlockOutputBits 64 L₀))) * ∑ z : Z, μ z

The original-left initializer envelope has its checked sign, cap, and exact total.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneIterationState_right_envelope (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) (ν : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (z : Z), 0 ≤ ν z) (cap : ∀ (z : Z) (y₀ : Fin d → Bool), w z * mapWeight (fun (b : B) => ys z b none) (r z) y₀ ≤ ν z) : have s := affinePhaseOneIterationState n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice; have envelope := affinePhaseOneTranscriptRightEnvelope n t L₀ e₀ L₁ ν l x; (∀ (z : AffinePhaseOneTranscript Z t L₀ L₁), 0 ≤ envelope z) ∧ (∀ (z : AffinePhaseOneTranscript Z t L₀ L₁) (y₀ : Fin d → Bool), s.weight z * mapWeight (fun (b : B) => s.rightWords z b none) (s.right z) y₀ ≤ envelope z) ∧ ∑ z : AffinePhaseOneTranscript Z t L₀ L₁, envelope z = ↑(Fintype.card (AffinePhaseOneCopies t (matchedBlockSeedBits L₁))) * ↑(Fintype.card (AffinePhaseOneRightMessage t L₀)) * ∑ z : Z, ν z

The original-right initializer envelope has its checked sign, cap, and exact total.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneIterationState_iterate_factored (n d t h L₀ e₀ L₁ e₁ er rounds : ℕ) {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) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : have s := affinePhaseOneIterationState n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice; mapWeight (fun (p : (Z × B) × A) => s.lift er rounds (affinePhaseOneIterationLift n d t L₀ e₀ L₁ e₁ x mask ys advice p)) (factoredWeight w l r) = factoredWeight (s.iterate er rounds).weight (s.iterate er rounds).left (s.iterate er rounds).right

All initialized round factors are an exact image of the original source law.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneIterationState_iterate_rows_eq (n d t h L₀ e₀ L₁ e₁ er rounds : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [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) (p : (Z × B) × A) (j : Option (Fin t)) : have s := affinePhaseOneIterationState n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice; have q := s.lift er rounds (affinePhaseOneIterationLift n d t L₀ e₀ L₁ e₁ x mask ys advice p); (fun (k : Fin (matchedBlockOutputBits h L₁)) => (s.iterate er rounds).leftRows q.1.1 q.2 j k ^^ (s.iterate er rounds).rightRows q.1.1 q.1.2 j k) = affineCorrelationBreaker n d h L₀ e₀ L₁ e₁ er rounds (fun (k : Fin n) => x p.1.1 p.2 k ^^ mask p.1.1 p.1.2 k) (ys p.1.1 p.1.2 j) (advice j)

The initialized iteration executes the complete actual affine algorithm pointwise.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneIterationState_subsetWeight_eq (n d t h L₀ e₀ L₁ e₁ er rounds : ℕ) {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)) : have s := affinePhaseOneIterationState n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice; (s.iterate er rounds).subsetWeight S = mapWeight (fun (p : (Z × B) × A) => have input := fun (k : Fin n) => x p.1.1 p.2 k ^^ mask p.1.1 p.1.2 k; have tag := s.transcript er rounds (affinePhaseOneIterationLift n d t L₀ e₀ L₁ e₁ x mask ys advice p); (((tag, p.1.2), fun (j : ↥S) => affineCorrelationBreaker n d h L₀ e₀ L₁ e₁ er rounds input (ys p.1.1 p.1.2 (some ↑j)) (advice (some ↑j))), affineCorrelationBreaker n d h L₀ e₀ L₁ e₁ er rounds input (ys p.1.1 p.1.2 none) (advice none))) (factoredWeight w l r)

The full retained-subset law is exactly the actual algorithm on the original inputs.