Finite replay of binary counting certificates

The checker uses the existing finite configuration representation and ordinary native actions. Its validity flag is an option: invalid indices and nonzero terminal padding fail, including for the rejecting classifier. The empty communication interface introduces no oracle resource. The machine, its finite control, number of tapes and block width are fixed; polynomial time is in the encoded input/certificate pair, not uniformly in a supplied machine description.

Main definitions

• Turing.MultiTapeCTM.Checker.indexStep: a finite-storage occurrence or canonical padding step.
• Turing.MultiTapeCTM.Checker.output: finite replay followed by a genuine halting check.
• Turing.MultiTapeCTM.Checker.checkBinary: the binary verifier for either terminal verdict.

Main results

• Turing.MultiTapeCTM.Checker.output_eq_decodeCertificate: exact native replay correspondence.
• Turing.MultiTapeCTM.Checker.checkBinary_eq_certificateAccepts: exact binary/index correspondence.
• Turing.MultiTapeCTM.Checker.computableTidilyInPolyTime_checkBinary: the actual checker is polynomial-time, using finite dispatch and a linear encoded-storage loop invariant.

References

The finite configuration, encoding and tidy calculus retain the source credits in their modules. Counting semantics and canonical padding are developed in MultiTape.Counting.Certificate.

@[reducible, inline]

abbrev Turing.MultiTapeCTM.Checker.Storage (k : ℕ) (State : Type) : Type

Existing finite native storage with no communication channels.

def Turing.MultiTapeCTM.Checker.localActions {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) (view : State × Option Bool × (Fin k → Option Bool)) : List (Action k Bool State)

Read the ordered transition occurrences from a fixed finite local view.

def Turing.MultiTapeCTM.Checker.indexStep {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) (finite : Storage k State) (index : ℕ) : Option (Storage k State)

One occurrence, or a forced zero after halting; failure is distinct from rejection.

def Turing.MultiTapeCTM.Checker.finish {k : ℕ} {State : Type} (finite : Storage k State) : Option (List Bool)

A completed replay returns output only when it genuinely halted.

def Turing.MultiTapeCTM.Checker.output {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) : Storage k State → List ℕ → Option (List Bool)

Replay all canonical occurrence indices using finite storage.

theorem Turing.MultiTapeCTM.Checker.localActions_eq_actions {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) {finite : Storage k State} {cfg : Cfg k Bool State finite.tapes.input} (h : finite.tapes.Represents cfg) {state : State} (hs : finite.tapes.state = some state) : localActions machine (state, finite.tapes.inputSymbol, finite.tapes.workTapeSymbols) = machine.actions cfg

Finite local views give the same ordered occurrences as a represented native configuration.

theorem Turing.MultiTapeCTM.Checker.output_eq_decodeCertificate {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) {finite : Storage k State} {cfg : Cfg k Bool State finite.tapes.input} (h : finite.tapes.Represents cfg) (indices : List ℕ) : output machine finite indices = Option.map (fun (r : List ℕ × Cfg k Bool State finite.tapes.input) => r.2.output) (machine.decodeCertificate cfg indices)

Finite-storage replay computes exactly the previously proved certificate decoder's output.

theorem Turing.MultiTapeCTM.Checker.computableTidilyInPolyTime_indexStep {k : ℕ} {State : Type} [Finite State] (machine : MultiTapeCTM k Bool State) : MultiTapeTM.ComputableTidilyInPolyTime (fun (p : Storage k State × ℕ) => indexStep machine p.1 p.2) (MultiTapeTM.encPair MultiTapeTM.encFiniteConfig MultiTapeTM.encUnary) (MultiTapeTM.encOption MultiTapeTM.encFiniteConfig)

The actual finite-storage transition checker is certified, including arbitrary invalid indices. Its fixed finite dispatch table is charged by the existing finite-domain compiler.

theorem Turing.MultiTapeCTM.Checker.indexStep_spaceBound {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) {finite next : Storage k State} {inputSize steps index : ℕ} (h : MultiTapeMachine.FiniteConfig.SpaceBound inputSize steps 0 finite) (hnext : indexStep machine finite index = some next) : MultiTapeMachine.FiniteConfig.SpaceBound inputSize (steps + 1) 0 next

A replay step retains the existing linear storage bound, including forced terminal padding.

@[reducible, inline]

abbrev Turing.MultiTapeCTM.Checker.Runtime (k : ℕ) (State : Type) : Type

The checker stores unconsumed bits and either a live finite replay or a permanent failure.

def Turing.MultiTapeCTM.Checker.binaryStep {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) (width : ℕ) (runtime : Runtime k State) : Runtime k State

Consume one fixed-width block and replay its occurrence index. The saturation cap is fixed; for a full block it equals ordinary binary decoding.

