A complete fixed-menu geometric phase circuit

Generate all affine-line points, retain the original input, evaluate the menu, and select a clean request prefix. The output retains original request data and every point of the selected candidate's lines. Correctness for an encoded occupied state is established separately.

noncomputable def Algebraic.MassProduction.Nonuniform.GeometricPhase.selector {width sources dimension inputs requestDepth requestWidth padding routingDepth needed : ℕ} (positive : 0 < width) (menuDepth : ℕ) (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) : Circuit DeMorgan.signature (GeometricPhaseLayout.generatedBits menuDepth requestDepth dimension width + inputs) (CandidateSelection.rowBits requestDepth (requestWidth + 2 ^ width * (dimension * width)))

Evaluate the menu using generated point bits and preserved source data.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.Nonuniform.GeometricPhase.selector_size {width sources dimension inputs requestDepth requestWidth padding routingDepth needed : ℕ} (positive : 0 < width) (menuDepth : ℕ) (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) : (selector positive menuDepth sourceKeys sourceFlags original recordCount neededPositive neededFits).size = (MenuSelection.circuit (PowerLayout.points menuDepth requestDepth width) (PowerLayout.codes menuDepth) (GeometricPhaseLayout.validWires positive menuDepth requestDepth inputs dimension) (GeometricPhaseLayout.keyWires menuDepth requestDepth inputs dimension width) (fun (source : Fin sources) (bit : Fin (dimension * width)) => PreparedInputs.original (GeometricPhaseLayout.generatedBits menuDepth requestDepth dimension width) (sourceKeys source bit)) (fun (source : Fin sources) => PreparedInputs.original (GeometricPhaseLayout.generatedBits menuDepth requestDepth dimension width) (sourceFlags source)) recordCount (GeometricPhaseLayout.payloadWires menuDepth dimension width original) neededPositive neededFits).size

selector has exactly the gates of MenuSelection.circuit; the surrounding wiring adds none.

noncomputable def Algebraic.MassProduction.Nonuniform.GeometricPhase.circuit {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) : Circuit DeMorgan.signature inputs (CandidateSelection.rowBits requestDepth (requestWidth + 2 ^ width * (dimension * width)))

One complete geometric phase: point generation followed by menu selection.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.Nonuniform.GeometricPhase.circuit_size {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) : (circuit positive menu targetWires sourceKeys sourceFlags original recordCount neededPositive neededFits).size = (PreparedInputs.circuit (AffineMenuPoints.circuit positive menu targetWires)).size + (selector positive menuDepth sourceKeys sourceFlags original recordCount neededPositive neededFits).size

The exact gate count of circuit.

def Algebraic.MassProduction.Nonuniform.GeometricPhase.costBound (menuDepth requestDepth width dimension routingDepth requestWidth : ℕ) : ℕ

Explicit arithmetic bound for the geometric phase, including point generation.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.Nonuniform.GeometricPhase.circuit_cost_le {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) : (circuit positive menu targetWires sourceKeys sourceFlags original recordCount neededPositive neededFits).cost DeMorgan.standardCost ≤ costBound menuDepth requestDepth width dimension routingDepth requestWidth

The complete phase has the displayed linear point-count cost bound.