The time-hierarchy diagonalizer diagTM

The 8-tape machine D := diagTM clk at the heart of the time hierarchy theorem. On input x it:

1. builds the self-pair pair x x on work tape 7 (pairSelfTM);
2. decides TerminatedRegion x by a single input scan (termCheckTM); malformed inputs are routed to a fixed 0 output (writeTM Γw.zero);
3. for well-formed inputs: blanks the verdict cell (blankOutTM), builds the unary clock regTape (g |x|) on work tape 6 (the abstract clock-constructibility witness clk), runs the clocked universal machine on the self-pair (retargetInput clockedUtmTM), and finally negates output cell 1 (negOutTM) — accepting exactly when the simulated machine does not accept within g |x| steps.

Main definitions

• TM.ClockWitness — the body of ClockConstructible, named
• TM.blankOutTM — write □ at output cell 1, framing everything else
• TM.diagTM, TM.diagLang, TM.diagTime

Main results

• TM.clockConstructible_iff
• TM.diagTM_decidesInTime — diagTM clk decides diagLang clk in time diagTime C g
• TM.diagTM_flips — on terminated inputs whose interpreted machine halts within the clock budget, membership in diagLang clk is the negation of the simulated machine's acceptance
• TM.diagTime_le_poly — diagTime C g n ≤ (C + 786) * ((n+1)² * (g n + 1))

Implementation notes

Two landed specs do not quite fit and are bridged locally:

• writeTM writes □ under every work-tape head, which would corrupt the pair tape; blankOutTM (mirroring negOutTM) blanks output cell 1 while framing the input and all work tapes exactly.
• ClockWitness's postcondition only guarantees that the output tape is ▷-clean — not that it is restored to blank — so the landed clockedUtmTM_hoareTime_* (whose precondition demands a blank output tape) cannot be applied after clk. We re-derive them here with a merely ▷-clean output precondition (cleanUtmPre): initTM is output-idle, so its Hoare triple transports to any clean output tape by an output-swap simulation; every other ingredient already accepts a clean output tape.

def Complexity.TM.ClockWitness (tm : TM 8) (C : ℕ) (g : ℕ → ℕ) : Prop

The body of ClockConstructible, with the machine and constant exposed: tm writes the unary clock regTape (g |x|) on work tape 6 within C * (g |x| + |x| + 1) steps, framing the rest of the diagonalizer's tape layout. See ClockConstructible for the design discussion.

Equations

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

theorem Complexity.TM.clockConstructible_iff {g : ℕ → ℕ} : ClockConstructible g ↔ ∃ (tm : TM 8) (C : ℕ), tm.ClockWitness C g

ClockConstructible is exactly the existential closure of ClockWitness.

def Complexity.TM.blankOutTM {n : ℕ} : TM n

Replace output cell 1 with □ and halt with the output head parked at cell 1. Mirrors negOutTM exactly (rewind → right to cell 1 → write → halt); unlike writeTM, the input tape and all work tapes are exactly unchanged (readBackWrite writes and idleDir moves).

Equations

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

theorem Complexity.TM.blankOutTM_hoareTime {n : ℕ} (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (B : ℕ) (h0 : out₀.cells 0 = Γ.start) (hns : ∀ (j : ℕ), 1 ≤ j → out₀.cells j ≠ Γ.start) (hB : out₀.head ≤ B) (hinp : inp₀.read ≠ Γ.start) (hw : ∀ (i : Fin n), (work₀ i).read ≠ Γ.start) : blankOutTM.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out.cells = Function.update out₀.cells 1 Γ.blank ∧ out.head = 1) (B + 3)

blankOutTM specification (ghost form, exact frames). Starting from pinned tapes inp₀/work₀/out₀ with a well-formed output tape (cell 0 is ▷, no ▷ at cells ≥ 1, head ≤ B) and no tape head resting on ▷, blankOutTM halts within B + 3 steps having blanked output cell 1, all other output cells unchanged, output head parked at cell 1, and the input and work tapes exactly unchanged.

