Head bounds for prefixes of bounded traces

This internal module adapts the general head-growth estimates for NTM traces to the strict bound required by the one-step circuit formulas. At every proper prefix i < T of a trace from initCfg, all named heads are strictly below T. It also identifies one choiceStep from prefix i with prefix i + 1 of the same full choice sequence.

theorem Complexity.CircuitUnrolling.headsLt_trace_prefix_internal {k : ℕ} (tm : NTM k) (T i : ℕ) (choices : Fin T → Bool) (x : List Bool) (hi : i < T) : HeadsLt T (tm.trace i (fun (j : Fin i) => choices ⟨↑j, ⋯⟩) (tm.initCfg x))

Every named head in a proper prefix of an initialized length-T trace is strictly below the circuit horizon.

theorem Complexity.CircuitUnrolling.choiceStep_trace_prefix_internal {k : ℕ} (tm : NTM k) (T i : ℕ) (choices : Fin T → Bool) (x : List Bool) (hi : i < T) : choiceStep tm (choices ⟨i, hi⟩) (tm.trace i (fun (j : Fin i) => choices ⟨↑j, ⋯⟩) (tm.initCfg x)) = tm.trace (i + 1) (fun (j : Fin (i + 1)) => choices ⟨↑j, ⋯⟩) (tm.initCfg x)

Taking one choiceStep from prefix i gives prefix i + 1 of the same full bounded choice sequence.