Glue facts: phase outputs vs the interpreted step

Small bridges used when matching the body's phase outputs against TMDesc.toTM.step:

• a well-formed tape reads ▷ exactly at the origin, so the peek flags and the interpreter's sanitization conditions coincide;
• simRead of the live shadow read recovers the simulated read exactly;
• parsed entries' targets are in range, so the interpreter's min-clamp is the identity on them.

theorem Complexity.TM.UTMBody.read_start_iff {t : Tape} (h : t.StartInvariant) : t.read = Γ.start ↔ t.head = 0

A well-formed tape reads ▷ exactly at cell 0.

theorem Complexity.TM.UTMBody.simRead_flag_eq {sim utm : Tape} (h : VShift sim utm) (hwf : sim.StartInvariant) : simRead (decide (sim.head = 0)) utm.read = sim.read

The simulated read, reconstructed from the honest flag and the live shadow read, is exactly the simulated tape's read.

theorem Complexity.TM.UTMBody.parseEntry_q'_lt {w : ℕ} {seg : List Γw} {e : DescEntry} (hp : parseEntry w seg = some e) : e.act.q' < 2 ^ w

Every entry produced by parseEntry has an in-range target, so the interpreter's min-clamp is the identity on it.

theorem Complexity.TM.UTMBody.writeAndMove_readback_eq_move {t : Tape} (hwf : t.StartInvariant) (d : Dir3) : t.writeAndMove (TMDesc.readback t.read).toΓ d = t.move d

Writing back the read symbol (the interpreter's default action) and moving is just the move, on a well-formed tape.

theorem Complexity.TM.UTMBody.valueSlice_take (seg : List Γw) (w : ℕ) : List.take w (List.take (w + 10) (List.drop (w + 6) seg)) = List.take w (List.drop (w + 6) seg)

The value slice copied to scratch, restricted to its first w cells, is the segment's new-state field.

theorem Complexity.TM.UTMBody.scratch_cellBit_eq_segBit {t : Tape} {seg : List Γw} {w k : ℕ} (hk : k < 10) (hlen : 2 * w + 16 ≤ seg.length) (h : t.HoldsExact (List.take (w + 10) (List.drop (w + 6) seg))) : cellBit (t.cells (1 + w + k)) = segBit seg (2 * w + 6 + k)

Scratch cells holding the value slice decode, at the action offsets, to the segment's action bits.