Native parsimonious guess-and-verify machines

The witness-length routine, binary scanner, framed input writer and deterministic verifier are actual finite native machines. Singleton lifting and the shared compilers retain every occurrence. Polynomial clocks include the unary length computation, framing, buffer preparation and tidy workspace restoration. The contracts concern encoded instances; no behavior on words outside the instance encoding is asserted.

Main results

• Turing.MultiTapeCTM.exists_guess_machine: one occurrence per polynomial-length witness.
• Turing.MultiTapeCTM.exists_framedGuess_machine: retain the instance in the verifier encoding.
• Turing.MultiTapeCTM.exists_verifier_machine: one Boolean result occurrence per witness.

References

The guess-and-verify construction is standard in counting complexity [Val79b]. Native tidy machines and their calculus are by Christian Reitwiessner and Samuel Schlesinger. The captured-input construction follows Computability.Probabilistic.PPT.Capture, with source credit recorded there; the present singleton lift retains exact occurrence multiplicity.

theorem Turing.MultiTapeCTM.exists_guess_machine {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapeCTM k Bool State) (clock : Polynomial ℕ), machine.Nonblocking ∧ ∀ (a : α), machine.HaltsWithin (Polynomial.eval (enc a).length clock) (MultiTapeMachine.initialConfig machine (enc a)).tapes ∧ (List.map Cfg.output (machine.runList (Polynomial.eval (enc a).length clock) (MultiTapeMachine.initialConfig machine (enc a)).tapes)).Perm (Cslib.BitString.enumList (Polynomial.eval (enc a).length p))

Compute the witness length in unary and run the actual binary scanner. The finite machine is fixed before the instance is supplied, and emits each witness once, including the empty word.

theorem Turing.MultiTapeCTM.exists_framedGuess_machine {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapeCTM k Bool State) (clock : Polynomial ℕ), machine.Nonblocking ∧ ∀ (a : α), machine.HaltsWithin (Polynomial.eval (enc a).length clock) (MultiTapeMachine.initialConfig machine (enc a)).tapes ∧ (List.map Cfg.output (machine.runList (Polynomial.eval (enc a).length clock) (MultiTapeMachine.initialConfig machine (enc a)).tapes)).Perm (List.map (fun (word : List Bool) => (MultiTapeTM.encPair enc MultiTapeTM.encBits) (a, word)) (Cslib.BitString.enumList (Polynomial.eval (enc a).length p)))

A tidy frame writer surrounds the complete guessing computation, so the scanner still reads only the unary witness length. Every output is exactly the verifier's framed pair encoding.

theorem Turing.MultiTapeCTM.exists_verifier_machine {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) (verifier : α × List Bool → Bool) (hverify : MultiTapeTM.ComputableTidilyInPolyTime verifier (MultiTapeTM.encPair enc MultiTapeTM.encBits) MultiTapeTM.encBool) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapeCTM k Bool State) (clock : Polynomial ℕ), machine.Nonblocking ∧ ∀ (a : α), machine.HaltsWithin (Polynomial.eval (enc a).length clock) (MultiTapeMachine.initialConfig machine (enc a)).tapes ∧ (List.map Cfg.output (machine.runList (Polynomial.eval (enc a).length clock) (MultiTapeMachine.initialConfig machine (enc a)).tapes)).Perm (List.map (fun (word : List Bool) => MultiTapeTM.encBool (verifier (a, word))) (Cslib.BitString.enumList (Polynomial.eval (enc a).length p)))

Run the native verifier once for each witness. Equal Boolean outcomes retain separate List occurrences; all branches halt at one polynomial clock in the original encoded input length.