A complete nonuniform near-linear geometric scheduler

For a power-of-two batch, one fixed circuit accepts arbitrary request payloads with encoded geometric targets. It adds distinct identifiers, executes every halving phase, and returns all payloads and disjoint recovery point lists. Menu choices precede the input. Repeated targets are allowed.

theorem Algebraic.MassProduction.Nonuniform.Scheduler.existsCircuit {width dimension depth payloadWidth inputs : ℕ} (positive : 0 < width) (dimensionPositive : 0 < dimension) (budget : 512 * Sorting.networkRecords depth * Nat.card (BinaryExtension width) ≤ Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (original : Fin (Sorting.networkRecords depth) → Fin payloadWidth → DeMorgan.Wiring inputs) (targetProjection : Fin (dimension * width) → Fin payloadWidth) : ∃ (scheduler : Circuit DeMorgan.signature inputs (BufferInput.inputWidth (Sorting.networkRecords depth) 0 (depth + payloadWidth) (2 ^ width) (dimension * width))), scheduler.cost DeMorgan.standardCost ≤ Sorting.networkRecords depth * 2 ^ width * BufferIteration.polynomialFactor (Sorting.networkRecords depth) dimension width (depth + payloadWidth) ∧ ∀ (input : Fin inputs → Bool) (targets : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width), (∀ (request : Fin (Sorting.networkRecords depth)) (bit : Fin (dimension * width)), DeMorgan.Wiring.eval input (original request (targetProjection bit)) = binaryExtensionVectorBits positive (targets request) bit) → ∃ (state : BufferModel.State (Sorting.networkRecords depth) (Sorting.networkRecords depth) 0 dimension width), scheduler.eval DeMorgan.interpretation input = BufferModel.input positive state (TaggedBuffer.data original input) targets ∧ BufferModel.WellScheduled state targets

A fixed circuit schedules the entire batch with a cost linear in the number of request/scalar pairs, up to the displayed polynomial factor. The output model retains exact original identities and request payloads.