Uniform evaluation of an actual affine extraction round

A single total string evaluator performs all four matched calls, rereading both original source words. Under the component guards its output equals the actual semantic round at depth clog 2 (t+1)+64. The growing arithmetic budget also pays the old row's short-call guard.

All numerical inputs are unary. Polynomial time is unconditional, including malformed words and invalid parameters, and the complete encoded output has a quadratic length bound. No unrestricted unary exponential depth, statistical independence, or round extraction guarantee is asserted here.

theorem Algebraic.Cutwidth.Extractor.affineRoundPrefixWord_length (L : ℕ) (row : List Bool) : (affineRoundPrefixWord L row).length = matchedBlockSeedBits L

The initial prefix word always has the common short width.

theorem Algebraic.Cutwidth.Extractor.affineRoundPrefix_ofFn (h L : ℕ) (row : Fin (matchedBlockOutputBits h L) → Bool) : List.ofFn (affineRoundPrefix h L row) = affineRoundPrefixWord L (List.ofFn row)

The total vector prefix and false-completed string prefix agree at every semantic depth.

theorem Algebraic.Cutwidth.Extractor.affineRoundRuntime_short_guard (n d t L e : ℕ) (growing : GrowingMatchedBlockRuntimeValid n t L e) (length : Nat.clog 2 (d + 1) ≤ L) : MatchedBlockRuntimeValid d 24 L e

A valid growing schedule supplies every short-call guard except its source-length bound.

theorem Algebraic.Cutwidth.Extractor.affineRoundRuntime_row_guard (n t L e : ℕ) (growing : GrowingMatchedBlockRuntimeValid n t L e) : MatchedBlockRuntimeValid (matchedBlockOutputBits (growingMatchedBlockDepth t) L) 24 L e

The growing seed budget also makes the complete old row a valid short-extraction source.

theorem Algebraic.Cutwidth.Extractor.affineRoundRuntime_eq_affineRoundOutput (n d t L e : ℕ) (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) : affineRoundRuntime t L e (List.ofFn x) (List.ofFn y) (List.ofFn row) = List.ofFn (affineRoundOutput n d (growingMatchedBlockDepth t) L e x y row)

Canonical source and row words follow exactly the four actual semantic calls.

theorem Algebraic.Cutwidth.Extractor.affineRoundRuntime_short_length_le (L e : ℕ) (source seeds : List Bool) : (matchedBlockExtractorRuntime 24 L e source seeds).length ≤ matchedBlockSeedBits L

Each of the three short intermediate words is bounded even on invalid inputs.

theorem Algebraic.Cutwidth.Extractor.affineRoundRuntime_length (t L e : ℕ) (x y row : List Bool) : (affineRoundRuntime t L e x y row).length = if GrowingMatchedBlockRuntimeValid x.length t L e then 2 ^ growingMatchedBlockDepth t * L else 0

The final growing call determines the exact runtime output length.

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

Every runtime output has polynomially bounded length in the unary parameters.

theorem Algebraic.Cutwidth.Extractor.affineRoundPrefixWord_mem_FP {L : List Bool → ℕ} {row : List Bool → List Bool} (hL : Complexity.UnaryFn L) (hrow : row ∈ Complexity.FP) : (fun (z : List Bool) => affineRoundPrefixWord (L z) (row z)) ∈ Complexity.FP

Generating the false-completed row prefix is uniformly polynomial-time.

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

All four calls compose into a total uniform polynomial-time runtime.

theorem Algebraic.Cutwidth.Extractor.affineRoundEval_pair (x y row parameter scale error : List Bool) : affineRoundEval (Complexity.pair (Complexity.pair x (Complexity.pair y row)) (Complexity.pair parameter (Complexity.pair scale error))) = affineRoundRuntime parameter.length scale.length error.length x y row

The paired evaluator decodes three data words and three unary parameter words.

theorem Algebraic.Cutwidth.Extractor.affineRoundEval_mem_FP : affineRoundEval ∈ Complexity.FP

One total string evaluator computes the complete round on every encoded input.

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

The complete encoded evaluator has a quadratic output-length bound.