A universal nonuniform geometric phase

Under the finite-field packing budget, one fixed menu and its concrete circuit handle every encoded occupied state and target tuple. The output accepts exactly the rounded-up half prefix. The menu-success premise of the geometric circuit is discharged by the finite counting theorem.

theorem Algebraic.MassProduction.Nonuniform.GeometricPhase.existsUniversalPhase {width dimension requestDepth inputs sources requestWidth padding routingDepth : ℕ} (positive : 0 < width) (dimensionPositive : 0 < dimension) (capacity : ℕ) (activeLe : Sorting.networkRecords requestDepth ≤ capacity) (budget : 512 * capacity * Nat.card (BinaryExtension width) ≤ Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (targetWires : Fin (Sorting.networkRecords requestDepth) → Fin (dimension * width) → DeMorgan.Wiring inputs) (sourceKeys : Fin sources → Fin (dimension * width) → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (original : Fin (Sorting.networkRecords requestDepth) → Fin requestWidth → DeMorgan.Wiring inputs) (recordCount : sources + Sorting.networkRecords (phaseMenuDepth capacity (Sorting.networkRecords requestDepth) (dimension * width) + requestDepth + width) + padding = Sorting.networkRecords routingDepth) : ∃ (menu : Fin (Sorting.networkRecords (phaseMenuDepth capacity (Sorting.networkRecords requestDepth) (dimension * width))) → Fin (Sorting.networkRecords requestDepth) → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), ∀ (input : Fin inputs → Bool) (state : PhaseState (Fin dimension → BinaryExtension width) (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) capacity (Sorting.networkRecords requestDepth)), (∀ (request : Fin (Sorting.networkRecords requestDepth)) (bit : Fin (dimension * width)), DeMorgan.Wiring.eval input (targetWires request bit) = binaryExtensionVectorBits positive (state.2 request) bit) → MenuPointLayout.occupied sourceKeys sourceFlags input = Finset.image (binaryExtensionVectorBits positive) (phaseOccupied state) → (Function.Injective fun (request : Fin (Sorting.networkRecords requestDepth)) (bit : Fin requestWidth) => DeMorgan.Wiring.eval input (original request bit)) → CorrectOutput positive menu (fun (request : Fin (Sorting.networkRecords requestDepth)) (bit : Fin requestWidth) => DeMorgan.Wiring.eval input (original request bit)) state.2 (phaseOccupied state) (acceptedCount requestDepth) ((circuit positive menu targetWires sourceKeys sourceFlags original recordCount ⋯ ⋯).eval DeMorgan.interpretation input)

One fixed concrete phase circuit works for every encoded state under the packing budget, with no successful-menu premise left to the caller.