Canonical certificates for labelled terminal branches

An occurrence-index certificate replays a list-choice machine until its first halt, then requires only zeros in the remaining positions. A running endpoint, out-of-range occurrence or nonzero terminal padding is invalid for both the accepting and rejecting classifiers.

Main definitions

• Turing.MultiTapeCTM.decodeCertificate: replay and validate an index certificate.
• Turing.MultiTapeCTM.padCertificate: uniquely pad a terminal trace to a fixed clock.
• Turing.MultiTapeCTM.certificateCount: count valid certificates with a specified verdict.

Main results

• Turing.MultiTapeCTM.padCertificate_bijOn: the actual padding map is a bijection between bounded terminal branches and all successful decoder inputs of the fixed length.
• Turing.MultiTapeCTM.certificateCounts_eq: both accepting and rejecting counts are preserved.

These are combinatorial results over natural-number indices. No polynomial-time binary checker, #P membership, reverse verifier-to-machine simulation or GapP characterization is proved here. Those require separate uniform constructions and resource proofs.

References

• L. Valiant, The complexity of computing the permanent
• S. Fenner, L. Fortnow, S. Kurtz, Gap-definable counting classes

The operational machine and occurrence semantics are those of MultiTape.Counting.

def Turing.MultiTapeCTM.decodeCertificate {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) : Cfg k Symbol State input → List ℕ → Option (List ℕ × Cfg k Symbol State input)

Decode occurrence indices, allowing only zero padding after the first halt. The result retains the consumed trace and final configuration. Invalid indices, nonzero terminal padding, and a running configuration at the end of the certificate all fail.

theorem Turing.MultiTapeCTM.decodeCertificate_of_halted {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) {cfg : Cfg k Symbol State input} (h : cfg.Halted) (word : List ℕ) : machine.decodeCertificate cfg word = if word = List.replicate word.length 0 then some ([], cfg) else none

theorem Turing.MultiTapeCTM.decodeCertificate_append_replicate {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) {cfg final : Cfg k Symbol State input} {choices : List ℕ} (hrun : machine.runBranch cfg choices = some final) (hhalt : final.Halted) (padding : ℕ) : machine.decodeCertificate cfg (choices ++ List.replicate padding 0) = some (choices, final)

Every terminal branch has exactly the intended all-zero padded certificate.

theorem Turing.MultiTapeCTM.decodeCertificate_sound {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) {cfg final : Cfg k Symbol State input} {word choices : List ℕ} (h : machine.decodeCertificate cfg word = some (choices, final)) : machine.runBranch cfg choices = some final ∧ final.Halted ∧ word = choices ++ List.replicate (word.length - choices.length) 0

Successful decoding gives a genuine first-halting branch, with uniquely forced padding.

theorem Turing.MultiTapeCTM.decodeCertificate_eq_some_iff {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg final : Cfg k Symbol State input) (word choices : List ℕ) : machine.decodeCertificate cfg word = some (choices, final) ↔ machine.runBranch cfg choices = some final ∧ final.Halted ∧ word = choices ++ List.replicate (word.length - choices.length) 0

Decoding is exact replay plus canonical zero padding, rather than an assumed counting certificate. Both acceptance and rejection can use its same validity condition.

def Turing.MultiTapeCTM.padCertificate (fuel : ℕ) (choices : List ℕ) : List ℕ

Pad a terminal occurrence trace to a fixed clock. Padding is not an actual machine step.

theorem Turing.MultiTapeCTM.padCertificate_injOn {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) (fuel : ℕ) : Set.InjOn (padCertificate fuel) ↑(machine.branches fuel cfg)

Canonical padding is injective on terminal branches, including branches of different lengths.

def Turing.MultiTapeCTM.certificates {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (fuel : ℕ) (cfg : Cfg k Symbol State input) : Finset (List ℕ)

The finite set of canonical fixed-length certificates. Its membership theorem identifies it with the independently defined decoder's successful inputs.

theorem Turing.MultiTapeCTM.mem_certificates_iff {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) (fuel : ℕ) (word : List ℕ) : word ∈ machine.certificates fuel cfg ↔ word.length = fuel ∧ (machine.decodeCertificate cfg word).isSome = true

theorem Turing.MultiTapeCTM.padCertificate_bijOn {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) (fuel : ℕ) : Set.BijOn (padCertificate fuel) ↑(machine.branches fuel cfg) {word : List ℕ | word.length = fuel ∧ (machine.decodeCertificate cfg word).isSome = true}

The actual trace-to-certificate map is a bijection onto all successful fixed-length decoder inputs. No extra copies are introduced by terminal padding or by distinct equal-effect choices.

theorem Turing.MultiTapeCTM.card_certificates {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (cfg : Cfg k Symbol State input) (fuel : ℕ) : (machine.certificates fuel cfg).card = (machine.branches fuel cfg).card

Canonical certificates and terminal branches have exactly the same cardinality.

def Turing.MultiTapeCTM.certificateAccepts {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (verdict : List Symbol → Bool) (cfg : Cfg k Symbol State input) (word : List ℕ) : Bool

The certificate classifier retains decoder validity for either terminal verdict. In particular, complementing the verdict still excludes every invalid certificate.

theorem Turing.MultiTapeCTM.certificateAccepts_of_invalid {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (verdict : List Symbol → Bool) {cfg : Cfg k Symbol State input} {word : List ℕ} (h : machine.decodeCertificate cfg word = none) : machine.certificateAccepts verdict cfg word = false

def Turing.MultiTapeCTM.certificateCount {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (verdict : List Symbol → Bool) (fuel : ℕ) (cfg : Cfg k Symbol State input) : ℕ

Count fixed-length canonical certificates with the specified terminal verdict.

theorem Turing.MultiTapeCTM.certificateCount_eq_branchCount {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (verdict : List Symbol → Bool) (fuel : ℕ) (cfg : Cfg k Symbol State input) : machine.certificateCount verdict fuel cfg = machine.branchCount verdict fuel cfg

The decoder's exact bijection preserves every terminal verdict, hence both accepting and rejecting counts. This is a combinatorial result, with no efficient binary checker claimed.

theorem Turing.MultiTapeCTM.certificateCounts_eq {k : ℕ} {State : Type u_2} (machine : MultiTapeCTM k Bool State) {input : List Bool} (fuel : ℕ) (cfg : Cfg k Bool State input) : machine.certificateCount (fun (x : List Bool) => x == [true]) fuel cfg = machine.acceptCount fuel cfg ∧ machine.certificateCount (fun (out : List Bool) => !out == [true]) fuel cfg = machine.rejectCount fuel cfg

The two valid-certificate classifiers recover the accepting and rejecting machine counts separately; invalid certificates contribute to neither side.