Body machine: match-phase loop lemmas #
Closed-form loop lemmas for the body machine's match phase (design appendix,
phases 0 and 3): the halt-check lockstep compare (hc1), the key-scan
state-field compare (cmpQ), the six key-symbol cells (cmpS), the
q'-field countdown copy (copyQ', trick 1), and the ten action cells
(copyAct).
All lemmas follow the ghost-cell style of BodyInternal.lean: tape contents
are given as cell functions with ▷-freeness hypotheses, every idle tape is
exactly preserved (idle_tape_id frames), and scratch extension is stated
as an update-on-an-interval of the ghost cells (as in dfCopy_loop).
One step whose arm is idle q' changes only the control state, provided
every head reads a non-▷ symbol.
Generic lockstep compare loop for any state whose transition, on
agreeing non-□ state/desc reads, steps both the state and desc heads
right and stays in cur (the shape shared by hc1 and cmpQ f):
while the state tape (ghost cells S, head from a) and the desc tape
(ghost cells W, head from b) agree on n non-□ symbols, the
machine advances both heads n cells in n steps. All cells and every
other tape are exactly preserved.
Halt-check compare, match case: from hc1 with the state tape
(ghost S, head a) and desc tape (ghost W, head b) agreeing on
n non-□ symbols and then both hitting □ simultaneously, reach
haltRewS in n + 1 steps with heads at a + n and b + n. All
cells and every other tape are exactly preserved.
Halt-check compare, mismatch case: same lockstep compare as
hc1_match_loop, but at offset n the two tapes disagree for the first
time (not both □, and not both-non-□-and-equal): reach preRewS in
n + 1 steps with heads at a + n and b + n. All cells and every
other tape are exactly preserved.
Key-field compare, match case: from cmpQ f with the state tape
(ghost S, head a) and desc tape (ghost W, head b) agreeing on
n non-□ symbols, and the state tape hitting □ at offset n (the
state's key part is consumed — the exit fires regardless of the desc
symbol), reach cmpS f 0 in n + 1 steps with heads at a + n and
b + n (the exit step moves neither head). All cells and every other
tape are exactly preserved.
Key-field compare, mismatch case: same lockstep compare as
cmpQ_match_loop, but at offset n the state symbol is non-□ and
fails to match the desc symbol (desc □ or different): reach
skipSeg f in n + 1 steps with heads at a + n and b + n (the
exit step moves neither head). All cells and every other tape are
exactly preserved.
Key-symbol compare, match case: from cmpS f idx with the desc
tape (ghost W, head b) holding the expected keyCell symbols
(all non-□) at offsets 0..k (idx.val + k = 5), reach copyQ' f
in k + 1 steps with the desc head at b + k + 1. The three virtual
tapes are stationary, so their live reads v0/v1/v2 stay valid
throughout. On the final step the state head (ghost V, head a)
takes trick 1's pre-step one cell left. All cells and every other tape
are exactly preserved.
Key-symbol compare, mismatch case: from cmpS f idx with the desc
tape (ghost W, head b) matching the expected keyCell symbols at
offsets < n but failing at offset n (idx.val + n ≤ 5; the cell
differs from the expected symbol or is □), reach skipSeg f in
n + 1 steps with the desc head at b + n. The state head does not
move. All cells and every other tape are exactly preserved.
q'-field copy, clean case (trick 1): from copyQ' f with the state
tape (ghost S, ▷ at cell 0 only, head counting down from s), the
desc tape (ghost W, head b) holding s non-□ cells, and the
scratch tape (ghost E, frontier e), copy the s desc cells to
scratch cells e..e+s-1 while the state head walks left; when it hits
▷ the forced bounce lands it at cell 1 and the machine enters
copyAct f 0 — s + 1 steps in total. State and desc cells and every
other tape are exactly preserved.
q'-field copy, early-□ case: from copyQ' f counting down from
state head s, the desc tape hits □ after only n < s copied cells:
the machine exits to skipSeg f in n + 1 steps (the □-exit step is
an idle transition) with the state head at s - n, the desc head at
b + n (on the □), and scratch extended by the n copied cells.
State and desc cells and every other tape are exactly preserved.
Action-cell copy, clean case: from copyAct f j with the desc tape
(ghost W, head b) holding k + 1 non-□ cells
(j.val + k = 9, so k + 1 = 10 - j.val) and the scratch tape (ghost
E, frontier e), copy the remaining action cells to scratch cells
e..e+k and enter appRewScr f in k + 1 steps, with the desc head
at b + k + 1 and the scratch frontier at e + k + 1. Desc cells and
every other tape are exactly preserved.
Action-cell copy, early-□ case: from copyAct f j, the desc tape
hits □ at offset n (j.val + n ≤ 9) after n copied cells: the
machine exits to skipSeg f in n + 1 steps (the □-exit step is an
idle transition) with the desc head at b + n (on the □) and scratch
extended by the n copied cells. Desc cells and every other tape are
exactly preserved.