Body correctness: the per-iteration theorem

The capstone gluing of the body correctness: from the body's start state, under the standing invariant SimInv, one pass of the body machine reaches bodyDone in bodyIterTime α steps and

• is an exact no-op when the interpreted machine (decodeDesc α).toTM is halted at mc, and
• re-establishes SimInv at (decodeDesc α).toTM.step mc otherwise.

The proof chains the phase lemmas of BodyAssembly/BodyLoop (hcPhase_halted/hcPhase_running → peekSeekPhase → matchLoop → applyPhase/defaultTail) and identifies the machine's decoded action with the abstract table lookup via the BodyLookup correspondence (firstMatch_lookup/noMatch_lookup, value_slices).

The side condition TerminatedRegion rules out the one machine/decoder divergence: an entry region starting with an empty segment followed by junk (see matchLoop).

def Complexity.TM.UTMBody.TerminatedRegion (α : List Bool) : Prop

The side condition ruling out the machine/decoder divergence on an empty leading table segment followed by junk (see matchLoop).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.UTMBody.bodyIterTime (α : List Bool) : ℕ

Time bound for one body iteration: quadratic in the description length, with generous constants (the match loop dominates).

Equations

• Complexity.TM.UTMBody.bodyIterTime α = ((Complexity.groupPairs α).length + 2) * (4 * (Complexity.groupPairs α).length + 60) + 30 * (Complexity.groupPairs α).length + 100

theorem Complexity.TM.UTMBody.bodyIteration (α : List Bool) (mc : Cfg 1 (decodeDesc α).toTM.Q) (hterm : TerminatedRegion α) (c : Cfg 6 bodyTM.Q) (hst : c.state = BodyQ.hc0) (hinv : SimInv α mc c.input c.work c.output) : ∃ (c' : Cfg 6 bodyTM.Q), ∃ t ≤ bodyIterTime α, bodyTM.reachesIn t c c' ∧ c'.state = BodyQ.bodyDone ∧ c'.input = c.input ∧ c'.output = c.output ∧ match (decodeDesc α).toTM.step mc with | none => ∀ (i : Fin 6), c'.work i = c.work i | some mc' => SimInv α mc' c'.input c'.work c'.output

Per-iteration correctness of the body machine: from hc0 under SimInv, the body reaches bodyDone within bodyIterTime α steps, leaving the real input/output tapes untouched; if the interpreted machine is halted the pass is an exact no-op on every work tape, and otherwise SimInv is re-established at the stepped configuration.