Variable support of transition formulas

This internal module proves that every one-step transition formula reads only its designated choice wire and the atom wires of the incoming configuration. The resulting numeric bound is the topological-ordering premise needed by the packed Boolean-formula compiler.

theorem Complexity.CircuitUnrolling.mem_vars_nextFormula_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (atom : ConfigAtom tm T) (i : ℕ) (hi : i ∈ (nextFormula tm T base choiceWire atom).vars) : i = choiceWire ∨ ∃ (oldAtom : ConfigAtom tm T), i = configWire tm T base oldAtom

Internal support law for every next-configuration formula variable.

theorem Complexity.CircuitUnrolling.vars_nextFormula_lt_internal {k : ℕ} (tm : NTM k) (T base choiceWire available : ℕ) (atom : ConfigAtom tm T) (hchoice : choiceWire < available) (hconfig : base + configWidth tm T ≤ available) (i : ℕ) : i ∈ (nextFormula tm T base choiceWire atom).vars → i < available

Internal numeric support bound used to compile a transition after a prefix.