Correct and uniform polynomial-time evaluation of the full advice chain

The actual left-to-right advice fold and final extraction agree with their Boolean-vector definitions at the common scale. A single total string program handles variable sources, scale, error, and advice length. Its loop bound includes both original sources, both parameters, remaining advice, and the right state. No validity promise is needed for polynomial time.

These results establish the algorithm and its runtime. The statistical chain invariant and the correlation-breaking guarantee are proved in Advice.Extraction (adviceCorrelationBreaker_dist_le).

theorem Algebraic.Cutwidth.Extractor.adviceInitialWord_length (L : ℕ) (y : List Bool) : (adviceInitialWord L y).length = matchedBlockOutputBits 64 L

Initialization always writes the whole right-state width, using false completion.

theorem Algebraic.Cutwidth.Extractor.adviceInitialState_ofFn (m L : ℕ) (y : Fin m → Bool) : List.ofFn (adviceInitialState m L y) = adviceInitialWord L (List.ofFn y)

Runtime initialization exactly serializes the semantic prefix with false completion.

theorem Algebraic.Cutwidth.Extractor.encodeAdviceRunState_length (state : AdviceRunState) : (encodeAdviceRunState state).length = 4 * state.x.length + 2 * state.y.length + 2 * state.scale + 2 * state.error + 2 * state.remaining.length + state.q.length + 12

The full state codec has this exact length, including its immutable data.

theorem Algebraic.Cutwidth.Extractor.decodeAdviceRunState_encode (state : AdviceRunState) : decodeAdviceRunState (encodeAdviceRunState state) = state

Encoding and decoding preserve every component of a canonical state.

theorem Algebraic.Cutwidth.Extractor.adviceRunStepEval_encode (state : AdviceRunState) : adviceRunStepEval (encodeAdviceRunState state) = encodeAdviceRunState (adviceRunStep state)

The encoded transition computes exactly the structured transition.

theorem Algebraic.Cutwidth.Extractor.adviceRun_length_le (L e : ℕ) (x y advice : List Bool) (i : ℕ) : (encodeAdviceRunState (adviceRun L e x y advice i)).length ≤ 4 * x.length + 2 * y.length + 2 * L + 2 * e + 2 * advice.length + matchedBlockOutputBits 64 L + 12

Every iterate has a bound accounting for the entire encoded state.

theorem Algebraic.Cutwidth.Extractor.adviceRun_eq_adviceFold (n m L e : ℕ) (guard : FlipFlopSizeGuard n m L e) (x : Fin n → Bool) (y : Fin m → Bool) (advice : List Bool) : adviceRun L e (List.ofFn x) (List.ofFn y) advice advice.length = { x := List.ofFn x, y := List.ofFn y, scale := L, error := e, remaining := [], q := List.ofFn (adviceFold n m L e x y (adviceInitialState m L y) advice) }

Canonical execution consumes all advice and writes exactly the semantic final state.

theorem Algebraic.Cutwidth.Extractor.adviceCorrelationBreakerRuntime_eq (n m L e : ℕ) (guard : FlipFlopSizeGuard n m L e) (x : Fin n → Bool) (y : Fin m → Bool) (advice : List Bool) : adviceCorrelationBreakerRuntime L e (List.ofFn x) (List.ofFn y) advice = List.ofFn (adviceCorrelationBreaker n m L e x y advice)

The complete runtime agrees with the actual advice chain and final extractor.

theorem Algebraic.Cutwidth.Extractor.adviceCorrelationBreakerRuntime_length_le (L e : ℕ) (x y advice : List Bool) : (adviceCorrelationBreakerRuntime L e x y advice).length ≤ matchedBlockSeedBits L

Every result fits in the common seed width, including invalid inputs.

theorem Algebraic.Cutwidth.Extractor.adviceRunStepEval_mem_FP : adviceRunStepEval ∈ Complexity.FP

The total encoded step is polynomial-time on arbitrary state words.

theorem Algebraic.Cutwidth.Extractor.adviceRun_encoded_mem_FP {L e : List Bool → ℕ} {x y advice : List Bool → List Bool} (hL : Complexity.UnaryFn L) (he : Complexity.UnaryFn e) (hx : x ∈ Complexity.FP) (hy : y ∈ Complexity.FP) (hadvice : advice ∈ Complexity.FP) : (fun (z : List Bool) => encodeAdviceRunState (adviceRun (L z) (e z) (x z) (y z) (advice z) (advice z).length)) ∈ Complexity.FP

The complete bounded loop is uniform in both parameters and all three input words.

theorem Algebraic.Cutwidth.Extractor.adviceCorrelationBreakerRuntime_mem_FP {L e : List Bool → ℕ} {x y advice : List Bool → List Bool} (hL : Complexity.UnaryFn L) (he : Complexity.UnaryFn e) (hx : x ∈ Complexity.FP) (hy : y ∈ Complexity.FP) (hadvice : advice ∈ Complexity.FP) : (fun (z : List Bool) => adviceCorrelationBreakerRuntime (L z) (e z) (x z) (y z) (advice z)) ∈ Complexity.FP

All advice steps and final extraction have one unconditional polynomial-time certificate.

theorem Algebraic.Cutwidth.Extractor.adviceCorrelationBreakerEval_pair (x y scale error advice : List Bool) : adviceCorrelationBreakerEval (Complexity.pair (Complexity.pair x y) (Complexity.pair scale (Complexity.pair error advice))) = adviceCorrelationBreakerRuntime scale.length error.length x y advice

The evaluator decodes original sources, unary scale/error, and the whole advice word.

theorem Algebraic.Cutwidth.Extractor.adviceCorrelationBreakerEval_mem_FP : adviceCorrelationBreakerEval ∈ Complexity.FP

One total string evaluator computes the full advice construction in polynomial time.