Circuit evaluation of every candidate's clean requests

Shared point-conflict detection followed by one finite OR per request returns the exact clean-request predicate for every candidate. The cost includes one occupancy router for the whole menu and is linear in the number of point records up to polynomial width and sorting-depth factors.

def Algebraic.MassProduction.Nonuniform.MenuClean.pointIndices {candidates requests slots depth : ℕ} (layout : Fin candidates × Fin requests × Fin slots ≃ Fin (Sorting.networkRecords depth)) (line : Fin (candidates * requests)) (slot : Fin slots) : Fin (Sorting.networkRecords depth)

Point slots of the request at a row-major candidate-request position.

Equations

• Algebraic.MassProduction.Nonuniform.MenuClean.pointIndices layout line slot = layout ((finProdFinEquiv.symm line).1, (finProdFinEquiv.symm line).2, slot)

noncomputable def Algebraic.MassProduction.Nonuniform.MenuClean.circuit {candidates requests slots depth groupWidth inputs keyWidth sources padding routingDepth : ℕ} (layout : Fin candidates × Fin requests × Fin slots ≃ Fin (Sorting.networkRecords depth)) (codes : Fin candidates → Fin groupWidth → Bool) (valid : Fin (Sorting.networkRecords depth) → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (recordCount : sources + Sorting.networkRecords depth + padding = Sorting.networkRecords routingDepth) : Circuit DeMorgan.signature inputs (candidates * requests)

The complete menu clean-flag circuit, before choosing a successful row.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.MenuClean.circuit_size {candidates requests slots depth groupWidth inputs keyWidth sources padding routingDepth : ℕ} (layout : Fin candidates × Fin requests × Fin slots ≃ Fin (Sorting.networkRecords depth)) (codes : Fin candidates → Fin groupWidth → Bool) (valid : Fin (Sorting.networkRecords depth) → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (recordCount : sources + Sorting.networkRecords depth + padding = Sorting.networkRecords routingDepth) : (circuit layout codes valid keys sourceKeys sourceFlags recordCount).size = (GroupClean.circuit (pointIndices layout) (PointConflicts.circuit (MenuPointLayout.groups layout codes) valid keys sourceKeys sourceFlags recordCount)).size

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

theorem Algebraic.MassProduction.Nonuniform.MenuClean.circuit_eval_iff {candidates requests slots depth groupWidth inputs keyWidth sources padding routingDepth : ℕ} (layout : Fin candidates × Fin requests × Fin slots ≃ Fin (Sorting.networkRecords depth)) (codes : Fin candidates → Fin groupWidth → Bool) (codesInjective : Function.Injective codes) (valid : Fin (Sorting.networkRecords depth) → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (recordCount : sources + Sorting.networkRecords depth + padding = Sorting.networkRecords routingDepth) (input : Fin inputs → Bool) (candidate : Fin candidates) (request : Fin requests) (withinRequest : ∀ (request : Fin requests) (left right : Fin slots), DeMorgan.Wiring.eval input (valid (layout (candidate, request, left))) = true → DeMorgan.Wiring.eval input (valid (layout (candidate, request, right))) = true → ((fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys (layout (candidate, request, left)) bit)) = fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys (layout (candidate, request, right)) bit)) → left = right) : (circuit layout codes valid keys sourceKeys sourceFlags recordCount).eval DeMorgan.interpretation input (finProdFinEquiv (candidate, request)) = true ↔ Clean (fun (request : Fin requests) (x : Unit) => EnumeratedClean.pointSet (fun (slot : Fin slots) => DeMorgan.Wiring.eval input (valid (layout (candidate, request, slot)))) fun (slot : Fin slots) (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys (layout (candidate, request, slot)) bit)) (MenuPointLayout.occupied sourceKeys sourceFlags input) (fun (x : Fin requests) => ()) request

Every fixed output is exactly its candidate's clean-request predicate.

theorem Algebraic.MassProduction.Nonuniform.MenuClean.circuit_cost_le {candidates requests slots depth groupWidth inputs keyWidth sources padding routingDepth : ℕ} (layout : Fin candidates × Fin requests × Fin slots ≃ Fin (Sorting.networkRecords depth)) (codes : Fin candidates → Fin groupWidth → Bool) (valid : Fin (Sorting.networkRecords depth) → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (recordCount : sources + Sorting.networkRecords depth + padding = Sorting.networkRecords routingDepth) : (circuit layout codes valid keys sourceKeys sourceFlags recordCount).cost DeMorgan.standardCost ≤ 256 * Sorting.networkRecords depth * (depth + (groupWidth + (1 + keyWidth)) + 1) ^ 5 + 128 * Sorting.networkRecords routingDepth * (routingDepth + keyWidth + 1 + 2) ^ 5 + 2 * Sorting.networkRecords depth + candidates * requests * (slots + 1)

Explicit cost: one duplicate detector, one shared occupancy router, two combining gates per point, and one aggregation per request.