Interpreting a flat menu point array

An equivalence identifies the sorting-network records with candidate, request, and point-slot triples. Candidate identifiers are fixed and injective. Under this layout the point-conflict circuit computes precisely the enumerated recovery-set conflict predicate for each candidate.

def Algebraic.MassProduction.Nonuniform.MenuPointLayout.groups {candidates requests slots depth groupWidth : ℕ} (layout : Fin candidates × Fin requests × Fin slots ≃ Fin (Sorting.networkRecords depth)) (codes : Fin candidates → Fin groupWidth → Bool) (index : Fin (Sorting.networkRecords depth)) : Fin groupWidth → Bool

The candidate identifier of each flat point record.

Equations

• Algebraic.MassProduction.Nonuniform.MenuPointLayout.groups layout codes index = codes (layout.symm index).1

def Algebraic.MassProduction.Nonuniform.MenuPointLayout.occupied {sources keyWidth inputs : ℕ} (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) : Finset (Fin keyWidth → Bool)

The occupied points represented by active source flags.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.MenuPointLayout.mem_occupied_iff {sources keyWidth inputs : ℕ} (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (point : Fin keyWidth → Bool) : point ∈ occupied sourceKeys sourceFlags input ↔ ∃ (source : Fin sources), (fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (sourceKeys source bit)) = point ∧ DeMorgan.Wiring.eval input (sourceFlags source) = true

Source matching is exactly membership in the occupied point set.

theorem Algebraic.MassProduction.Nonuniform.MenuPointLayout.pointCircuit_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) (slot : Fin slots) : (PointConflicts.circuit (groups layout codes) valid keys sourceKeys sourceFlags recordCount).eval DeMorgan.interpretation input (layout (candidate, request, slot)) = true ↔ EnumeratedClean.Conflict (fun (request : Fin requests) (slot : Fin slots) => DeMorgan.Wiring.eval input (valid (layout (candidate, request, slot)))) (fun (request : Fin requests) (slot : Fin slots) (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys (layout (candidate, request, slot)) bit)) (occupied sourceKeys sourceFlags input) request slot

The flat circuit computes the exact conflict predicate of one candidate.