theorem Turing.MultiTapeCTM.Checker.computableTidilyInPolyTime_binaryStep {k : ℕ} {State : Type} [Finite State] (machine : MultiTapeCTM k Bool State) (width : ℕ) : MultiTapeTM.ComputableTidilyInPolyTime (binaryStep machine width) (MultiTapeTM.encPair MultiTapeTM.encBits (MultiTapeTM.encOption MultiTapeTM.encFiniteConfig)) (MultiTapeTM.encPair MultiTapeTM.encBits (MultiTapeTM.encOption MultiTapeTM.encFiniteConfig))

Execute one binary certificate block using the certified parser and finite replay step.

def Turing.MultiTapeCTM.Checker.initial {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) (p : List Bool × List Bool) : Runtime k State

Initialize the actual checker on an input word and a binary certificate.

def Turing.MultiTapeCTM.Checker.runBinary {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) (width : ℕ) (p : List Bool × List Bool) : Runtime k State

The fixed-width replay loop. A short final block remains unconsumed and is rejected later.

theorem Turing.MultiTapeCTM.Checker.computableTidilyInPolyTime_runBinary {k : ℕ} {State : Type} [Finite State] (machine : MultiTapeCTM k Bool State) (width : ℕ) : MultiTapeTM.ComputableTidilyInPolyTime (runBinary machine width) (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits) (MultiTapeTM.encPair MultiTapeTM.encBits (MultiTapeTM.encOption MultiTapeTM.encFiniteConfig))

The actual replay loop is polynomial-time. Its invariant charges the input, every work tape, output and remaining certificate; there is no assumed simulation or counting certificate.

theorem Turing.MultiTapeCTM.Checker.computableTidilyInPolyTime_finish {k : ℕ} {State : Type} [Finite State] : MultiTapeTM.ComputableTidilyInPolyTime finish MultiTapeTM.encFiniteConfig (MultiTapeTM.encOption MultiTapeTM.encBits)

Read the final output only after an actual simulated halt.

def Turing.MultiTapeCTM.Checker.finishRuntime {k : ℕ} {State : Type} (runtime : Runtime k State) : Option (List Bool)

A leftover partial block or an invalid/nonhalting replay has no output certificate.

theorem Turing.MultiTapeCTM.Checker.finishRuntime_iterate_binaryStep {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) {count width : ℕ} {word : List Bool} (h : word.length = count * width) (current : Option (Storage k State)) : finishRuntime ((binaryStep machine width)^[count] (word, current)) = current.bind fun (finite : Storage k State) => output machine finite (binaryIndices count width word)

On full-width certificates the actual loop is exactly the canonical index replay. Failure remains absorbing, so the equality also covers invalid occurrence indices and padding.

theorem Turing.MultiTapeCTM.Checker.finishRuntime_runBinary {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) {width count : ℕ} (hwidth : 0 < width) (input : List Bool) {word : List Bool} (hlen : word.length = count * width) : finishRuntime (runBinary machine width (input, word)) = Option.map (fun (r : List ℕ × Cfg k Bool State input) => r.2.output) (machine.decodeCertificate (Cfg.init machine.initial input) (binaryIndices count width word))

The compiled loop returns exactly the output of the canonical native decoder. The positive block width converts the supplied binary length into the declared number of machine steps.

theorem Turing.MultiTapeCTM.Checker.computableTidilyInPolyTime_finishRuntime {k : ℕ} {State : Type} [Finite State] : MultiTapeTM.ComputableTidilyInPolyTime finishRuntime (MultiTapeTM.encPair MultiTapeTM.encBits (MultiTapeTM.encOption MultiTapeTM.encFiniteConfig)) (MultiTapeTM.encOption MultiTapeTM.encBits)

def Turing.MultiTapeCTM.Checker.checkBinary {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) (width : ℕ) (verdict : Bool) (p : List Bool × List Bool) : Bool

The actual binary checker retains validity independently of its requested terminal verdict.

theorem Turing.MultiTapeCTM.Checker.checkBinary_eq_certificateAccepts {k : ℕ} {State : Type} (machine : MultiTapeCTM k Bool State) {width count : ℕ} (hwidth : 0 < width) (verdict : Bool) (input : List Bool) {word : List Bool} (hlen : word.length = count * width) : checkBinary machine width verdict (input, word) = machine.certificateAccepts (fun (out : List Bool) => (out == [true]) == verdict) (Cfg.init machine.initial input) (binaryIndices count width word)

Each terminal verdict uses the same exact validity condition as the canonical decoder.

theorem Turing.MultiTapeCTM.Checker.computableTidilyInPolyTime_checkBinary {k : ℕ} {State : Type} [Finite State] (machine : MultiTapeCTM k Bool State) (width : ℕ) (verdict : Bool) : MultiTapeTM.ComputableTidilyInPolyTime (checkBinary machine width verdict) (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits) MultiTapeTM.encBool

Both the accepting and rejecting binary verifiers are polynomial-time on every input pair.