Body machine: the match-loop induction

The final piece of the body correctness: from cmpQ f at the start of the entry region, the machine walks the takeField segment split exactly as machFind does (BodyLookup.lean) — per segment either the full key-and-value scan succeeds (cmpQ → cmpS → copyQ' → copyAct → appRewScr), or the first failure point diverts to the uniform mismatch path (skipSeg → segCheck → mmScr → rewindSt) and the loop resumes at the next segment; an empty next segment sends the machine to the default path (dfScr) with the sanitized default moves applied (trick 4).

matchLoop packages both outcomes against machFind:

• machFind … = some seg — the machine reaches appRewScr f with the matched segment's value slice on the scratch tape;
• machFind … = none — the machine reaches dfScr having applied the default moves, scratch confined and blank beyond its head.

Corner (empty first segment). machFind/parseEntries treat a region that starts with □ as an exhausted table. The machine, started at cmpQ on such a region, instead steps past the empty segment (cmpQ→skipSeg→segCheck at the next cell) — it only recognizes the table terminator as a □ read by segCheck. On R = □ :: s :: … with s ≠ □ the two genuinely diverge: the machine goes on to scan the segments after the empty one while machFind returns none. matchLoop therefore carries the hypothesis that an empty head segment is a real terminator (R = □ :: s :: … → s = □). Every region the loop actually sees satisfies it: canonical descriptions (TMDesc.syms) have entry regions of the form entry □ ⋯ □ □ (head symbol is an entry bit) or □ (empty table), and the loop re-enters cmpQ only through segCheck, which has just read the next region's head symbol and found it non-□.

theorem Complexity.TM.UTMBody.matchLoop (f : VFlags) (v0 v1 v2 : Γ) (stSyms : List Γw) (hst_nb : ∀ s ∈ stSyms, s ≠ Γw.blank) (R : List Γw) (pos : ℕ) (c : Cfg 6 bodyTM.Q) : (∀ (s : Γw) (rest : List Γw), R = Γw.blank :: s :: rest → s = Γw.blank) → c.state = BodyQ.cmpQ f → (∀ (j : ℕ), (c.work dsT).cells (pos + j) = (R[j]?.getD Γw.blank).toΓ) → (c.work dsT).head = pos → 1 ≤ pos → (∀ (j : ℕ), 1 ≤ j → (c.work dsT).cells j ≠ Γ.start) → (c.work stT).HoldsExact stSyms → (c.work stT).head = 1 → (c.work scT).HoldsExact [] → (c.work scT).head = 1 → (c.work vIn).read = v0 → (c.work vWk).read = v1 → (c.work vOut).read = v2 → (c.work vIn).read ≠ Γ.start → (c.work vWk).read ≠ Γ.start → (c.work vOut).read ≠ Γ.start → c.input.read ≠ Γ.start → c.output.read ≠ Γ.start → (∀ (seg : List Γw), machFind stSyms.length stSyms (keyCells f v0 v1 v2) R = some seg → ∃ (c' : Cfg 6 bodyTM.Q), ∃ t ≤ (R.length + 2) * (4 * stSyms.length + 60), bodyTM.reachesIn t c c' ∧ c'.state = BodyQ.appRewScr f ∧ (c'.work scT).HoldsExact (List.take (stSyms.length + 10) (List.drop (stSyms.length + 6) seg)) ∧ (c'.work scT).head = stSyms.length + 10 + 1 ∧ c'.work stT = c.work stT ∧ (c'.work dsT).cells = (c.work dsT).cells ∧ 1 ≤ (c'.work dsT).head ∧ (c'.work dsT).head ≤ pos + R.length + 1 ∧ c'.work vIn = c.work vIn ∧ c'.work vWk = c.work vWk ∧ c'.work vOut = c.work vOut ∧ c'.input = c.input ∧ c'.output = c.output) ∧ (machFind stSyms.length stSyms (keyCells f v0 v1 v2) R = none → ∃ (c' : Cfg 6 bodyTM.Q), ∃ t ≤ (R.length + 2) * (4 * stSyms.length + 60), bodyTM.reachesIn t c c' ∧ c'.state = BodyQ.dfScr ∧ c'.work vIn = (c.work vIn).writeAndMove (readBackWrite v0).toΓ (if f.1 = true then Dir3.right else Dir3.stay) ∧ c'.work vWk = (c.work vWk).writeAndMove (readBackWrite v1).toΓ (if f.2.1 = true then Dir3.right else Dir3.stay) ∧ c'.work vOut = (c.work vOut).writeAndMove (readBackWrite v2).toΓ (if f.2.2 = true then Dir3.right else Dir3.stay) ∧ (c'.work stT).cells = (c.work stT).cells ∧ 1 ≤ (c'.work stT).head ∧ (c'.work stT).head ≤ stSyms.length + 1 ∧ (c'.work dsT).cells = (c.work dsT).cells ∧ 1 ≤ (c'.work dsT).head ∧ (c'.work dsT).head ≤ pos + R.length + 1 ∧ (c'.work scT).cells 0 = Γ.start ∧ (∀ (j : ℕ), 1 ≤ j → (c'.work scT).cells j ≠ Γ.start) ∧ 1 ≤ (c'.work scT).head ∧ (c'.work scT).head ≤ stSyms.length + 11 ∧ (∀ (j : ℕ), (c'.work scT).head ≤ j → 1 ≤ j → (c'.work scT).cells j = Γ.blank) ∧ c'.input = c.input ∧ c'.output = c.output)

The match-loop induction (design appendix 2, machine side): from cmpQ f at the start of the entry region suffix R (desc cells at pos + j hold R's symbols, blank-padded; an empty head segment of R, if any, is a real terminator — see the module docstring), with the state tape holding stSyms at head 1, a clean scratch tape, and the three virtual tapes stationary with live reads v0/v1/v2:

• if machFind accepts a segment seg, the machine reaches appRewScr f with seg's value slice (the w + 10 cells after its key) on the scratch tape, the state tape restored, desc cells unchanged, and the virtual tapes untouched;
• if machFind rejects (none), the machine reaches dfScr having applied the sanitized default moves (trick 4) to the three virtual tapes, with state and desc cells unchanged and the scratch confined (▷-free, blank at and beyond its head, head ≤ w + 11) — the shape defaultTail consumes;

in either case within (|R| + 2)·(4·|stSyms| + 60) steps.