Ordinary finite verifiers compiled to witness machines

The compiler first realizes the witness bound on ordinary tapes, then stores a finite certificate, builds a canonical pair, and runs the ordinary verifier. Setup scratch and verifier scratch are separate blocks. Only the external source stream is uncharged; the stored certificate and paired input are charged.

def Complexity.WitnessTM.ofDeterministic {k : ℕ} (M : TM k) : WitnessTM k

A deterministic phase that leaves the external source stream untouched.

Equations

• Complexity.WitnessTM.ofDeterministic M = { machine := M.liftLast, advancing := fun (x : M.liftLast.Q) => false, protocol := ⋯ }

def Complexity.WitnessTM.seq {k : ℕ} (A B : WitnessTM k) : WitnessTM k

Compose two witness phases with the standard one-step handoff.

Equations

• A.seq B = { machine := A.machine.seqTM B.machine, advancing := Complexity.TM.seqAdv A.advancing B.advancing, protocol := ⋯ }

@[reducible, inline]

abbrev Complexity.WitnessTM.Verifier.tapes (r k : ℕ) : ℕ

Charged tape count: private setup block, verifier work, pair, and certificate.

Equations

• Complexity.WitnessTM.Verifier.tapes r k = r + 1 + (k + 2)

def Complexity.WitnessTM.Verifier.counterIdx (r k : ℕ) : Fin (tapes r k)

The unary counter remains at the end of the setup's private block.

Equations

• Complexity.WitnessTM.Verifier.counterIdx r k = Fin.castAdd (k + 2) (Fin.last r)

def Complexity.WitnessTM.Verifier.pairIdx (r k : ℕ) : Fin (tapes r k)

The paired virtual input follows the verifier's own work tapes.

Equations

• Complexity.WitnessTM.Verifier.pairIdx r k = (Fin.last (r + 1 + k)).castSucc

def Complexity.WitnessTM.Verifier.witnessIdx (r k : ℕ) : Fin (tapes r k)

The stored finite certificate uses the final charged tape.

Equations

• Complexity.WitnessTM.Verifier.witnessIdx r k = Fin.last (r + 1 + (k + 1))

def Complexity.WitnessTM.Verifier.window (bound resource : ℕ → ℕ) (n : ℕ) : ℕ

The finite maximum accommodates time and space bounds without monotonicity.

Equations

• Complexity.WitnessTM.Verifier.window bound resource n = (Finset.range (bound n + 1)).sup fun (m : ℕ) => resource (2 * n + 2 + m)

def Complexity.WitnessTM.Verifier.time {r : ℕ} {bound : ℕ → ℕ} (setup : WitnessBoundSetup r bound) (T : ℕ → ℕ) (n : ℕ) : ℕ

Exact phase-budget expression; all setup and handoff costs are included.

Equations

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

def Complexity.WitnessTM.Verifier.space {r : ℕ} {bound : ℕ → ℕ} (setup : WitnessBoundSetup r bound) (S : ℕ → ℕ) (n : ℕ) : ℕ

Conservative phase-space budget, including stored certificate, relocated input, setup scratch, and output travel, but no verifier-time contribution.

Equations

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

def Complexity.WitnessTM.Verifier.language (bound : ℕ → ℕ) (L₀ : Language) : Language

The bounded existential language of an ordinary paired-input verifier.

Equations

• Complexity.WitnessTM.Verifier.language bound L₀ = {x : List Bool | ∃ (y : List Bool), y.length ≤ bound x.length ∧ Complexity.pair x y ∈ L₀}

def Complexity.WitnessTM.Verifier.suffix {k : ℕ} (r : ℕ) (M : TM k) : TM (tapes r k)

Once a certificate is stored, pair construction and verification are ordinary deterministic phases with no further witness-stream access.

Equations

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

def Complexity.WitnessTM.Verifier.guessPrefix {r : ℕ} {bound : ℕ → ℕ} (setup : WitnessBoundSetup r bound) (k : ℕ) : WitnessTM (tapes r k)

The only witness-consuming prefix: realize the numeric bound, then store a finite certificate. Later verification can reread that charged copy freely.

Equations

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

def Complexity.WitnessTM.Verifier.compile {r : ℕ} {bound : ℕ → ℕ} {k : ℕ} (setup : WitnessBoundSetup r bound) (M : TM k) : WitnessTM (tapes r k)

The ordinary finite-verifier compiler. Every data-bearing intermediate tape is charged; the sole free tape provides online choices for materialization.

Equations

• Complexity.WitnessTM.Verifier.compile setup M = (Complexity.WitnessTM.Verifier.guessPrefix setup k).seq (Complexity.WitnessTM.ofDeterministic (Complexity.WitnessTM.Verifier.suffix r M))