Output-length bounds — proof internals

This module proves that a deterministic machine cannot produce more output bits than the number of transitions it has taken. The key support lemma says that an output cell beyond the initial head position plus the elapsed time is unchanged.

Public statements are in Complexitylib.Models.TuringMachine.OutputBounds.

theorem Complexity.TM.reachesIn_output_cells_far_internal {n : ℕ} {tm : TM n} {t : ℕ} {c c' : Cfg n tm.Q} : tm.reachesIn t c c' → ∀ (j : ℕ), c.output.head + t < j → c'.output.cells j = c.output.cells j

Cells beyond the output head's maximum reach are never changed.

theorem Complexity.TM.output_length_le_of_reachesIn_internal {n : ℕ} {tm : TM n} {x y : List Bool} {c' : Cfg n tm.Q} {t : ℕ} (hreach : tm.reachesIn t (tm.initCfg x) c') (hout : c'.output.HasOutput y) : y.length ≤ t

A run from an initial configuration needs at least one transition for each bit present in its final output string.

theorem Complexity.TM.computesInTime_output_length_le_internal {n : ℕ} {tm : TM n} {f : List Bool → List Bool} {T : ℕ → ℕ} (h : tm.ComputesInTime f T) (x : List Bool) : (f x).length ≤ T x.length

A time-bounded function computation has output length bounded by its advertised running time.