Array-level evaluation of packed transition fragments

This internal adapter derives the abstract assignment expected by the formula compiler directly from the concrete input array. Consequently, clients can evaluate a packed transition using an encoded configuration and an actual choice wire, without separately constructing a total Boolean assignment.

theorem Complexity.CircuitUnrolling.evalAux?_stepFragment_of_encodes_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) [NeZero available] (choice : Bool) (wires : Array Bool) (c : Cfg k tm.Q) (hsize : wires.size = available) (hchoice : wires[choiceWire]? = some choice) (hconfig : EncodesConfig tm T configBase wires c) (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)

Evaluate one packed step directly from a concrete encoded configuration and choice wire.