Body machine: peek, default-move, and apply phases

Phase lemmas for the body machine's interaction with the three virtual tapes (the +1-shift shadows of the simulated input/work/output tapes, VTape.lean):

• peek_correct — the two-step peek captures the at-origin flags and restores all tapes exactly;
• segCheck_default_step / segCheck_continue_step — the no-match branch's sanitized default moves (trick 4) and the ordinary continue step;
• appQ'_loop — the overwrite copy of the new state from scratch onto the state tape (trick 2);
• appAct_all — the ten-step decode of the five 2-cell action groups (trick 6), transforming the three virtual tapes exactly as one sanitized simulated action.

grpΓw_eq_decΓw / grpDir_eq_decDir bridge the machine's 2-bit group decoders to the description decoders in Desc.lean.

theorem Complexity.TM.UTMBody.grpΓw_eq_decΓw (b₀ b₁ : Bool) : grpΓw b₀ b₁ = decΓw [b₀, b₁]

The machine's 2-bit write-symbol decoder agrees with decΓw.

theorem Complexity.TM.UTMBody.grpDir_eq_decDir (b₀ b₁ : Bool) : grpDir b₀ b₁ = decDir [b₀, b₁]

The machine's 2-bit direction decoder agrees with decDir.

theorem Complexity.TM.UTMBody.peek_correct {c : Cfg 6 bodyTM.Q} {sim0 sim1 sim2 : Tape} (h0 : VShift sim0 (c.work vIn)) (h1 : VShift sim1 (c.work vWk)) (h2 : VShift sim2 (c.work vOut)) (hwf0 : sim0.StartInvariant) (hwf1 : sim1.StartInvariant) (hwf2 : sim2.StartInvariant) (hst : c.state = BodyQ.peek1) (hstT : (c.work stT).read ≠ Γ.start) (hdsT : (c.work dsT).read ≠ Γ.start) (hscT : (c.work scT).read ≠ Γ.start) (hin : c.input.read ≠ Γ.start) (hout : c.output.read ≠ Γ.start) : ∃ (c' : Cfg 6 bodyTM.Q), bodyTM.reachesIn 2 c c' ∧ c'.state = BodyQ.seek1 (decide (sim0.head = 0), decide (sim1.head = 0), decide (sim2.head = 0)) ∧ c'.work vIn = c.work vIn ∧ c'.work vWk = c.work vWk ∧ c'.work vOut = c.work vOut ∧ c'.work stT = c.work stT ∧ c'.work dsT = c.work dsT ∧ c'.work scT = c.work scT ∧ c'.input = c.input ∧ c'.output = c.output

The peek phase (peek1 → peek2 → seek1 f): in two steps the body machine captures the at-origin flags of the three virtual tapes and restores every tape exactly. The flags are honest: the machine proceeds to seek1 (decide (sim0.head = 0), decide (sim1.head = 0), decide (sim2.head = 0)).

theorem Complexity.TM.UTMBody.segCheck_default_step {c : Cfg 6 bodyTM.Q} {f : VFlags} {sim0 sim1 sim2 : Tape} (h0 : VShift sim0 (c.work vIn)) (h1 : VShift sim1 (c.work vWk)) (h2 : VShift sim2 (c.work vOut)) (hwf0 : sim0.StartInvariant) (hwf1 : sim1.StartInvariant) (hwf2 : sim2.StartInvariant) (hf0 : f.1 = decide (sim0.head = 0)) (hf1 : f.2.1 = decide (sim1.head = 0)) (hf2 : f.2.2 = decide (sim2.head = 0)) (hst : c.state = BodyQ.segCheck f) (hdc : (c.work dsT).read = Γ.blank) (hstT : (c.work stT).read ≠ Γ.start) (hscT : (c.work scT).read ≠ Γ.start) (hin : c.input.read ≠ Γ.start) (hout : c.output.read ≠ Γ.start) : ∃ (c' : Cfg 6 bodyTM.Q), bodyTM.reachesIn 1 c c' ∧ c'.state = BodyQ.dfScr ∧ VShift (sim0.move (if f.1 = true then Dir3.right else Dir3.stay)) (c'.work vIn) ∧ VShift (sim1.move (if f.2.1 = true then Dir3.right else Dir3.stay)) (c'.work vWk) ∧ VShift (sim2.move (if f.2.2 = true then Dir3.right else Dir3.stay)) (c'.work vOut) ∧ c'.work stT = c.work stT ∧ c'.work dsT = c.work dsT ∧ c'.work scT = c.work scT ∧ c'.input = c.input ∧ c'.output = c.output

The no-match default step (segCheck f reading □ → dfScr, trick 4): one step applies the default action's sanitized moves to the three virtual tapes — right where the at-origin flag is set, stay otherwise — matching the interpreted machine's sanitized stay directions. All writes are read-backs; every other tape is preserved exactly.

theorem Complexity.TM.UTMBody.segCheck_continue_step {c : Cfg 6 bodyTM.Q} {f : VFlags} (hst : c.state = BodyQ.segCheck f) (hdc : (c.work dsT).read ≠ Γ.blank) (hparked : ∀ (i : Fin 6), (c.work i).read ≠ Γ.start) (hin : c.input.read ≠ Γ.start) (hout : c.output.read ≠ Γ.start) : ∃ (c' : Cfg 6 bodyTM.Q), bodyTM.reachesIn 1 c c' ∧ c'.state = BodyQ.mmScr f ∧ (∀ (i : Fin 6), c'.work i = c.work i) ∧ c'.input = c.input ∧ c'.output = c.output

The segCheck continue step (segCheck f reading non-□ → mmScr f): a pure control-state change — every tape is preserved exactly.

theorem Complexity.TM.UTMBody.appQ'_loop {f : VFlags} (E : ℕ → Γ) (hEns : ∀ (j : ℕ), 1 ≤ j → E j ≠ Γ.start) (n : ℕ) (S : ℕ → Γ) : (∀ (j : ℕ), 1 ≤ j → S j ≠ Γ.start) → ∀ (a e : ℕ), 1 ≤ a → 1 ≤ e → (∀ j < n, S (a + j) ≠ Γ.blank) → S (a + n) = Γ.blank → ∀ (c : Cfg 6 bodyTM.Q), c.state = BodyQ.appQ' f → (c.work stT).cells = S → (c.work stT).head = a → (c.work scT).cells = E → (c.work scT).head = e → c.input.read ≠ Γ.start → c.output.read ≠ Γ.start → (∀ (i : Fin 6), i ≠ stT → i ≠ scT → (c.work i).read ≠ Γ.start) → ∃ (c' : Cfg 6 bodyTM.Q), bodyTM.reachesIn (n + 1) c c' ∧ c'.state = BodyQ.appAct f 0 none ∧ c'.work stT = { head := a + n, cells := fun (j : ℕ) => if a ≤ j ∧ j < a + n then E (e + (j - a)) else S j } ∧ c'.work scT = { head := e + n, cells := E } ∧ c'.input = c.input ∧ c'.output = c.output ∧ ∀ (i : Fin 6), i ≠ stT → i ≠ scT → c'.work i = c.work i

The apply-phase state overwrite (appQ' f, trick 2): with the state head at a (old cells S, blank at distance n) and the scratch head at e (cells E, ▷-free), the machine copies n scratch symbols over the old state — reading the old state cell to know when to stop — then idles once on the □ into appAct f 0 none. Total n + 1 steps; the scratch tape and every other tape are exactly preserved.

theorem Complexity.TM.UTMBody.appAct_all {c : Cfg 6 bodyTM.Q} {f : VFlags} {sim0 sim1 sim2 : Tape} {E : ℕ → Γ} {e : ℕ} (h0 : VShift sim0 (c.work vIn)) (h1 : VShift sim1 (c.work vWk)) (h2 : VShift sim2 (c.work vOut)) (hwf0 : sim0.StartInvariant) (hwf1 : sim1.StartInvariant) (hwf2 : sim2.StartInvariant) (hf0 : f.1 = decide (sim0.head = 0)) (hf1 : f.2.1 = decide (sim1.head = 0)) (hf2 : f.2.2 = decide (sim2.head = 0)) (hst : c.state = BodyQ.appAct f 0 none) (hscC : (c.work scT).cells = E) (hscH : (c.work scT).head = e) (he : 1 ≤ e) (hEns : ∀ (j : ℕ), 1 ≤ j → E j ≠ Γ.start) (hstT : (c.work stT).read ≠ Γ.start) (hdsT : (c.work dsT).read ≠ Γ.start) (hin : c.input.read ≠ Γ.start) (hout : c.output.read ≠ Γ.start) : ∃ (c' : Cfg 6 bodyTM.Q), bodyTM.reachesIn 10 c c' ∧ c'.state = BodyQ.clScr ∧ VShift (sim0.move (if f.1 = true then Dir3.right else grpDir (cellBit (E (e + 4))) (cellBit (E (e + 5))))) (c'.work vIn) ∧ VShift (sim1.writeAndMove (grpΓw (cellBit (E e)) (cellBit (E (e + 1)))).toΓ (if f.2.1 = true then Dir3.right else grpDir (cellBit (E (e + 6))) (cellBit (E (e + 7))))) (c'.work vWk) ∧ VShift (sim2.writeAndMove (grpΓw (cellBit (E (e + 2))) (cellBit (E (e + 3)))).toΓ (if f.2.2 = true then Dir3.right else grpDir (cellBit (E (e + 8))) (cellBit (E (e + 9))))) (c'.work vOut) ∧ c'.work stT = c.work stT ∧ c'.work dsT = c.work dsT ∧ c'.work scT = { head := e + 10, cells := E } ∧ c'.input = c.input ∧ c'.output = c.output

The full apply-phase action decode (appAct f 0 none → … → clScr, trick 6): ten steps consume the ten scratch action cells E e .. E (e+9) in five 2-cell groups — write ww on vWork (g0), write wo on vOut (g1), move vInput (g2), move vWork (g3), move vOut (g4) — each write suppressed to □ and each move forced right where the corresponding at-origin flag is set, matching the interpreted machine's sanitized action exactly (note sim.write at the origin is itself a structural no-op, so the stated sim-side write is unconditional). The scratch tape ends at head e + 10 with cells unchanged; the state, desc, input, and output tapes are preserved exactly.