Uniform computation of the actual first affine phase

One total string program performs the first extraction, the actual advice construction, and the growing-depth final extraction, retaining the original source words throughout. Canonical inputs agree with affinePhaseOneOutput under the three explicit component guards. No source distribution or statistical premise occurs in the computation theorem.

The runtime and paired evaluator are uniformly polynomial-time on all inputs. In particular, the unary parameter selects logarithmic recursion depth; arbitrary unary depths with exponentially many leaves are not used.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneFirstSeedWord_length (L₀ : ℕ) (y : List Bool) : (affinePhaseOneFirstSeedWord L₀ y).length = matchedBlockSeedBits L₀

False completion produces exactly the first matched seed width.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneFirstSeed_ofFn (d L₀ : ℕ) (y : Fin d → Bool) : List.ofFn (affinePhaseOneFirstSeed d L₀ y) = affinePhaseOneFirstSeedWord L₀ (List.ofFn y)

The total prefix operation agrees with the semantic initial seed, including short words.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneRuntime_eq_affinePhaseOneOutput (n d t L₀ e₀ L₁ e₁ er : ℕ) (first : MatchedBlockRuntimeValid n 64 L₀ e₀) (adviceGuard : FlipFlopSizeGuard d (matchedBlockOutputBits 64 L₀) L₁ e₁) (last : GrowingMatchedBlockRuntimeValid n t L₁ er) (x : Fin n → Bool) (y : Fin d → Bool) (advice : List Bool) : affinePhaseOneRuntime t L₀ e₀ L₁ e₁ er (List.ofFn x) (List.ofFn y) advice = List.ofFn (affinePhaseOneOutput n d (growingMatchedBlockDepth t) L₀ e₀ L₁ e₁ er x y advice)

The three actual string calls compute the semantic first-phase output exactly.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneRuntime_length (t L₀ e₀ L₁ e₁ er : ℕ) (x y advice : List Bool) : (affinePhaseOneRuntime t L₀ e₀ L₁ e₁ er x y advice).length = if GrowingMatchedBlockRuntimeValid x.length t L₁ er then 2 ^ growingMatchedBlockDepth t * L₁ else 0

Exact output length depends only on the final component's guard.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneRuntime_length_le (t L₀ e₀ L₁ e₁ er : ℕ) (x y advice : List Bool) : (affinePhaseOneRuntime t L₀ e₀ L₁ e₁ er x y advice).length ≤ 2 ^ 65 * (t + 1) * L₁

A polynomial output bound holds for every choice of parameters and source words.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneFirstSeedWord_mem_FP {L₀ : List Bool → ℕ} {y : List Bool → List Bool} (hL₀ : Complexity.UnaryFn L₀) (hy : y ∈ Complexity.FP) : (fun (z : List Bool) => affinePhaseOneFirstSeedWord (L₀ z) (y z)) ∈ Complexity.FP

Exact initial-seed padding is uniformly polynomial-time.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneRuntime_mem_FP {t L₀ e₀ L₁ e₁ er : List Bool → ℕ} {x y advice : List Bool → List Bool} (ht : Complexity.UnaryFn t) (hL₀ : Complexity.UnaryFn L₀) (he₀ : Complexity.UnaryFn e₀) (hL₁ : Complexity.UnaryFn L₁) (he₁ : Complexity.UnaryFn e₁) (her : Complexity.UnaryFn er) (hx : x ∈ Complexity.FP) (hy : y ∈ Complexity.FP) (hadvice : advice ∈ Complexity.FP) : (fun (z : List Bool) => affinePhaseOneRuntime (t z) (L₀ z) (e₀ z) (L₁ z) (e₁ z) (er z) (x z) (y z) (advice z)) ∈ Complexity.FP

All numerical and word operands may vary with the runtime input.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneEval_pair (x y advice parameter firstScale firstError secondScale secondError finalError : List Bool) : affinePhaseOneEval (Complexity.pair (Complexity.pair x (Complexity.pair y advice)) (Complexity.pair parameter (Complexity.pair (Complexity.pair firstScale firstError) (Complexity.pair secondScale (Complexity.pair secondError finalError))))) = affinePhaseOneRuntime parameter.length firstScale.length firstError.length secondScale.length secondError.length finalError.length x y advice

The paired evaluator decodes three data words and six unary numerical words.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneEval_mem_FP : affinePhaseOneEval ∈ Complexity.FP

One paired evaluator is polynomial-time on all strings, including malformed pairings.

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

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