Correctness of a complete fixed-menu geometric phase

For encoded targets and occupancy, the circuit chooses one successful candidate, preserves every original request as a permutation, carries its complete generated point list, and returns a clean prefix. The menu-success premise can be supplied by the universal phase-menu theorem.

theorem Algebraic.MassProduction.Nonuniform.GeometricPhase.circuit_correct {width menuDepth requestDepth dimension inputs sources requestWidth padding routingDepth needed : ℕ} (positive : 0 < width) (menu : Fin (Sorting.networkRecords menuDepth) → Fin (Sorting.networkRecords requestDepth) → 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 (menuDepth + requestDepth + width) + padding = Sorting.networkRecords routingDepth) (neededPositive : 0 < needed) (neededFits : needed ≤ Sorting.networkRecords requestDepth) (input : Fin inputs → Bool) (targets : Fin (Sorting.networkRecords requestDepth) → Fin dimension → BinaryExtension width) (targetsCorrect : ∀ (request : Fin (Sorting.networkRecords requestDepth)) (bit : Fin (dimension * width)), DeMorgan.Wiring.eval input (targetWires request bit) = binaryExtensionVectorBits positive (targets request) bit) (occupied : Finset (Fin dimension → BinaryExtension width)) (occupiedCorrect : MenuPointLayout.occupied sourceKeys sourceFlags input = Finset.image (binaryExtensionVectorBits positive) occupied) (available : ∃ (candidate : Fin (Sorting.networkRecords menuDepth)), needed ≤ Nat.card { request : Fin (Sorting.networkRecords requestDepth) // Clean (fun (request : Fin (Sorting.networkRecords requestDepth)) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) => puncturedLine (targets request) direction) occupied (menu candidate) request }) (distinct : Function.Injective fun (request : Fin (Sorting.networkRecords requestDepth)) (bit : Fin requestWidth) => DeMorgan.Wiring.eval input (original request bit)) : ∃ (candidate : Fin (Sorting.networkRecords menuDepth)) (order : Equiv.Perm (Fin (Sorting.networkRecords requestDepth))), (∀ (request : Fin (Sorting.networkRecords requestDepth)) (bit : Fin requestWidth), Sorting.flatRecords ((circuit positive menu targetWires sourceKeys sourceFlags original recordCount neededPositive neededFits).eval DeMorgan.interpretation input) request (Fin.natAdd 1 (Fin.castAdd (2 ^ width * (dimension * width)) bit)) = DeMorgan.Wiring.eval input (original (order request) bit)) ∧ (∀ (request : Fin (Sorting.networkRecords requestDepth)) (slot : Fin (2 ^ width)) (bit : Fin (dimension * width)), Sorting.flatRecords ((circuit positive menu targetWires sourceKeys sourceFlags original recordCount neededPositive neededFits).eval DeMorgan.interpretation input) request (Fin.natAdd 1 (Fin.natAdd requestWidth (finProdFinEquiv (slot, bit)))) = binaryExtensionVectorBits positive (PaddedLinePoints.point positive (targets (order request)) (menu candidate (order request)) slot) bit) ∧ ∀ (request : Fin (Sorting.networkRecords requestDepth)), ↑request < needed → Clean (fun (request : Fin (Sorting.networkRecords requestDepth)) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) => puncturedLine (targets request) direction) occupied (menu candidate) (order request)

The complete phase preserves request data and point lists while selecting the requested number of pairwise-disjoint, unoccupied recovery lines.