Support lemmas for the time-hierarchy theorem

Four self-contained ingredients used by the diagonalization argument:

• groupPairs_length_le — decoding a bit string into 2-bit groups at most halves its length.
• TM.UTMBody.utmStepTime_le_sq — the per-iteration cost of the UTM loop is quadratic in the description length, with an explicit constant.
• Complexity.LittleO.nat_mul_le — a little-o hypothesis yields, for every scale factor C, an eventual pointwise bound C * f n ≤ g n over ℕ.
• TM.halt_or_run_dichotomy — a deterministic machine either halts within a step budget V or is still running after exactly V steps.

theorem Complexity.groupPairs_length_le (α : List Bool) : 2 * (groupPairs α).length ≤ α.length

groupPairs consumes two bits per emitted symbol (a trailing odd bit is dropped), so its output is at most half as long as its input.

theorem Complexity.TM.UTMBody.utmStepTime_le_sq (α : List Bool) : utmStepTime α ≤ 240 * (α.length + 1) ^ 2

The per-iteration cost of the UTM's simulate/halt-test loop is quadratic in the description length, with explicit constant 240.

theorem Complexity.LittleO.nat_mul_le {f g : ℕ → ℕ} (h : LittleO f g) (C : ℕ) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → C * f n ≤ g n

A little-o hypothesis beats every constant multiple eventually: from f = o(g) extract, for any scale C : ℕ, a threshold N past which C * f n ≤ g n pointwise over ℕ.

theorem Complexity.TM.halt_or_run_dichotomy {k : ℕ} (tm : TM k) (c₀ : Cfg k tm.Q) (V : ℕ) : (∃ (T : ℕ) (c : Cfg k tm.Q), T ≤ V ∧ tm.reachesIn T c₀ c ∧ tm.halted c) ∨ ∃ (c : Cfg k tm.Q), tm.reachesIn V c₀ c ∧ ¬tm.halted c

Run dichotomy: from any configuration, a deterministic machine either halts within V steps or reaches a non-halted configuration in exactly V steps.