Correctness and closure proofs for the concrete advice-bit program

Canonical words follow the same three-call and eight-call computations as the vector definitions. Polynomial time is composed from the registered matched-extractor certificate, including both conditional choices. The final refresh gives a uniform output-size bound even on invalid parameters.

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

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

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

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

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

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

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

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