Restore final one-bit results by their original request identifiers

Only result bits and identifiers participate in the final routing pass. The scheduler's full point-list records need not be sorted again.

theorem Algebraic.MassProduction.Nonuniform.RestoreRequestOrder.existsCircuit {requests idWidth inputs : ℕ} (codes : Fin requests → Fin idWidth → Bool) (distinct : Function.Injective codes) (identifiers : Fin requests → Fin idWidth → DeMorgan.Wiring inputs) (values : Fin requests → DeMorgan.Wiring inputs) : ∃ (restored : Circuit DeMorgan.signature inputs requests), restored.cost DeMorgan.standardCost ≤ 256 * (requests + requests + 1) * (FiniteParameters.binaryDepth (requests + requests + 1) + idWidth + 1 + 2) ^ 5 ∧ ∀ (input : Fin inputs → Bool) (order : Equiv.Perm (Fin requests)), (∀ (request : Fin requests) (bit : Fin idWidth), DeMorgan.Wiring.eval input (identifiers request bit) = codes (order request) bit) → ∀ (request : Fin requests), restored.eval DeMorgan.interpretation input (order request) = DeMorgan.Wiring.eval input (values request)

One shared routing pass restores a permuted array of Boolean results. The identifier permutation is semantic input data, not an offline circuit choice, so the same circuit works for every scheduler output order.