TerminatedRegion for encoded descriptions

The body machine's per-iteration theorem carries the side condition TerminatedRegion α, ruling out the one machine/decoder divergence: an entry region starting with an empty segment followed by junk. This file discharges that condition for the inputs the universal machine actually runs on: canonical encodings encodeDesc d of well-formed descriptions with a nonempty table, with arbitrary trailing junk.

The proof redoes the field decomposition of decodeDesc_encodeDesc_append: after two takeFields the region is the encoded entry table, which starts with the (nonempty, blank-free) symbols of the first entry — never with a separator □. Extracted tables are nonempty (descOfTM_entries_ne_nil), since every machine has at least its start state.

theorem Complexity.TM.UTMBody.terminatedRegion_encodeDesc {d : TMDesc} (_hd : d.WF) (hne : d.entries ≠ []) (junk : List Bool) : TerminatedRegion (encodeDesc d ++ junk)

Encoded descriptions have terminated entry regions: the entry region of encodeDesc d ++ junk starts with the first table entry's symbols — nonempty and blank-free — so the TerminatedRegion premise (a region starting with □) never fires.

theorem Complexity.TM.UTMBody.terminatedRegion_encodeDesc_plain {d : TMDesc} (hd : d.WF) (hne : d.entries ≠ []) : TerminatedRegion (encodeDesc d)

terminatedRegion_encodeDesc for the bare encoding (no junk).

theorem Complexity.TM.UTMBody.descOfTM_entries_ne_nil (M : TM 1) : M.descOfTM.entries ≠ []

Extracted tables are nonempty: every machine has at least its start state, and the dense table lists a row for each state/symbols key.