Clock constructibility for the time hierarchy theorem

TM.ClockConstructible g is the constructibility hypothesis used by the proved time hierarchy theorem in Complexitylib.Classes.Hierarchy: an 8-tape machine can write the unary clock regTape (g n) on work tape 6 in time O(g n + n), ghost-preserving the rest of the diagonalizer's tape layout.

Contents:

1. TM.ClockConstructible — the layout-pinned definition (see its docstring for the design tradeoffs), plus the congruence helper ClockConstructible.congr.
2. TM.clockLenTM and TM.clockConstructible_succ — the base instance ClockConstructible (fun n => n + 1) via a single input sweep.
3. TM.moveClockTM, TM.clockMulTM and ClockConstructible.mul_succ — closure under multiplication by n + 1: move the clock to the scratch tape, then append it to the clock tape's frontier once per input position.
4. TM.clockConstructible_pow — ClockConstructible (fun n => (n + 1) ^ k) for all k ≥ 1: the polynomial clocks of the hierarchy theorem.

All machines are hand-written in the UTM house style (small inductive state, ghost-framed step/run lemmas as in UTM/Clock.lean and InputLen.lean).

theorem Complexity.TM.Tape.init_move_right_eq_regT_zero : (Tape.init []).move Dir3.right = regTape 0

The canonical parked blank tape (liftTM's pinned extra tape) is the zero register.

def Complexity.TM.ClockConstructible (g : ℕ → ℕ) : Prop

Clock constructibility — the hypothesis of the time hierarchy theorem. g is clock-constructible if some 8-tape machine, started on input x in the diagonalizer's tape layout, writes the unary register regTape (g |x|) on work tape 6 within C * (g |x| + |x| + 1) steps, disturbing nothing else.

The definition is deliberately layout-pinned rather than maximally general: the diagonalizer D is an 8-tape machine whose UTM phases run on tapes 0–5, whose encoded pair ⟨M, x⟩ lives on tape 7, and whose clock lives on tape 6. Instead of a lift-and-frame story, the hypothesis quantifies over the ghost frame work₀ directly:

• tapes 0–4 and 7 may hold arbitrary parked content (head ≥ 1, reading a non-▷ symbol) and must be preserved exactly;
• tape 6 (the clock) starts as the canonical parked blank tape (Tape.init []).move Dir3.right (the tape the liftTM combinators pin blank extras to; it equals regTape 0) and ends as regTape (g |x|);
• tape 5 is a designated scratch tape: it must also start blank, and it is restored blank — this is exactly the work i = work₀ i clause at i = 5, since work₀ 5 is pinned blank. D runs clock-initialization before any UTM phase touches tapes 0–5, so granting the clock machine one blank scratch tape costs nothing, and it makes the closure constructions (multiplication, hence all polynomials) feasible;
• the input tape is read-only, so only its cells are pinned; its head starts at cell 1 — the started form the combinator seams produce (transitionInput forces the input head to ≥ 1 at every phase boundary, so a head-0 input can never reach a mid-sequence phase) — and is returned to cell 1 (needed to chain clock phases sequentially);
• the output tape must be ▷-clean with head parked at cell 1, and is returned in the same state (clock machines never write the output).

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.ClockConstructible.congr {g g' : ℕ → ℕ} (h : ClockConstructible g) (hgg' : ∀ (n : ℕ), g n = g' n) : ClockConstructible g'

ClockConstructible respects pointwise-equal clock bounds.

def Complexity.TM.clockLenTM : TM 8

Measure the input length plus one into the clock tape: scan the input left to right writing one mark on tape 6 per bit, write one final mark at the input's first blank (the + 1), then rewind both heads to cell 1 in lockstep. Every other tape idles throughout.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.clockConstructible_succ : ClockConstructible fun (n : ℕ) => n + 1

The successor function is clock-constructible: clockLenTM writes |x| + 1 clock marks in a single input sweep, well within the 2 * (g n + n + 1) budget.

def Complexity.TM.moveClockTM : TM 8

Move the clock register to the scratch tape: sweep right over tape 6's marks, blanking each while writing a mark on tape 5 in lockstep, then rewind both heads to cell 1. From (regTape 0, regTape v) on tapes (5, 6) to (regTape v, regTape 0); every other tape idles throughout.

Equations

• One or more equations did not get rendered due to their size.

inductive Complexity.TM.MulPhase : Type

Control states of clockMulTM.

• drive : MulPhase
• inScan : MulPhase
• inRew : MulPhase
• rewC : MulPhase
• rew6 : MulPhase
• park : MulPhase
• done : MulPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqMulPhase : DecidableEq MulPhase

Equations

• Complexity.TM.instDecidableEqMulPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeMulPhase : Fintype MulPhase

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.clockMulTM : TM 8

Multiply the moved clock by |x| + 1: with regTape v on the scratch tape 5 and an empty clock tape 6 (head at its frontier, cell 1), run one round per scratch mark (drive consumes it): each round scans the input left to right appending one clock mark per bit plus one at the first blank (inScan), then rewinds the input head to cell 1 (inRew). The clock head never leaves its frontier, so each round costs 2|x| + 3 steps. After the last round the scratch is blanked while rewinding (rewC), the clock rewinds to cell 1 (rew6), and the machine parks: tape 5 is regTape 0 and tape 6 is regTape (v * (|x| + 1)).

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.ClockConstructible.mul_succ {g : ℕ → ℕ} (h : ClockConstructible g) : ClockConstructible fun (n : ℕ) => g n * (n + 1)

Closure under multiplication by n + 1. Run the g-clock, move its register to the scratch tape (moveClockTM), then append it to the clock tape's frontier once per input position (clockMulTM), producing regTape (g n * (n + 1)) in time O(g n * (n + 1) + n). This is where the designated scratch tape 5 earns its keep.

theorem Complexity.TM.clockConstructible_pow (k : ℕ) : 1 ≤ k → ClockConstructible fun (n : ℕ) => (n + 1) ^ k

Polynomial clocks: every positive power of n + 1 is clock-constructible — the clock family the time hierarchy theorem uses against polynomial time bounds.