Heads that idle never drift outward

Space accounting for the phase machinery of the combinators rests on one fact. Between phases, and throughout the rewind and check phases, every tape is moved by idleDir — and on a tape carrying its left marker that sends the head to exactly max head 1: it bounces off cell 0 and otherwise stands still. So however many steps a rewind takes, no head drifts outward, and a space bound established before the phase survives it with no additive slack.

The output tape is the exception: it is walked left to the marker and then one cell right, which is still within max head 1.

Main results

• TM.head_writeAndMove_idleDir_le_max — an idle write-and-move stays within max head 1
• TM.seq_head_bound — the step seqTM interposes between its two simulations idles every tape
• TM.loop_head_bound — every phase of loopTM outside the two simulations keeps every head within max head 1
• TM.if_head_bound — the same for ifTM
• TM.loop_idle_step_state, TM.if_idle_step_state — an interposed step lands only at another interposed phase or at a start state
• TM.loopTM_rewind_loop_frame — the rewind phase of loopTM leaves the input and work tapes identical, heads included

theorem Complexity.TM.head_move_le_max (t : Tape) (d : Dir3) (hd : d = Dir3.right → t.head = 0) : (t.move d).head ≤ max t.head 1

A head that only ever moves right off the left marker stays within max head 1.

theorem Complexity.TM.head_writeAndMove_le_max (t : Tape) (w : Γw) (d : Dir3) (hd : d = Dir3.right → t.head = 0) : (t.writeAndMove w.toΓ d).head ≤ max t.head 1

The same for a write followed by a move: writing does not move the head.

theorem Complexity.TM.head_move_idleDir_le_max {t : Tape} (h : t.StartInvariant) : (t.move (idleDir t.read)).head ≤ max t.head 1

An idle move never leaves max head 1.

theorem Complexity.TM.head_writeAndMove_idleDir_le_max (t : Tape) (w : Γw) (h : t.StartInvariant) : (t.writeAndMove w.toΓ (idleDir t.read)).head ≤ max t.head 1

An idle write-and-move never leaves max head 1.

theorem Complexity.TM.seq_head_bound {n : ℕ} (tm₁ tm₂ : TM n) {c c' : Cfg n (tm₁.seqTM tm₂).Q} (hstate : c.state = Sum.inl tm₁.qhalt) (hstep : (tm₁.seqTM tm₂).step c = some c') (hinp : c.input.StartInvariant) (hwork : ∀ (i : Fin n), (c.work i).StartInvariant) (hout : c.output.StartInvariant) : c'.input.head ≤ max c.input.head 1 ∧ (∀ (i : Fin n), (c'.work i).head ≤ max (c.work i).head 1) ∧ c'.output.head ≤ max c.output.head 1

The single step seqTM interposes between its two simulations idles every tape.

theorem Complexity.TM.loop_head_bound {n : ℕ} (tmBody tmTest : TM n) {c c' : Cfg n (tmBody.loopTM tmTest).Q} (hbody : ∀ (q : tmBody.Q), c.state = Sum.inl q → q = tmBody.qhalt) (htest : ∀ (q : tmTest.Q), c.state = Sum.inr (Sum.inr q) → q = tmTest.qhalt) (hstep : (tmBody.loopTM tmTest).step c = some c') (hinp : c.input.StartInvariant) (hwork : ∀ (i : Fin n), (c.work i).StartInvariant) (hout : c.output.StartInvariant) : c'.input.head ≤ max c.input.head 1 ∧ (∀ (i : Fin n), (c'.work i).head ≤ max (c.work i).head 1) ∧ c'.output.head ≤ max c.output.head 1

Outside its two simulation phases, loopTM never grows a head beyond max head 1. The phase transitions and the rewind and check phases all idle the input and work tapes, and move the output head right only off the left marker.

theorem Complexity.TM.if_head_bound {n : ℕ} (tmTest tmThen tmElse : TM n) {c c' : Cfg n (tmTest.ifTM tmThen tmElse).Q} (ht : ∀ (q : tmTest.Q), c.state = Sum.inl q → q = tmTest.qhalt) (hthen : ∀ (q : tmThen.Q), c.state = Sum.inr (Sum.inr (Sum.inl q)) → q = tmThen.qhalt) (helse : ∀ (q : tmElse.Q), c.state = Sum.inr (Sum.inr (Sum.inr q)) → q = tmElse.qhalt) (hstep : (tmTest.ifTM tmThen tmElse).step c = some c') (hinp : c.input.StartInvariant) (hwork : ∀ (i : Fin n), (c.work i).StartInvariant) (hout : c.output.StartInvariant) : c'.input.head ≤ max c.input.head 1 ∧ (∀ (i : Fin n), (c'.work i).head ≤ max (c.work i).head 1) ∧ c'.output.head ≤ max c.output.head 1

Outside its three simulation phases, ifTM never grows a head beyond max head 1.

