Fixed-width binary certificates for labelled branches

Each occurrence index occupies one fixed-width binary block. The width is fixed by the machine, not by its input. Distinct indices remain distinct even when their actions or successors agree.

Main definitions

• Turing.MultiTapeCTM.binaryCertificate: concatenate the fixed-width index codes.
• Turing.MultiTapeCTM.binaryIndices: read a fixed number of binary blocks as indices.

Main results

• Turing.MultiTapeCTM.binaryIndices_binaryCertificate: decoding the code recovers its indices.
• Turing.MultiTapeCTM.binaryCertificate_binaryIndices: full-width words are recovered exactly.
• Turing.MultiTapeCTM.decodeCertificate_indices_lt: a transition-list bound also bounds every index in a successful canonical certificate, including terminal padding.

References

The binary representation is the existing Cslib.BitString.binaryWord; its module records the original formalization credit. The occurrence and padding semantics are MultiTape.Counting and MultiTape.Counting.Certificate.

def Turing.MultiTapeCTM.binaryCertificate (width : ℕ) (indices : List ℕ) : List Bool

Encode each occurrence index as one fixed-width block, in chronological order.

def Turing.MultiTapeCTM.binaryIndices (count width : ℕ) (word : List Bool) : List ℕ

Decode a specified number of fixed-width blocks using the existing bit-string row view.

@[simp]

theorem Turing.MultiTapeCTM.length_binaryIndices (count width : ℕ) (word : List Bool) : (binaryIndices count width word).length = count

theorem Turing.MultiTapeCTM.length_binaryCertificate {width : ℕ} {indices : List ℕ} (h : ∀ index ∈ indices, index < 2 ^ width) : (binaryCertificate width indices).length = indices.length * width

Bounded indices each contribute exactly one full block.

theorem Turing.MultiTapeCTM.binaryIndices_binaryCertificate {width : ℕ} {indices : List ℕ} (h : ∀ index ∈ indices, index < 2 ^ width) : binaryIndices indices.length width (binaryCertificate width indices) = indices

Encoding followed by block decoding preserves every bounded occurrence index.

theorem Turing.MultiTapeCTM.binaryCertificate_binaryIndices {count width : ℕ} {word : List Bool} (h : word.length = count * width) : binaryCertificate width (binaryIndices count width word) = word

Decoding and re-encoding a full-width word preserves all bits, including leading zeros.

theorem Turing.MultiTapeCTM.runBranch_indices_lt {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) {bound : ℕ} (hbound : ∀ (cfg : Cfg k Symbol State input), (machine.actions cfg).length ≤ bound) {cfg final : Cfg k Symbol State input} {choices : List ℕ} (hrun : machine.runBranch cfg choices = some final) (index : ℕ) : index ∈ choices → index < bound

Every used index is below the occurrence-list bound, without identifying equal successors.

theorem Turing.MultiTapeCTM.decodeCertificate_indices_lt {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) {bound : ℕ} (hpos : 0 < bound) (hbound : ∀ (cfg : Cfg k Symbol State input), (machine.actions cfg).length ≤ bound) {cfg final : Cfg k Symbol State input} {word choices : List ℕ} (hdecode : machine.decodeCertificate cfg word = some (choices, final)) (index : ℕ) : index ∈ word → index < bound

The same positive bound covers actual indices and the forced zero padding after halting.