Output negation phase: negOutTM

The last phase of the time-hierarchy diagonalizer replaces output cell 1 with the binary negation of "cell 1 = 1": 1 ↦ 0, and anything else (0 or □) ↦ 1. (The complementTM/flipBit machinery maps □ ↦ □, which is not binary — hence this machine.)

Behavior

Mirrors writeTM: from qstart,

• rewind: move the output head left until it reads ▷, then right once (to cell 1). All other tapes idle.
• goRight: one buffer step at cell 1, preserving its contents (unlike writeTM, which blanks it — here the next step must still read it).
• write: read output cell 1 and overwrite it with its binary negation.
• done: halt, parked at output cell 1.

The input tape and all work tapes are exactly unchanged (readBackWrite writes and idleDir moves); the output cells are unchanged except cell 1.

Main definitions

• TM.negOutTM — the output-negating machine

Main results

• TM.negOutTM_hoareTime — ghost-style Hoare-time specification: with the initial tapes pinned as inp₀/work₀/out₀, the machine halts within B + 3 steps (B bounding the initial output head) with out.cells = Function.update out₀.cells 1 (if out₀.cells 1 = Γ.one then Γ.zero else Γ.one), the output head parked at cell 1, and inp = inp₀, work = work₀.

inductive Complexity.TM.NegOutPhase : Type

Control states of negOutTM (mirrors WritePhase).

• rewind : NegOutPhase
• goRight : NegOutPhase
• write : NegOutPhase
• done : NegOutPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqNegOutPhase : DecidableEq NegOutPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeNegOutPhase : Fintype NegOutPhase

Equations

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

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

Replace output cell 1 with the binary negation of "cell 1 = 1" (1 ↦ 0; anything else ↦ 1) and halt with the output head parked at cell 1. Phases: rewind output to ▷ → right to cell 1 → read-and-negate → halt. The input tape and all work tapes are exactly unchanged.

Equations

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

theorem Complexity.TM.negOutTM_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) : negOutTM.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 (if out₀.cells 1 = Γ.one then Γ.zero else Γ.one) ∧ out.head = 1) (B + 3)

negOutTM 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 ▷, negOutTM halts within B + 3 steps having replaced output cell 1 with the binary negation of "cell 1 = 1" (1 ↦ 0; 0/□ ↦ 1), all other output cells unchanged, output head parked at cell 1, and the input and work tapes exactly unchanged.