Wiring the geometric phase evaluator

The generated point block precedes the original input. Constant validity flags discard the zero scalar. Each request payload carries both its original data and the complete generated point list of that candidate, so accepted point lists can become occupancy inputs in the next phase.

@[reducible, inline]

abbrev Algebraic.MassProduction.Nonuniform.GeometricPhaseLayout.generatedBits (menuDepth requestDepth dimension width : ℕ) : ℕ

Total width of the generated point block.

Equations

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

noncomputable def Algebraic.MassProduction.Nonuniform.GeometricPhaseLayout.validWires {width : ℕ} (positive : 0 < width) (menuDepth requestDepth inputs dimension : ℕ) (index : Fin (Sorting.networkRecords (menuDepth + requestDepth + width))) : DeMorgan.Wiring (generatedBits menuDepth requestDepth dimension width + inputs)

Constant scalar-validity flags for every menu point.

Equations

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

def Algebraic.MassProduction.Nonuniform.GeometricPhaseLayout.keyWires (menuDepth requestDepth inputs dimension width : ℕ) (index : Fin (Sorting.networkRecords (menuDepth + requestDepth + width))) (bit : Fin (dimension * width)) : DeMorgan.Wiring (generatedBits menuDepth requestDepth dimension width + inputs)

The point address of a generated record.

Equations

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

def Algebraic.MassProduction.Nonuniform.GeometricPhaseLayout.payloadWires {requestDepth requestWidth inputs : ℕ} (menuDepth dimension width : ℕ) (original : Fin (Sorting.networkRecords requestDepth) → Fin requestWidth → DeMorgan.Wiring inputs) (line : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) : Fin (requestWidth + 2 ^ width * (dimension * width)) → DeMorgan.Wiring (generatedBits menuDepth requestDepth dimension width + inputs)

Carry original request data followed by all candidate-specific point bits.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.GeometricPhaseLayout.validWires_eval {width menuDepth requestDepth dimension inputs : ℕ} (positive : 0 < width) (prepared : Fin (generatedBits menuDepth requestDepth dimension width + inputs) → Bool) (candidate : Fin (Sorting.networkRecords menuDepth)) (request : Fin (Sorting.networkRecords requestDepth)) (slot : Fin (2 ^ width)) : DeMorgan.Wiring.eval prepared (validWires positive menuDepth requestDepth inputs dimension ((PowerLayout.points menuDepth requestDepth width) (candidate, request, slot))) = PaddedLinePoints.valid positive slot

Padded validity is preserved at the corresponding triple index.

theorem Algebraic.MassProduction.Nonuniform.GeometricPhaseLayout.keyWires_eval {width menuDepth requestDepth dimension inputs : ℕ} (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) (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) (candidate : Fin (Sorting.networkRecords menuDepth)) (request : Fin (Sorting.networkRecords requestDepth)) (slot : Fin (2 ^ width)) (bit : Fin (dimension * width)) : DeMorgan.Wiring.eval ((PreparedInputs.circuit (AffineMenuPoints.circuit positive menu targetWires)).eval DeMorgan.interpretation input) (keyWires menuDepth requestDepth inputs dimension width ((PowerLayout.points menuDepth requestDepth width) (candidate, request, slot)) bit) = binaryExtensionVectorBits positive (PaddedLinePoints.point positive (targets request) (menu candidate request) slot) bit

Generated point keys have the exact field-level affine-line semantics.

theorem Algebraic.MassProduction.Nonuniform.GeometricPhaseLayout.requestSet_eq {width menuDepth requestDepth dimension inputs : ℕ} (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) (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) (candidate : Fin (Sorting.networkRecords menuDepth)) (request : Fin (Sorting.networkRecords requestDepth)) : MenuSelection.requestSet (PowerLayout.points menuDepth requestDepth width) (validWires positive menuDepth requestDepth inputs dimension) (keyWires menuDepth requestDepth inputs dimension width) ((PreparedInputs.circuit (AffineMenuPoints.circuit positive menu targetWires)).eval DeMorgan.interpretation input) candidate request = Finset.image (binaryExtensionVectorBits positive) (puncturedLine (targets request) (menu candidate request))

