Body correctness: phase assembly

The per-iteration proof of the body machine, assembled from the phase lemmas. This file starts with the standing invariant SimInv (the tape shape between loop iterations, relative to the interpreted machine's configuration) and the halt-check phase: from the body's start state, a halted interpreted machine makes the body a bounded-time no-op, and a running one brings it to the peek phase with all tapes restored.

theorem Complexity.TM.UTMBody.Γw.toΓ_inj {x y : Γw} (h : x.toΓ = y.toΓ) : x = y

Γw.toΓ is injective.

theorem Complexity.TM.UTMBody.Γw.toΓ_eq_blank {x : Γw} : x.toΓ = Γ.blank ↔ x = Γw.blank

Γw.toΓ hits Γ.blank only at □.

structure Complexity.TM.UTMBody.SimInv (α : List Bool) (mc : Cfg 1 (decodeDesc α).toTM.Q) (inp : Tape) (work : Fin 6 → Tape) (out : Tape) : Prop

The body's standing tape shape between loop iterations, relative to a configuration mc of the interpreted machine (decodeDesc α).toTM. The state-tape clause is a disjunction: the running shape (the w-bit encoding of the current state) or the post-default shape (the qhalt field verbatim — the machine is then halted).

• vin : VShift mc.input (work vIn)
• vwk : VShift (mc.work 0) (work vWk)
• vout : VShift mc.output (work vOut)
• wf_in : mc.input.StartInvariant
• wf_wk : (mc.work 0).StartInvariant
• wf_out : mc.output.StartInvariant
• state : ↑mc.state < 2 ^ (decodeDesc α).w ∧ (work stT).HoldsExact (bitsToSyms ((decodeDesc α).w.toBits ↑mc.state)) ∨ mc.state = (decodeDesc α).toTM.qhalt ∧ (work stT).HoldsExact (qhaltField (groupPairs α))
• state_head : (work stT).head = 1
• desc : (work dsT).HoldsExact (groupPairs α)
• desc_head : (work dsT).head = 1
• scratch : (work scT).HoldsExact []
• scratch_head : (work scT).head = 1
• inp_read : inp.read ≠ Γ.start
• out_read : out.read ≠ Γ.start

theorem Complexity.TM.UTMBody.SimInv.state_syms_ne_blank {α : List Bool} {mc : Cfg 1 (decodeDesc α).toTM.Q} {inp : Tape} {work : Fin 6 → Tape} {out : Tape} (h : SimInv α mc inp work out) : ∃ (S : List Γw), (work stT).HoldsExact S ∧ (∀ s ∈ S, s ≠ Γw.blank) ∧ (↑mc.state < 2 ^ (decodeDesc α).w ∧ S = bitsToSyms ((decodeDesc α).w.toBits ↑mc.state) ∨ mc.state = (decodeDesc α).toTM.qhalt ∧ S = qhaltField (groupPairs α))

The state tape's contents (either disjunct) are blank-free.

theorem Complexity.TM.UTMBody.SimInv.others_read {α : List Bool} {mc : Cfg 1 (decodeDesc α).toTM.Q} {inp : Tape} {work : Fin 6 → Tape} {out : Tape} (h : SimInv α mc inp work out) (i : Fin 6) : i ≠ stT → i ≠ dsT → (work i).read ≠ Γ.start

Standard parked-reads package for the non-state, non-desc work tapes.

theorem Complexity.TM.UTMBody.SimInv.read_ne_start_of_holdsExact {t : Tape} {l : List Γw} (h : t.HoldsExact l) (hh : 1 ≤ t.head) : t.read ≠ Γ.start

Any HoldsExact tape with head off ▷ reads a non-▷ symbol.

theorem Complexity.TM.UTMBody.hcPhase_halted {α : List Bool} {mc : Cfg 1 (decodeDesc α).toTM.Q} (c : Cfg 6 bodyTM.Q) (hst : c.state = BodyQ.hc0) (hinv : SimInv α mc c.input c.work c.output) (hhalt : mc.state = (decodeDesc α).toTM.qhalt) : ∃ (c' : Cfg 6 bodyTM.Q), ∃ t ≤ 5 * (groupPairs α).length + 7, bodyTM.reachesIn t c c' ∧ c'.state = BodyQ.bodyDone ∧ c'.input = c.input ∧ (∀ (i : Fin 6), c'.work i = c.work i) ∧ c'.output = c.output

Halt-check phase, halted case: when the interpreted machine sits at its halt state, the body runs from its start state to bodyDone as a pure no-op — every tape is exactly restored — within 5·|groupPairs α| + 7 steps.

theorem Complexity.TM.UTMBody.hcPhase_running {α : List Bool} {mc : Cfg 1 (decodeDesc α).toTM.Q} (c : Cfg 6 bodyTM.Q) (hst : c.state = BodyQ.hc0) (hinv : SimInv α mc c.input c.work c.output) (hrun : mc.state ≠ (decodeDesc α).toTM.qhalt) : ∃ (c' : Cfg 6 bodyTM.Q), ∃ t ≤ 5 * (groupPairs α).length + 7, bodyTM.reachesIn t c c' ∧ c'.state = BodyQ.peek1 ∧ c'.input = c.input ∧ (∀ (i : Fin 6), c'.work i = c.work i) ∧ c'.output = c.output

Halt-check phase, running case: when the interpreted machine is not at its halt state, the body's halt check falls through to the peek phase with every tape exactly restored, within 5·|groupPairs α| + 7 steps.

theorem Complexity.TM.UTMBody.peekSeekPhase {α : List Bool} {mc : Cfg 1 (decodeDesc α).toTM.Q} (c : Cfg 6 bodyTM.Q) (hst : c.state = BodyQ.peek1) (hinv : SimInv α mc c.input c.work c.output) : ∃ (c' : Cfg 6 bodyTM.Q), ∃ t ≤ 2 * (groupPairs α).length + 4, bodyTM.reachesIn t c c' ∧ c'.state = BodyQ.cmpQ (decide (mc.input.head = 0), decide ((mc.work 0).head = 0), decide (mc.output.head = 0)) ∧ (∀ (i : Fin 6), i ≠ dsT → c'.work i = c.work i) ∧ c'.work dsT = { head := (takeField (groupPairs α)).1.length + (qhaltField (groupPairs α)).length + 3, cells := (c.work dsT).cells } ∧ c'.input = c.input ∧ c'.output = c.output

Peek and seek phases: from peek1, capture the (honest) at-origin flags and walk the desc head to the start of the entry region (|F1| + |F2| + 3), all other tapes exactly restored, within 2·|groupPairs α| + 4 steps.

theorem Complexity.TM.UTMBody.cleanupPhase (c : Cfg 6 bodyTM.Q) (E S W : ℕ → Γ) (p sp dp : ℕ) (hsp : 1 ≤ sp) (hdp : 1 ≤ dp) (hst : c.state = BodyQ.clScr) (hE0 : E 0 = Γ.start) (hEns : ∀ (j : ℕ), 1 ≤ j → E j ≠ Γ.start) (hEbeyond : ∀ (j : ℕ), p < j → E j = Γ.blank) (hscC : (c.work scT).cells = E) (hscH : (c.work scT).head = p) (hS0 : S 0 = Γ.start) (hSns : ∀ (j : ℕ), 1 ≤ j → S j ≠ Γ.start) (hstC : (c.work stT).cells = S) (hstH : (c.work stT).head = sp) (hW0 : W 0 = Γ.start) (hWns : ∀ (j : ℕ), 1 ≤ j → W j ≠ Γ.start) (hdsC : (c.work dsT).cells = W) (hdsH : (c.work dsT).head = dp) (hin : c.input.read ≠ Γ.start) (hout : c.output.read ≠ Γ.start) (hoth : ∀ (i : Fin 6), i ≠ stT → i ≠ dsT → i ≠ scT → (c.work i).read ≠ Γ.start) : ∃ (c' : Cfg 6 bodyTM.Q), bodyTM.reachesIn (p + 1 + (sp + 1) + (dp + 1)) c c' ∧ c'.state = BodyQ.bodyDone ∧ (c'.work scT).HoldsExact [] ∧ (c'.work scT).head = 1 ∧ c'.work stT = { head := 1, cells := S } ∧ c'.work dsT = { head := 1, cells := W } ∧ (∀ (i : Fin 6), i ≠ stT → i ≠ dsT → i ≠ scT → c'.work i = c.work i) ∧ c'.input = c.input ∧ c'.output = c.output

Cleanup phase (after a successful apply): blank-rewind the scratch tape, then rewind the state and desc heads; ends at bodyDone with the scratch cleared and every other tape's cells intact.

theorem Complexity.TM.UTMBody.defaultTail {α : List Bool} (c : Cfg 6 bodyTM.Q) (E : ℕ → Γ) (SL : List Γw) (p sp dp : ℕ) (hsp : 1 ≤ sp) (hdp : 1 ≤ dp) (hst : c.state = BodyQ.dfScr) (hE0 : E 0 = Γ.start) (hEns : ∀ (j : ℕ), 1 ≤ j → E j ≠ Γ.start) (hEbeyond : ∀ (j : ℕ), p < j → E j = Γ.blank) (hscC : (c.work scT).cells = E) (hscH : (c.work scT).head = p) (hSL_hold : (c.work stT).HoldsExact SL) (hSL_nb : ∀ s ∈ SL, s ≠ Γw.blank) (hstH : (c.work stT).head = sp) (hdesc : (c.work dsT).HoldsExact (groupPairs α)) (hdsH : (c.work dsT).head = dp) (hin : c.input.read ≠ Γ.start) (hout : c.output.read ≠ Γ.start) (hoth : ∀ (i : Fin 6), i ≠ stT → i ≠ dsT → i ≠ scT → (c.work i).read ≠ Γ.start) : ∃ (c' : Cfg 6 bodyTM.Q), ∃ t ≤ p + 2 * sp + 2 * SL.length + 2 * dp + 2 * (takeField (groupPairs α)).1.length + 3 * (qhaltField (groupPairs α)).length + 12, bodyTM.reachesIn t c c' ∧ c'.state = BodyQ.bodyDone ∧ (c'.work stT).HoldsExact (qhaltField (groupPairs α)) ∧ (c'.work stT).head = 1 ∧ c'.work dsT = { head := 1, cells := (c.work dsT).cells } ∧ (c'.work scT).HoldsExact [] ∧ (c'.work scT).head = 1 ∧ (∀ (i : Fin 6), i ≠ stT → i ≠ dsT → i ≠ scT → c'.work i = c.work i) ∧ c'.input = c.input ∧ c'.output = c.output

Default-phase tail (from dfScr, after the sanitized virtual moves were applied on the segCheck step): clear the scratch, blank the state tape, copy the qhalt field onto it, rewind everything; ends at bodyDone with the state tape holding the qhalt field — the shape of the invariant's post-default disjunct.

theorem Complexity.TM.UTMBody.applyPhase (c : Cfg 6 bodyTM.Q) {f : VFlags} {sim0 sim1 sim2 : Tape} (EL SL : List Γw) (sc_p dp : ℕ) (_hscp : 1 ≤ sc_p) (hdp : 1 ≤ dp) (hlen : EL.length = SL.length + 10) (hSL_nb : ∀ s ∈ SL, s ≠ Γw.blank) (hst : c.state = BodyQ.appRewScr f) (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)) (hSL_hold : (c.work stT).HoldsExact SL) (hstH : (c.work stT).head = 1) (hEL_hold : (c.work scT).HoldsExact EL) (hscH : (c.work scT).head = sc_p) (hdesc_wf : (c.work dsT).StartInvariant) (hdsH : (c.work dsT).head = dp) (hin : c.input.read ≠ Γ.start) (hout : c.output.read ≠ Γ.start) : ∃ (c' : Cfg 6 bodyTM.Q), ∃ t ≤ sc_p + 3 * SL.length + dp + 28, bodyTM.reachesIn t c c' ∧ c'.state = BodyQ.bodyDone ∧ (c'.work stT).HoldsExact (List.take SL.length EL) ∧ (c'.work stT).head = 1 ∧ c'.work dsT = { head := 1, cells := (c.work dsT).cells } ∧ (c'.work scT).HoldsExact [] ∧ (c'.work scT).head = 1 ∧ VShift (sim0.move (if f.1 = true then Dir3.right else grpDir (cellBit ((c.work scT).cells (1 + SL.length + 4))) (cellBit ((c.work scT).cells (1 + SL.length + 5))))) (c'.work vIn) ∧ VShift (sim1.writeAndMove (grpΓw (cellBit ((c.work scT).cells (1 + SL.length))) (cellBit ((c.work scT).cells (1 + SL.length + 1)))).toΓ (if f.2.1 = true then Dir3.right else grpDir (cellBit ((c.work scT).cells (1 + SL.length + 6))) (cellBit ((c.work scT).cells (1 + SL.length + 7))))) (c'.work vWk) ∧ VShift (sim2.writeAndMove (grpΓw (cellBit ((c.work scT).cells (1 + SL.length + 2))) (cellBit ((c.work scT).cells (1 + SL.length + 3)))).toΓ (if f.2.2 = true then Dir3.right else grpDir (cellBit ((c.work scT).cells (1 + SL.length + 8))) (cellBit ((c.work scT).cells (1 + SL.length + 9))))) (c'.work vOut) ∧ c'.input = c.input ∧ c'.output = c.output

Apply phase (from appRewScr f, scratch holding the copied value EL = new-state field (|SL| cells, the old state's width) followed by the ten action cells): rewind scratch, overwrite the state tape, decode and act on the virtual tapes, clean up. Ends at bodyDone with the state tape holding the value's first |SL| cells and the virtual tapes transformed by the sanitized action.