Universal power-of-two menus for encoded binary-field states

Points and projective directions fit in the same dimension * width bits. The covering-menu theorem therefore applies directly to the field and request counts used by the geometric phase circuit.

theorem Algebraic.MassProduction.Nonuniform.projectiveRep_injective {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : Function.Injective fun (direction : Projectivization K V) => direction.rep

Choosing a projective representative is injective as a function of directions.

theorem Algebraic.MassProduction.Nonuniform.existsBinaryPowerPhaseMenu {width dimension : ℕ} (positive : 0 < width) (dimensionPositive : 0 < dimension) (capacity requestDepth : ℕ) (activeLe : Sorting.networkRecords requestDepth ≤ capacity) (budget : 512 * capacity * Nat.card (BinaryExtension width) ≤ Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (menu : Fin (Sorting.networkRecords (phaseMenuDepth capacity (Sorting.networkRecords requestDepth) (dimension * width))) → Fin (Sorting.networkRecords requestDepth) → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), ∀ (state : PhaseState (Fin dimension → BinaryExtension width) (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) capacity (Sorting.networkRecords requestDepth)), ∃ (entry : Fin (Sorting.networkRecords (phaseMenuDepth capacity (Sorting.networkRecords requestDepth) (dimension * width)))), HalfClean state (menu entry)

A fixed binary-field menu covers all phase states under the packing budget.