Nondeterministic trace decomposition

This module exposes canonical finite-trace splitting rules without leaking dependent Fin casts into fixed-schedule simulation proofs.

Main results

• NTM.trace_snoc -- split the final step off a nonempty trace.
• NTM.trace_invariant -- prove an indexed invariant one trace step at a time.

theorem Complexity.NTM.trace_snoc {n : ℕ} (tm : NTM n) (T : ℕ) (choices : Fin (T + 1) → Bool) (c : Cfg n tm.Q) : tm.trace (T + 1) choices c = tm.trace 1 (fun (x : Fin 1) => choices (Fin.last T)) (tm.trace T (fun (i : Fin T) => choices i.castSucc) c)

Split the final step off a nonempty trace. The prefix uses Fin.castSucc, and the final choice is selected by Fin.last.

theorem Complexity.NTM.trace_invariant {n : ℕ} (tm : NTM n) (T : ℕ) (choices : Fin T → Bool) (c : Cfg n tm.Q) (invariant : ℕ → Cfg n tm.Q → Prop) (initial : invariant 0 c) (step : ∀ (time : ℕ) (htime : time < T) (current : Cfg n tm.Q), invariant time current → invariant (time + 1) (tm.trace 1 (fun (x : Fin 1) => choices ⟨time, htime⟩) current)) : invariant T (tm.trace T choices c)

Prove an indexed invariant along a finite trace. The step rule receives the original choice at the current time, while this theorem owns all prefix reindexing and final-step stitching.