Uniform execution of repeated actual affine rounds

The semantic correspondence reads the same original source words at every round. The polynomial-time certificate bounds the complete encoded state, including the original words, unary parameters, and arbitrary initial row. It is unconditional on malformed inputs and invalid numerical parameters.

theorem Algebraic.Cutwidth.Extractor.affineRoundsRuntime_succ (t L e i : ℕ) (x y row : List Bool) : affineRoundsRuntime t L e (i + 1) x y row = affineRoundRuntime t L e x y (affineRoundsRuntime t L e i x y row)

One further iteration performs the actual round on the current row.

theorem Algebraic.Cutwidth.Extractor.affineRoundsStepEval_pair (t L e : ℕ) (x y row : List Bool) : affineRoundsStepEval (Complexity.pair (affineRoundsContextWord t L e x y) row) = Complexity.pair (affineRoundsContextWord t L e x y) (affineRoundRuntime t L e x y row)

An encoded step preserves the original context exactly.

theorem Algebraic.Cutwidth.Extractor.affineRoundsStepEval_iterate (t L e i : ℕ) (x y row : List Bool) : affineRoundsStepEval^[i] (Complexity.pair (affineRoundsContextWord t L e x y) row) = Complexity.pair (affineRoundsContextWord t L e x y) (affineRoundsRuntime t L e i x y row)

Every encoded iterate contains the original context and the actual evolving row.

theorem Algebraic.Cutwidth.Extractor.affineRoundsRuntime_length_le (t L e i : ℕ) (x y row : List Bool) : (affineRoundsRuntime t L e i x y row).length ≤ row.length + 2 ^ 65 * (t + 1) * L

Every iterate is bounded by the initial row and one round output bound.

theorem Algebraic.Cutwidth.Extractor.affineRoundsState_length_le (t L e i : ℕ) (x y row : List Bool) : (Complexity.pair (affineRoundsContextWord t L e x y) (affineRoundsRuntime t L e i x y row)).length ≤ 2 * (affineRoundsContextWord t L e x y).length + 2 + row.length + 2 ^ 65 * (t + 1) * L

The complete encoded state includes both original sources and all unary parameters.

theorem Algebraic.Cutwidth.Extractor.affineRoundsRuntime_eq_affineRoundsOutput (n d t L e i : ℕ) (right : MatchedBlockRuntimeValid d 24 L e) (rowGuard : MatchedBlockRuntimeValid (matchedBlockOutputBits (growingMatchedBlockDepth t) L) 24 L e) (last : GrowingMatchedBlockRuntimeValid n t L e) (x : Fin n → Bool) (y : Fin d → Bool) (row : Fin (matchedBlockOutputBits (growingMatchedBlockDepth t) L) → Bool) : affineRoundsRuntime t L e i (List.ofFn x) (List.ofFn y) (List.ofFn row) = List.ofFn (affineRoundsOutput n d (growingMatchedBlockDepth t) L e i x y row)

Canonical words follow exactly the semantic iteration on the same original sources.

theorem Algebraic.Cutwidth.Extractor.affineRoundsContextWord_mem_FP {t L e : List Bool → ℕ} {x y : List Bool → List Bool} (ht : Complexity.UnaryFn t) (hL : Complexity.UnaryFn L) (he : Complexity.UnaryFn e) (hx : x ∈ Complexity.FP) (hy : y ∈ Complexity.FP) : (fun (z : List Bool) => affineRoundsContextWord (t z) (L z) (e z) (x z) (y z)) ∈ Complexity.FP

Encoding the immutable source context and unary parameters is polynomial-time.

theorem Algebraic.Cutwidth.Extractor.affineRoundsStepEval_mem_FP : affineRoundsStepEval ∈ Complexity.FP

One total encoded step is polynomial-time on every word.

theorem Algebraic.Cutwidth.Extractor.affineRoundsRuntime_mem_FP {t L e i : List Bool → ℕ} {x y row : List Bool → List Bool} (ht : Complexity.UnaryFn t) (hL : Complexity.UnaryFn L) (he : Complexity.UnaryFn e) (hi : Complexity.UnaryFn i) (hx : x ∈ Complexity.FP) (hy : y ∈ Complexity.FP) (hrow : row ∈ Complexity.FP) : (fun (z : List Bool) => affineRoundsRuntime (t z) (L z) (e z) (i z) (x z) (y z) (row z)) ∈ Complexity.FP

A unary number of actual rounds is uniformly polynomial-time with no validity promise.

theorem Algebraic.Cutwidth.Extractor.affineRoundsEval_pair (t L e : ℕ) (x y row rounds : List Bool) : affineRoundsEval (Complexity.pair (Complexity.pair (affineRoundsContextWord t L e x y) row) rounds) = affineRoundsRuntime t L e rounds.length x y row

The single evaluator decodes the original sources, row, parameters, and round count.

theorem Algebraic.Cutwidth.Extractor.affineRoundsEval_mem_FP : affineRoundsEval ∈ Complexity.FP

One total polynomial-time evaluator runs the complete repeated-round program.

theorem Algebraic.Cutwidth.Extractor.affineRoundsEval_length_le (z : List Bool) : (affineRoundsEval z).length ≤ z.length + 2 ^ 65 * (z.length + 1) ^ 2

The full evaluator has a quadratic output bound, including the zero-round input row.