Realize a bound and store a finite witness

The initialized prefix keeps setup scratch separate, preserves fresh verifier work, and materializes a certificate on a charged tape. Its endpoint resets all later resource accounting to parked heads plus the bounded guess time.

def Complexity.WitnessTM.Verifier.prefixEntry (r k : ℕ) (x : List Bool) : TapePred (tapes r k + 1)

Initial visible tapes with a live, immutable external source at cell one.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.WitnessTM.Verifier.prefixReady (r k : ℕ) (x : List Bool) (B : ℕ) : TapePred (tapes r k + 1)

Setup's canonical reserved frame alongside the same live external source.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.WitnessTM.Verifier.prefixPost (r k : ℕ) (x : List Bool) (B : ℕ) : TapePred (tapes r k + 1)

A bounded certificate is stored; reserved verifier/pair tapes remain blank. All marker invariants and charged head bounds are retained for the later seam.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.WitnessTM.Verifier.setup_hoareTime {r : ℕ} {bound : ℕ → ℕ} (setup : WitnessBoundSetup r bound) (k : ℕ) (x : List Bool) : (ofDeterministic (setup.machine.liftTM (k + 2))).machine.HoareTime (prefixEntry r k x) (prefixReady r k x (bound x.length)) (setup.time x.length)

Setup can run with its external source ignored and uncharged.

theorem Complexity.WitnessTM.Verifier.prefixReady_transition {r k : ℕ} {x : List Bool} {B : ℕ} {inp out : Tape} {work : Fin (tapes r k + 1) → Tape} (h : prefixReady r k x B inp work out) : prefixReady r k x B (TM.transitionInput inp) (fun (i : Fin (tapes r k + 1)) => TM.transitionTape (work i)) (TM.transitionTape out)

The setup-to-store handoff is literally idle on the canonical parked frame.

theorem Complexity.WitnessTM.Verifier.store_ready_hoareTime (r k : ℕ) (x : List Bool) (B : ℕ) : (storeBounded (witnessIdx r k) (counterIdx r k)).machine.HoareTime (prefixReady r k x B) (prefixPost r k x B) (NTM.guessBoundedTime B 0)

Storing after setup yields every frame needed by the deterministic suffix.

theorem Complexity.WitnessTM.Verifier.prefix_hoareTime {r : ℕ} {bound : ℕ → ℕ} (setup : WitnessBoundSetup r bound) (k : ℕ) (x : List Bool) : (guessPrefix setup k).machine.HoareTime (prefixEntry r k x) (prefixPost r k x (bound x.length)) (setup.time x.length + 1 + NTM.guessBoundedTime (bound x.length) 0)

The initialized prefix has the sum of its two concrete phase budgets.

theorem Complexity.WitnessTM.Verifier.prefix_hoareSafety {r : ℕ} {bound : ℕ → ℕ} (setup : WitnessBoundSetup r bound) (k : ℕ) (x : List Bool) (H : ℕ) (hs : setup.space x.length ≤ H) (hg : 1 + NTM.guessBoundedTime (bound x.length) 0 ≤ H) : (guessPrefix setup k).machine.HoareSafety (prefixEntry r k x) fun (inp : Tape) (work : Fin (tapes r k + 1) → Tape) (out : Tape) => { state := (), input := inp, work := fun (i : Fin (tapes r k)) => work i.castSucc, output := out }.WithinDecisionSpace x.length H

Prefix safety uses setup's independent space and the materialization bound, without charging the external stream or any later verifier running time.

theorem Complexity.WitnessTM.Verifier.prefix_generates {r : ℕ} {bound : ℕ → ℕ} (setup : WitnessBoundSetup r bound) (k : ℕ) (x y : List Bool) (hy : y.length ≤ bound x.length) : ∃ (g : ℕ → Bool) (c : Cfg (tapes r k + 1) (guessPrefix setup k).machine.Q), ∃ t ≤ setup.time x.length + 1 + NTM.guessBoundedTime (bound x.length) 0, (guessPrefix setup k).machine.reachesIn t (NTM.loadCfg (guessPrefix setup k).machine x g) c ∧ (guessPrefix setup k).machine.halted c ∧ c.work (witnessIdx r k).castSucc = (Tape.init (List.map Γ.ofBool y)).move Dir3.right

Every bounded certificate is realized by the initialized prefix. The source stream is chosen after the deterministic setup, which never consults that stream.