Partrec Chain Alphabet Fragments

This file provides basic definitions and lemmas for working with the chain tape alphabet ChainΓ:

• γ'ToChainΓ and chainConsBottom: distinguished cells
• chainBinaryRepr: binary representation of natural numbers as ChainΓ cells
• Basic non-defaultness properties used by the direct code bridge

Key results

• chainConsBottom_ne_default: the cons-bottom marker is a valid nonblank cell.
• chainBinaryRepr_zero: zero is represented by the empty fragment.
• chainBinaryRepr_ne_default: every encoded natural-number cell is nonblank.

Instances

noncomputable instance instDecEqChainΓ' : DecidableEq ChainΓ

Equations

• instDecEqChainΓ' = instDecidableEqProd

Distinguished ChainΓ cells

noncomputable def γ'ToChainΓ (γ' : Turing.PartrecToTM2.Γ') : ChainΓ

Map a Γ' value to its corresponding ChainΓ cell (without bottom marker).

Equations

• γ'ToChainΓ γ' = (false, Function.update (fun (x : Turing.PartrecToTM2.K') => none) Turing.PartrecToTM2.K'.main (some γ'))

noncomputable def chainConsBottom : ChainΓ

The ChainΓ cell for the bottom marker with cons.

Equations

• chainConsBottom = (true, Function.update (fun (x : Turing.PartrecToTM2.K') => none) Turing.PartrecToTM2.K'.main (some Turing.PartrecToTM2.Γ'.cons))

theorem chainConsBottom_ne_default : chainConsBottom ≠ default

chainConsBottom is non-default.

Binary Representation

noncomputable def chainBinaryRepr (n : ℕ) : List ChainΓ

Binary representation of n as ChainΓ cells (LSB first, no markers).

Equations

• chainBinaryRepr n = List.map γ'ToChainΓ (Turing.PartrecToTM2.trNat n)

theorem chainBinaryRepr_zero : chainBinaryRepr 0 = []

chainBinaryRepr 0 is the empty list.

theorem chainBinaryRepr_ne_default (n : ℕ) (g : ChainΓ) : g ∈ chainBinaryRepr n → g ≠ default

All elements of chainBinaryRepr n are non-default.