Evaluation of packed one-step circuit fragments

This internal module lifts the semantics of individual transition formulas through the formula batch compiler. The packed outputs form a fresh encoded configuration block for the halted-or-successor machine configuration.

theorem Complexity.CircuitUnrolling.evalAux?_stepFragment_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) [NeZero available] (choice : Bool) (assignment : ℕ → Bool) (wires : Array Bool) (c : Cfg k tm.Q) (hsize : wires.size = available) (hinput : ∀ i < available, wires[i]? = some (assignment i)) (hchoice : assignment choiceWire = choice) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T configBase atom) = ConfigAtom.value c atom) (hchoiceBound : choiceWire < available) (hconfigBound : configBase + configWidth tm T ≤ available) (hheads : HeadsLt T c) : ∃ (result : Array Bool), (stepFragment tm T configBase choiceWire available).evalAux? wires = some result ∧ result.size = wires.size + stepFragmentSize tm T configBase choiceWire ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ EncodesConfig tm T (stepOutputBase tm T configBase choiceWire available) result (choiceStep tm choice c)

Internal evaluation theorem for a packed one-step transition fragment.