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.NTM.trace_map_prefix-- transport a running prefix with its exact choice sequence.
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.
theorem
Complexity.NTM.trace_map_prefix
{n n' : ℕ}
(source : NTM n)
(target : NTM n')
(wrap : Cfg n source.Q → Cfg n' target.Q)
(step :
∀ (choice : Bool) (c : Cfg n source.Q),
c.state ≠ source.qhalt →
target.trace 1 (fun (x : Fin 1) => choice) (wrap c) = wrap (source.trace 1 (fun (x : Fin 1) => choice) c))
(T : ℕ)
(choices : Fin T → Bool)
(c : Cfg n source.Q)
(running : ∀ (t : ℕ) (ht : t < T), (source.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c).state ≠ source.qhalt)
:
Transport an exact trace through a configuration map, preserving every choice bit. The source must be running at each proper prefix, but may halt at the endpoint. The target may continue after that halt: no halt reflection or injectivity is assumed.