theorem Complexity.TM.if_idle_step_state {n : ℕ} (tmTest tmThen tmElse : TM n) {c c' : Cfg n (tmTest.ifTM tmThen tmElse).Q} (ht : ∀ (q : tmTest.Q), c.state = Sum.inl q → q = tmTest.qhalt) (hthen : ∀ (q : tmThen.Q), c.state = Sum.inr (Sum.inr (Sum.inl q)) → q = tmThen.qhalt) (helse : ∀ (q : tmElse.Q), c.state = Sum.inr (Sum.inr (Sum.inr q)) → q = tmElse.qhalt) (hstep : (tmTest.ifTM tmThen tmElse).step c = some c') : (∃ (ph : IfPhase), c'.state = Sum.inr (Sum.inl ph)) ∨ c'.state = Sum.inr (Sum.inr (Sum.inl tmThen.qstart)) ∨ c'.state = Sum.inr (Sum.inr (Sum.inr tmElse.qstart))

Outside its three simulations, ifTM steps only to an interposed phase or to a branch's start state.

theorem Complexity.TM.loop_phase_step_state {n : ℕ} (tmBody tmTest : TM n) {c c' : Cfg n (tmBody.loopTM tmTest).Q} {ph : LoopPhase} (hstate : c.state = Sum.inr (Sum.inl ph)) (hstep : (tmBody.loopTM tmTest).step c = some c') : (∃ (ph' : LoopPhase), c'.state = Sum.inr (Sum.inl ph')) ∨ c'.state = Sum.inl tmBody.qstart

From one of the interposed phases, loopTM moves either to another such phase or back to the body's start state.

theorem Complexity.TM.loop_idle_step_state {n : ℕ} (tmBody tmTest : TM n) {c c' : Cfg n (tmBody.loopTM tmTest).Q} (hb : ∀ (q : tmBody.Q), c.state = Sum.inl q → q = tmBody.qhalt) (ht : ∀ (q : tmTest.Q), c.state = Sum.inr (Sum.inr q) → q = tmTest.qhalt) (hstep : (tmBody.loopTM tmTest).step c = some c') : (∀ (q : tmBody.Q), c'.state = Sum.inl q → q = tmBody.qstart) ∧ ∀ (q : tmTest.Q), c'.state = Sum.inr (Sum.inr q) → q = tmTest.qstart

An interposed step lands at a start state or at another interposed phase. So the only way back into the body or the test is through their start states — which is what lets a loop invariant be re-established once per iteration.

The rewind phase leaves the input and work tapes alone

theorem Complexity.TM.loop_rewind_step_left_frame {n : ℕ} (tmBody tmTest : TM n) (c : Cfg n (tmBody.loopTM tmTest).Q) (hstate : c.state = Sum.inr (Sum.inl LoopPhase.rewindOut)) (hread_ne : c.output.read ≠ Γ.start) (_hc0 : c.output.cells 0 = Γ.start) (_hns : ∀ j ≥ 1, c.output.cells j ≠ Γ.start) (hih : c.input.head ≥ 1) (hins : ∀ j ≥ 1, c.input.cells j ≠ Γ.start) (hwh : ∀ (i : Fin n), (c.work i).head ≥ 1) (hwns : ∀ (i : Fin n), ∀ j ≥ 1, (c.work i).cells j ≠ Γ.start) : ∃ (c' : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).step c = some c' ∧ c'.state = Sum.inr (Sum.inl LoopPhase.rewindOut) ∧ c'.output.head = c.output.head - 1 ∧ c'.output.cells = c.output.cells ∧ c'.input = c.input ∧ c'.work = c.work

One leftward rewind step of loopTM, framed: the input and work tapes are untouched.

theorem Complexity.TM.loop_rewind_step_base_frame {n : ℕ} (tmBody tmTest : TM n) (c : Cfg n (tmBody.loopTM tmTest).Q) (hstate : c.state = Sum.inr (Sum.inl LoopPhase.rewindOut)) (hread : c.output.read = Γ.start) (_hc0 : c.output.cells 0 = Γ.start) (hnostart : ∀ j ≥ 1, c.output.cells j ≠ Γ.start) (hih : c.input.head ≥ 1) (hins : ∀ j ≥ 1, c.input.cells j ≠ Γ.start) (hwh : ∀ (i : Fin n), (c.work i).head ≥ 1) (hwns : ∀ (i : Fin n), ∀ j ≥ 1, (c.work i).cells j ≠ Γ.start) : ∃ (c' : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).step c = some c' ∧ c'.state = Sum.inr (Sum.inl LoopPhase.check) ∧ c'.output.head = 1 ∧ c'.output.cells = c.output.cells ∧ c'.input = c.input ∧ c'.work = c.work

The final rewind step of loopTM, framed.

theorem Complexity.TM.loopTM_rewind_loop_frame {n : ℕ} (tmBody tmTest : TM n) (p : ℕ) (c : Cfg n (tmBody.loopTM tmTest).Q) (hstate : c.state = Sum.inr (Sum.inl LoopPhase.rewindOut)) (hc0 : c.output.cells 0 = Γ.start) (hns : ∀ j ≥ 1, c.output.cells j ≠ Γ.start) (hp : c.output.head = p) (hih : c.input.head ≥ 1) (hins : ∀ j ≥ 1, c.input.cells j ≠ Γ.start) (hwh : ∀ (i : Fin n), (c.work i).head ≥ 1) (hwns : ∀ (i : Fin n), ∀ j ≥ 1, (c.work i).cells j ≠ Γ.start) : ∃ (c_check : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).reachesIn (p + 1) c c_check ∧ c_check.state = Sum.inr (Sum.inl LoopPhase.check) ∧ c_check.output.head = 1 ∧ c_check.output.cells = c.output.cells ∧ c_check.input = c.input ∧ c_check.work = c.work

The rewind phase of loopTM, framed. From rewindOut with the output head at p, the machine reaches check in p + 1 steps with the output head at cell 1, the output cells unchanged, and the input and work tapes identical — heads included. This is what lets a loop invariant on the work tapes survive the phase and be re-established for the next iteration.