Halt-test verdict correspondence

The halt-test machine compares the state tape against the description tape's second field — exactly the qhF field that parseSyms decodes as the halt state. This file proves the comparison agrees with the abstract halt check of the interpreted machine (decodeDesc α).toTM:

• a running state tape (w-bit encoding of q < 2^w) matches the field iff q is the decoded halt state (well-formed fields decode by Nat.toBits/Nat.fromBits; malformed-width fields never match, and the decoded sentinel 2^w is unreachable);
• after a default transition the state tape holds the field verbatim, and the interpreted machine sits exactly at its (clamped) halt state.

theorem Complexity.TM.UTMBody.bitsToSyms_filterMap_of_ne_blank {l : List Γw} : (∀ s ∈ l, s ≠ Γw.blank) → bitsToSyms (List.filterMap symBit? l) = l

A blank-free Γw list is the symbol image of its own bits.

def Complexity.TM.UTMBody.qhaltField (dSyms : List Γw) : List Γw

The description tape's second field (the qhalt field), as scanned by the halt-test machine and decoded by parseSyms.

Equations

• Complexity.TM.UTMBody.qhaltField dSyms = (Complexity.takeField (Complexity.takeField dSyms).2).1

theorem Complexity.TM.UTMBody.decodeDesc_qhalt (α : List Bool) : (decodeDesc α).qhalt = if (qhaltField (groupPairs α)).length = (decodeDesc α).w then fieldNat (qhaltField (groupPairs α)) else 2 ^ (decodeDesc α).w

The qhalt field of a decoded description determines its halt state: fieldNat if the width matches, the sentinel 2^w otherwise.

theorem Complexity.TM.UTMBody.decodeDesc_w (α : List Bool) : (decodeDesc α).w = (takeField (groupPairs α)).1.length

The decoded width is the first field's length.

theorem Complexity.TM.UTMBody.verdict_running (α : List Bool) {q : ℕ} (hq : q < 2 ^ (decodeDesc α).w) : bitsToSyms ((decodeDesc α).w.toBits q) = qhaltField (groupPairs α) ↔ q = min (decodeDesc α).qhalt (2 ^ (decodeDesc α).w)

Running-state verdict: for q < 2^w (with w the decoded width), the state tape's w-bit encoding of q equals the qhalt field iff the interpreted machine's state q is its halt state.