def Complexity.TM.diagTM (clk : TM 8) : TM 8

The time-hierarchy diagonalizer. Build pair x x on tape 7; check TerminatedRegion x (malformed inputs output 0); otherwise blank the verdict cell, build the clock regTape (g |x|) on tape 6 (clk), run the clocked universal machine on the self-pair, and negate output cell 1.

Equations

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

def Complexity.TM.diagLang (clk : TM 8) : Language

The language the diagonalizer decides: inputs on which it halts with 1 at output cell 1.

Equations

• clk.diagLang = {x : List Bool | ∃ (c : Complexity.Cfg 8 clk.diagTM.Q) (t : ℕ), clk.diagTM.reachesIn t (clk.diagTM.initCfg x) c ∧ clk.diagTM.halted c ∧ c.output.cells 1 = Complexity.Γ.one}

def Complexity.TM.diagTime (C : ℕ) (g : ℕ → ℕ) (n : ℕ) : ℕ

The diagonalizer's running-time bound (a closed form; see diagTime_le_poly for the clean polynomial bound).

Equations

• Complexity.TM.diagTime C g n = C * (g n + n + 1) + 2 * ((g n + 1) * (240 * (n + 1) ^ 2 + 10)) + 6 * g n + 65 * n + 215

theorem Complexity.TM.diagTM_decidesInTime (clk : TM 8) (C : ℕ) (g : ℕ → ℕ) (hclk : clk.ClockWitness C g) (hg1 : ∀ (n : ℕ), 1 ≤ g n) : clk.diagTM.DecidesInTime clk.diagLang (diagTime C g)

The diagonalizer decides its language in time diagTime C g. For any clock-constructibility witness (clk, C) for g ≥ 1, the machine diagTM clk decides diagLang clk within diagTime C g steps.

theorem Complexity.TM.diagTM_flips_of_halts (clk : TM 8) (C : ℕ) (g : ℕ → ℕ) (hclk : clk.ClockWitness C g) (x : List Bool) (hterm : UTMBody.TerminatedRegion x) (T : ℕ) (mcF : Cfg 1 (decodeDesc x).toTM.Q) (hT : T ≤ g x.length) (hrun : (decodeDesc x).toTM.reachesIn T ((decodeDesc x).toTM.initCfg x) mcF) (hhalt : (decodeDesc x).toTM.halted mcF) : x ∈ clk.diagLang ↔ mcF.output.cells 1 ≠ Γ.one

The diagonal flip. On a well-formed input x whose interpreted machine halts within the clock budget at mcF, the diagonalizer accepts x exactly when the interpreted machine does not.

theorem Complexity.TM.diagTM_flips (clk : TM 8) (C : ℕ) (g : ℕ → ℕ) (hclk : clk.ClockWitness C g) (hg1 : ∀ (n : ℕ), 1 ≤ g n) (x : List Bool) (hterm : UTMBody.TerminatedRegion x) (T : ℕ) (mcF : Cfg 1 (decodeDesc x).toTM.Q) (hT : T ≤ g x.length) (hrun : (decodeDesc x).toTM.reachesIn T ((decodeDesc x).toTM.initCfg x) mcF) (hhalt : (decodeDesc x).toTM.halted mcF) : x ∈ clk.diagLang ↔ mcF.output.cells 1 ≠ Γ.one

Compatibility form of diagTM_flips_of_halts. The positivity hypothesis is not needed for the flip itself, but remains in this public signature for callers of the original theorem.

theorem Complexity.TM.diagTime_le_poly (C : ℕ) (g : ℕ → ℕ) (n : ℕ) : diagTime C g n ≤ (C + 786) * ((n + 1) ^ 2 * (g n + 1))

Polynomial envelope for the diagonalizer's time bound: diagTime C g n ≤ (C + 786) * ((n + 1)² * (g n + 1)).