Correct, uniform polynomial-time evaluation of the advice-bit step

The actual three-call look-ahead and eight-call step agree exactly with their Boolean-vector definitions at the stated common scale. Their total string evaluators have registered polytime certificates with variable source words, shared scale, error exponent, and advice bit. These results certify the concrete computation and its cost. Opposite.False and Opposite.True prove the opposite-bit statistical guarantee, and Advice.Extraction the full advice iteration (adviceCorrelationBreaker_dist_le).

theorem Algebraic.Cutwidth.Extractor.flipFlopSeedPrefix_ofFn (L : ℕ) (q : Fin (matchedBlockOutputBits 64 L) → Bool) : List.ofFn (flipFlopSeedPrefix L q) = List.take (matchedBlockSeedBits L) (List.ofFn q)

The seed prefix is exactly the corresponding initial segment of the state word.

theorem Algebraic.Cutwidth.Extractor.flipFlopLookAheadRuntime_eq (n L e : ℕ) (left : MatchedBlockRuntimeValid n 24 L e) (state : MatchedBlockRuntimeValid (matchedBlockOutputBits 64 L) 24 L e) (x : Fin n → Bool) (q : Fin (matchedBlockOutputBits 64 L) → Bool) : flipFlopLookAheadRuntime L e (List.ofFn x) (List.ofFn q) = Complexity.pair (List.ofFn (flipFlopLookAhead n L e x q).1) (List.ofFn (flipFlopLookAhead n L e x q).2)

The string look-ahead encodes precisely both outputs of the concrete vector program.

theorem Algebraic.Cutwidth.Extractor.flipFlopStepRuntime_eq (n m L e : ℕ) (guard : FlipFlopSizeGuard n m L e) (x : Fin n → Bool) (y : Fin m → Bool) (q : Fin (matchedBlockOutputBits 64 L) → Bool) (b : Bool) : flipFlopStepRuntime L e (List.ofFn x) (List.ofFn y) (List.ofFn q) b = List.ofFn (flipFlopStep n m L e x y q b)

At a common valid scale, every input and either advice bit follow the vector program.

theorem Algebraic.Cutwidth.Extractor.flipFlopStepRuntime_length_le (L e : ℕ) (x y q : List Bool) (b : Bool) : (flipFlopStepRuntime L e x y q b).length ≤ matchedBlockOutputBits 64 L

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

theorem Algebraic.Cutwidth.Extractor.flipFlopLookAheadRuntime_mem_FP {L e : List Bool → ℕ} {x q : List Bool → List Bool} (hL : Complexity.UnaryFn L) (he : Complexity.UnaryFn e) (hx : x ∈ Complexity.FP) (hq : q ∈ Complexity.FP) : (fun (z : List Bool) => flipFlopLookAheadRuntime (L z) (e z) (x z) (q z)) ∈ Complexity.FP

Three actual extractor calls compose uniformly in the source, state, scale, and error.

theorem Algebraic.Cutwidth.Extractor.flipFlopStepRuntime_mem_FP {L e : List Bool → ℕ} {x y q : List Bool → List Bool} {b : List Bool → Bool} (hL : Complexity.UnaryFn L) (he : Complexity.UnaryFn e) (hx : x ∈ Complexity.FP) (hy : y ∈ Complexity.FP) (hq : q ∈ Complexity.FP) (hb : Complexity.FPPred fun (z : List Bool) => b z = true) : (fun (z : List Bool) => flipFlopStepRuntime (L z) (e z) (x z) (y z) (q z) (b z)) ∈ Complexity.FP

The entire advice-bit step is polynomial-time, including the bit-dependent choices.

theorem Algebraic.Cutwidth.Extractor.flipFlopStepEval_pair (x y q scale error bit : List Bool) : flipFlopStepEval (Complexity.pair (Complexity.pair x (Complexity.pair y q)) (Complexity.pair scale (Complexity.pair error bit))) = flipFlopStepRuntime scale.length error.length x y q (bit[0]?.getD false)

Canonical paired input decodes the source words, unary scale and error, and advice bit.

theorem Algebraic.Cutwidth.Extractor.flipFlopStepEval_mem_FP : flipFlopStepEval ∈ Complexity.FP

A single total polynomial-time evaluator covers all input lengths and shared parameters.