Exact computation and polynomial time for the complete advice chain

Canonical inputs follow the semantic advice fold and its final extractor. The complete encoded-state bound discharges the iteration theorem, including all original inputs and remaining advice. The certificates have no numerical validity or statistical hypotheses.

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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.adviceRuntimeFold_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) (advice : List Bool) : List.foldl (flipFlopStepRuntime L e (List.ofFn x) (List.ofFn y)) (List.ofFn q) advice = List.ofFn (adviceFold n m L e x y q advice)

theorem Algebraic.Cutwidth.Extractor.Internal.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) }

theorem Algebraic.Cutwidth.Extractor.Internal.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)

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

theorem Algebraic.Cutwidth.Extractor.Internal.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

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