Generating every fixed-menu recovery line

All candidate directions are offline constants. Each point record selects its request's target bits and adds a precomputed scalar multiple of its candidate direction. One fixed circuit emits the full power-of-two menu array, costing at most one gate per point bit.

noncomputable def Algebraic.MassProduction.Nonuniform.AffineMenuPoints.offsets {width menuDepth requestDepth dimension : ℕ} (positive : 0 < width) (menu : Fin (Sorting.networkRecords menuDepth) → Fin (Sorting.networkRecords requestDepth) → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (index : Fin (Sorting.networkRecords (menuDepth + requestDepth + width))) : Fin (dimension * width) → Bool

Fixed affine offset for each candidate/request/scalar record.

Equations

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

def Algebraic.MassProduction.Nonuniform.AffineMenuPoints.sources {requestDepth dimension width inputs menuDepth : ℕ} (targets : Fin (Sorting.networkRecords requestDepth) → Fin (dimension * width) → DeMorgan.Wiring inputs) (index : Fin (Sorting.networkRecords (menuDepth + requestDepth + width))) : Fin (dimension * width) → DeMorgan.Wiring inputs

Every generated point selects the target of its original request.

Equations

• Algebraic.MassProduction.Nonuniform.AffineMenuPoints.sources targets index = targets ((Algebraic.MassProduction.Nonuniform.PowerLayout.points menuDepth requestDepth width).symm index).2.1

noncomputable def Algebraic.MassProduction.Nonuniform.AffineMenuPoints.circuit {width menuDepth requestDepth dimension inputs : ℕ} (positive : 0 < width) (menu : Fin (Sorting.networkRecords menuDepth) → Fin (Sorting.networkRecords requestDepth) → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (targets : Fin (Sorting.networkRecords requestDepth) → Fin (dimension * width) → DeMorgan.Wiring inputs) : Circuit DeMorgan.signature inputs (Sorting.networkRecords (menuDepth + requestDepth + width) * (dimension * width))

Generate every recovery-line point of every fixed candidate.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.AffineMenuPoints.circuit_size {width menuDepth requestDepth dimension inputs : ℕ} (positive : 0 < width) (menu : Fin (Sorting.networkRecords menuDepth) → Fin (Sorting.networkRecords requestDepth) → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (targets : Fin (Sorting.networkRecords requestDepth) → Fin (dimension * width) → DeMorgan.Wiring inputs) : (circuit positive menu targets).size = (ConstantTranslations.circuit (offsets positive menu) (sources targets)).size

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

theorem Algebraic.MassProduction.Nonuniform.AffineMenuPoints.circuit_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)) : (circuit positive menu targetWires).eval DeMorgan.interpretation input (finProdFinEquiv ((PowerLayout.points menuDepth requestDepth width) (candidate, request, slot), bit)) = binaryExtensionVectorBits positive (PaddedLinePoints.point positive (targets request) (menu candidate request) slot) bit

Exact field semantics at every fixed candidate/request/scalar output.

theorem Algebraic.MassProduction.Nonuniform.AffineMenuPoints.circuit_cost_le {width menuDepth requestDepth dimension inputs : ℕ} (positive : 0 < width) (menu : Fin (Sorting.networkRecords menuDepth) → Fin (Sorting.networkRecords requestDepth) → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (targets : Fin (Sorting.networkRecords requestDepth) → Fin (dimension * width) → DeMorgan.Wiring inputs) : (circuit positive menu targets).cost DeMorgan.standardCost ≤ Sorting.networkRecords (menuDepth + requestDepth + width) * (dimension * width)

All point generation is linear in the total number of emitted bits.