Unary registers

A register is a work tape holding a natural number in unary: cells 1..v hold 1, everything beyond is blank, and the head is parked at cell 1. All arithmetic in the Cook–Levin reduction emitter (docs/A5-ReductionEmitter.md) is over registers — the CNF encoding is unary, so no binary arithmetic is ever needed.

IsReg strengthens Tape.HasUnaryCounter with the cell-0 sentinel and all-blanks-beyond, making registers literally preserved by parked no-op actions and stable under the combinator phase transitions.

Main definitions

• TM.Parked — a tape whose head is off ▷ and which has no spurious ▷s
• TM.IsReg — the register predicate

Main results

• TM.IsReg.parked, TM.IsReg.hasUnaryCounter — bridges
• TM.reg_zero_init_bumped — a freshly bumped blank tape is IsReg 0

def Complexity.TM.Parked (t : Tape) : Prop

A tape parked for preservation: head off ▷ (so idleDir stays put and δ_right_of_start is moot) and no ▷ outside cell 0 (so readBackWrite writes back the read symbol verbatim). Machines that do not use a tape keep it parked and literally unchanged.

Equations

• Complexity.TM.Parked t = (1 ≤ t.head ∧ ∀ (j : ℕ), 1 ≤ j → t.cells j ≠ Complexity.Γ.start)

theorem Complexity.TM.Parked.read_ne_start {t : Tape} (h : Parked t) : t.read ≠ Γ.start

A parked tape never reads the start symbol ▷.

theorem Complexity.TM.Parked.writeAndMove_readBack_idle {t : Tape} (h : Parked t) : t.writeAndMove (readBackWrite t.read).toΓ (idleDir t.read) = t

A parked tape is untouched by the no-op action writeAndMove (readBackWrite read) (idleDir read).

theorem Complexity.TM.Parked.move_idle {t : Tape} (h : Parked t) : t.move (idleDir t.read) = t

A parked tape's head does not move under idleDir.

theorem Complexity.TM.write_readBack (t : Tape) (hread : t.read ≠ Γ.start) : t.write (readBackWrite t.read).toΓ = t

Writing back the read symbol is a no-op (off ▷ the symbol round-trips; on ▷ the write is structurally void).

theorem Complexity.TM.writeAndMove_readBack (t : Tape) (hread : t.read ≠ Γ.start) (d : Dir3) : t.writeAndMove (readBackWrite t.read).toΓ d = t.move d

Writing back the read symbol and moving is just the move.

theorem Complexity.TM.Parked.transitionTape_eq_self {t : Tape} (h : Parked t) : transitionTape t = t

Parked tapes pass through combinator phase boundaries unchanged.

theorem Complexity.TM.Parked.transitionInput_eq_self {t : Tape} (h : Parked t) : transitionInput t = t

Parked input tapes pass through combinator phase boundaries unchanged.

def Complexity.TM.IsReg (v : ℕ) (t : Tape) : Prop

Register. The tape holds v in unary: ▷ at cell 0, 1 at cells 1..v, blank everywhere beyond, head parked at cell 1.

Equations

• Complexity.TM.IsReg v t = (t.head = 1 ∧ t.cells 0 = Complexity.Γ.start ∧ (∀ i < v, t.cells (i + 1) = Complexity.Γ.one) ∧ ∀ (j : ℕ), v + 1 ≤ j → t.cells j = Complexity.Γ.blank)

theorem Complexity.TM.IsReg.head_eq {v : ℕ} {t : Tape} (h : IsReg v t) : t.head = 1

A register tape's head is parked at cell 1.

theorem Complexity.TM.IsReg.cell0 {v : ℕ} {t : Tape} (h : IsReg v t) : t.cells 0 = Γ.start

A register tape's cell 0 holds the sentinel ▷.

theorem Complexity.TM.IsReg.cells_one {v : ℕ} {t : Tape} (h : IsReg v t) {i : ℕ} (hi : i < v) : t.cells (i + 1) = Γ.one

Cells 1..v of a register holding v contain 1.