The set tested by the menu evaluator is precisely the encoded punctured line.

theorem Algebraic.MassProduction.Nonuniform.GeometricPhaseLayout.payloadWires_original_eval {inputs menuDepth requestDepth dimension width requestWidth : ℕ} (generated : Circuit DeMorgan.signature inputs (generatedBits menuDepth requestDepth dimension width)) (original : Fin (Sorting.networkRecords requestDepth) → Fin requestWidth → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (candidate : Fin (Sorting.networkRecords menuDepth)) (request : Fin (Sorting.networkRecords requestDepth)) (bit : Fin requestWidth) : DeMorgan.Wiring.eval ((PreparedInputs.circuit generated).eval DeMorgan.interpretation input) (payloadWires menuDepth dimension width original (finProdFinEquiv (candidate, request)) (Fin.castAdd (2 ^ width * (dimension * width)) bit)) = DeMorgan.Wiring.eval input (original request bit)

Original request data is carried without modification.

theorem Algebraic.MassProduction.Nonuniform.GeometricPhaseLayout.payloadWires_point_eval {requestDepth requestWidth inputs menuDepth dimension width : ℕ} (original : Fin (Sorting.networkRecords requestDepth) → Fin requestWidth → DeMorgan.Wiring inputs) (prepared : Fin (generatedBits menuDepth requestDepth dimension width + inputs) → Bool) (candidate : Fin (Sorting.networkRecords menuDepth)) (request : Fin (Sorting.networkRecords requestDepth)) (slot : Fin (2 ^ width)) (bit : Fin (dimension * width)) : DeMorgan.Wiring.eval prepared (payloadWires menuDepth dimension width original (finProdFinEquiv (candidate, request)) (Fin.natAdd requestWidth (finProdFinEquiv (slot, bit)))) = DeMorgan.Wiring.eval prepared (keyWires menuDepth requestDepth inputs dimension width ((PowerLayout.points menuDepth requestDepth width) (candidate, request, slot)) bit)

The point-list suffix of a request payload carries the generated keys.

theorem Algebraic.MassProduction.Nonuniform.GeometricPhaseLayout.occupied_prepared {inputs outputs sources keyWidth : ℕ} (generated : Circuit DeMorgan.signature inputs outputs) (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) : MenuPointLayout.occupied (fun (source : Fin sources) (bit : Fin keyWidth) => PreparedInputs.original outputs (sourceKeys source bit)) (fun (source : Fin sources) => PreparedInputs.original outputs (sourceFlags source)) ((PreparedInputs.circuit generated).eval DeMorgan.interpretation input) = MenuPointLayout.occupied sourceKeys sourceFlags input

Lifting source wires past preprocessing preserves their occupied set.

theorem Algebraic.MassProduction.Nonuniform.GeometricPhaseLayout.requestClean_iff {width menuDepth requestDepth dimension inputs sources : ℕ} (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) (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) (candidate : Fin (Sorting.networkRecords menuDepth)) (request : Fin (Sorting.networkRecords requestDepth)) : MenuSelection.RequestClean (PowerLayout.points menuDepth requestDepth width) (validWires positive menuDepth requestDepth inputs dimension) (keyWires menuDepth requestDepth inputs dimension width) (fun (source : Fin sources) (bit : Fin (dimension * width)) => PreparedInputs.original (generatedBits menuDepth requestDepth dimension width) (sourceKeys source bit)) (fun (source : Fin sources) => PreparedInputs.original (generatedBits menuDepth requestDepth dimension width) (sourceFlags source)) ((PreparedInputs.circuit (AffineMenuPoints.circuit positive menu targetWires)).eval DeMorgan.interpretation input) candidate request ↔ Clean (fun (request : Fin (Sorting.networkRecords requestDepth)) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) => puncturedLine (targets request) direction) occupied (menu candidate) request

The evaluator's encoded cleanliness predicate is exactly geometric cleanliness.