Topology of packed one-step circuit fragments

This internal module proves that a packed transition fragment is topologically well formed whenever its choice wire and incoming configuration block lie in the existing circuit prefix.

theorem Complexity.CircuitUnrolling.stepFragment_topologicallyWellFormed_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) [NeZero available] (hchoice : choiceWire < available) (hconfig : configBase + configWidth tm T ≤ available) : CircuitCode.RawCircuit.TopologicallyWellFormed available (stepFragment tm T configBase choiceWire available)

Internal topological well-formedness of a packed one-step fragment.