Universal machine: simulation bridges

Bridges between the phase machines' Hoare specifications and the body's standing invariant SimInv:

• the initialization machine's postcondition realizes SimInv at the interpreted machine's initial configuration (for every binary α — the decoded start state's fixed-width encoding is exactly the first description field, by the toBits/fromBits roundtrip at the field's own width);
• verdict and output-growth facts used by the loop and extraction proofs.

The completed loop simulation and headline universal-machine theorems are in UTM/SimLoop.lean and UTM/Universal.lean.

theorem Complexity.TM.UTMBody.qstartField_eq_encoding (α : List Bool) : (takeField (groupPairs α)).1 = bitsToSyms ((decodeDesc α).w.toBits ↑(decodeDesc α).toTM.qstart)

The first description field is the fixed-width encoding of the decoded start state — for arbitrary α.

theorem Complexity.TM.UTMBody.vshift_initTape_nil {t : Tape} (h : t.HoldsExact []) (hh : t.head = 1) : VShift (Tape.init []) t

A cleared, started tape shadows the empty simulated tape.

theorem Complexity.TM.UTMBody.vshift_initTape_x {t : Tape} (x : List Bool) (hc : t.cells = fun (k : ℕ) => if k = 0 then Γ.start else if k = 1 then Γ.blank else (List.map Γ.ofBool x)[k - 2]?.getD Γ.blank) (hh : t.head = 1) : VShift (Tape.init (List.map Γ.ofBool x)) t

The shifted copy of x (cells ▷ □ x ⋯, head 1) shadows the interpreted machine's initial input tape.

theorem Complexity.TM.UTMBody.initPost_simInv (α x : List Bool) (inp : Tape) (work : Fin 6 → Tape) (out : Tape) (hpost : inp.cells = (Tape.init (List.map Γ.ofBool (pair α x))).cells ∧ ((work 0).cells = fun (k : ℕ) => if k = 0 then Γ.start else if k = 1 then Γ.blank else (List.map Γ.ofBool x)[k - 2]?.getD Γ.blank) ∧ (work 0).head = 1 ∧ (work 1).HoldsExact [] ∧ (work 1).head = 1 ∧ (work 2).HoldsExact [] ∧ (work 2).head = 1 ∧ (work 3).HoldsExact (takeField (groupPairs α)).1 ∧ (work 3).head = 1 ∧ (work 4).HoldsExact (groupPairs α) ∧ (work 4).head = 1 ∧ (work 5).HoldsExact [] ∧ (work 5).head = 1 ∧ out.cells = (Tape.init []).cells ∧ out.head = 1) (hinp_head : 1 ≤ inp.head) : SimInv α ((decodeDesc α).toTM.initCfg x) inp work out

Initialization realizes the invariant: the tape shape guaranteed by initTM's postcondition is SimInv at the interpreted machine's initial configuration.

theorem Complexity.TM.UTMBody.simInv_verdict (α : List Bool) (mc : Cfg 1 (decodeDesc α).toTM.Q) {inp : Tape} {work : Fin 6 → Tape} {out : Tape} (hinv : SimInv α mc inp work out) : ∃ (stSyms : List Γw), (work stT).HoldsExact stSyms ∧ (∀ s ∈ stSyms, s ≠ Γw.blank) ∧ (stSyms = qhaltField (groupPairs α) ↔ mc.state = (decodeDesc α).toTM.qhalt)

The halt test's comparison decides exactly the interpreted machine's halt condition, under the invariant.

theorem Complexity.TM.UTMBody.writeAndMove_head_le (t : Tape) (s : Γ) (d : Dir3) : (t.writeAndMove s d).head ≤ t.head + 1

One tape action moves the head at most one cell.

theorem Complexity.TM.UTMBody.writeAndMove_cells_ne (t : Tape) (s : Γ) (d : Dir3) {j : ℕ} (hj : j ≠ t.head) : (t.writeAndMove s d).cells j = t.cells j

One tape action leaves cells other than the head untouched.

theorem Complexity.TM.UTMBody.reachesIn_output_head_le {n : ℕ} {tm : TM n} {t : ℕ} {c c' : Cfg n tm.Q} : tm.reachesIn t c c' → c'.output.head ≤ c.output.head + t

After t steps the output head has advanced at most t cells.

theorem Complexity.TM.UTMBody.reachesIn_output_cells_far {n : ℕ} {tm : TM n} {t : ℕ} {c c' : Cfg n tm.Q} : tm.reachesIn t c c' → ∀ (j : ℕ), c.output.head + t < j → c'.output.cells j = c.output.cells j

Cells beyond the output head's reach are never written.

theorem Complexity.TM.UTMBody.reachesIn_output_first_blank {n : ℕ} {tm : TM n} {t : ℕ} {x : List Bool} {c' : Cfg n tm.Q} (h : tm.reachesIn t (tm.initCfg x) c') : ∃ m ≤ t, c'.output.cells (m + 2) = Γ.blank ∧ ∀ j < m, c'.output.cells (j + 2) ≠ Γ.blank

From the initial configuration, the output tape has a first blank within t + 1 cells after t steps.