theorem Complexity.TM.IsReg.cells_blank {v : ℕ} {t : Tape} (h : IsReg v t) {j : ℕ} (hj : v + 1 ≤ j) : t.cells j = Γ.blank

Cells beyond position v of a register holding v are blank.

theorem Complexity.TM.IsReg.cells_ne_start {v : ℕ} {t : Tape} (h : IsReg v t) {j : ℕ} (hj : 1 ≤ j) : t.cells j ≠ Γ.start

Register cells off the sentinel are 1 or blank — never ▷.

theorem Complexity.TM.IsReg.parked {v : ℕ} {t : Tape} (h : IsReg v t) : Parked t

A register tape is parked.

theorem Complexity.TM.IsReg.hasUnaryCounter {v : ℕ} {t : Tape} (h : IsReg v t) : t.HasUnaryCounter v

A register is a unary counter (the weaker shape used by the counter subroutines).

theorem Complexity.TM.IsReg.read_eq {v : ℕ} {t : Tape} (h : IsReg v t) : t.read = if v = 0 then Γ.blank else Γ.one

The register's read: 1 when nonempty, blank when zero.

theorem Complexity.TM.reg_zero_init_bumped : IsReg 0 { head := 1, cells := (Tape.init []).cells }

A blank tape with the head bumped to cell 1 is the zero register.

def Complexity.TM.regCells (v : ℕ) : ℕ → Γ

Canonical register cells holding v in unary.

Equations

• Complexity.TM.regCells v j = if j = 0 then Complexity.Γ.start else if j ≤ v then Complexity.Γ.one else Complexity.Γ.blank

def Complexity.TM.regTape (v : ℕ) : Tape

The canonical register tape holding v.

Equations

• Complexity.TM.regTape v = { head := 1, cells := Complexity.TM.regCells v }

@[simp]

theorem Complexity.TM.regT_head (v : ℕ) : (regTape v).head = 1

The canonical register tape's head sits at cell 1.

@[simp]

theorem Complexity.TM.regT_cells (v : ℕ) : (regTape v).cells = regCells v

The canonical register tape's cells are regCells v.

@[simp]

theorem Complexity.TM.regCells_zero (v : ℕ) : regCells v 0 = Γ.start

Cell 0 of the canonical register cells is the sentinel ▷.

theorem Complexity.TM.regCells_one {v j : ℕ} (h1 : 1 ≤ j) (h2 : j ≤ v) : regCells v j = Γ.one

Cells 1..v of the canonical register cells for v hold 1.

theorem Complexity.TM.regCells_blank {v j : ℕ} (h : v + 1 ≤ j) : regCells v j = Γ.blank

Cells beyond position v of the canonical register cells for v are blank.

theorem Complexity.TM.regCells_ne_start {v j : ℕ} (hj : 1 ≤ j) : regCells v j ≠ Γ.start

Register cells away from the sentinel are never ▷.

theorem Complexity.TM.reg_regT (v : ℕ) : IsReg v (regTape v)

The canonical register tape regTape v satisfies IsReg v.

theorem Complexity.TM.IsReg.eq_regT {v : ℕ} {t : Tape} (h : IsReg v t) : t = regTape v

A register's tape is canonical: the IsReg predicate pins every cell and the head, so it is an equation.

theorem Complexity.TM.parked_regTape (v : ℕ) : Parked (regTape v)

The canonical register tape is parked.

theorem Complexity.TM.parked_regCells {h v : ℕ} (hh : 1 ≤ h) : Parked { head := h, cells := regCells v }

Register cells with the head anywhere off ▷ form a parked tape.

theorem Complexity.TM.regCells_update_succ (d : ℕ) : Function.update (regCells d) (d + 1) Γ.one = regCells (d + 1)

Writing the next mark turns regCells d into regCells (d + 1).

theorem Complexity.TM.regCells_update_blank_succ (d : ℕ) : Function.update (regCells (d + 1)) (d + 1) Γ.blank = regCells d

Erasing the final mark turns regCells (d + 1) into regCells d.