Realized finite witness bounds

A witness bound is supplied by an actual deterministic setup machine. Its unary counter occupies charged workspace. Time, all-prefix decision space, and the canonical phase-entry frame are recorded separately from the numeric bound.

def Complexity.WitnessBoundSetup.linearMachine : TM 1

Concrete setup for witnesses of length at most n + 1.

Equations

• Complexity.WitnessBoundSetup.linearMachine = Complexity.TM.bumpTM.seqTM ((Complexity.TM.inputLenRegTM 0).seqTM (Complexity.TM.incRegTM 0))

def Complexity.WitnessBoundSetup.fresh {n : ℕ} (x : List Bool) : TapePred n

Ordinary fresh tapes before the witness-bound setup phase.

Equations

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

def Complexity.WitnessBoundSetup.ready {r : ℕ} (x : List Bool) (bound : ℕ) : TapePred (r + 1)

The setup preserves input and blank output, parks its scratch tapes, and places the exact unary witness bound on its last tape.

Equations

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

structure Complexity.WitnessBoundSetup (r : ℕ) (bound : ℕ → ℕ) : Type 1

A machine realizing a length-dependent finite witness bound. The final work tape is the counter, and the preceding r tapes are private setup scratch.

• machine : TM (r + 1)

  The ordinary deterministic setup machine.

• time : ℕ → ℕ

  Its initialized time budget.

• space : ℕ → ℕ

  Its initialized charged decision-space budget.

• prepares (x : List Bool) : self.machine.HoareTime (fresh x) (ready x (bound x.length)) (self.time x.length)

  A canonical parked frame, including the stored bound, at termination.

• withinSpace (x : List Bool) : self.machine.HoareSafety (fresh x) fun (inp : Tape) (work : Fin (r + 1) → Tape) (out : Tape) => { state := (), input := inp, work := work, output := out }.WithinDecisionSpace x.length (self.space x.length)

  Every reachable prefix, including output travel, is charged.