Shared conflict detection for all candidate points

Each point carries a fixed candidate identifier and a validity flag. Equal points from different candidates do not collide. Invalid slots do not cause conflicts. One source array represents occupied points for the whole menu. The circuit combines duplicate detection and shared occupancy lookup and returns conflict flags in original point order.

def Algebraic.MassProduction.Nonuniform.PointConflicts.taggedKeys {depth groupWidth inputs keyWidth : ℕ} (groups : Fin (Sorting.networkRecords depth) → Fin groupWidth → Bool) (valid : Fin (Sorting.networkRecords depth) → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (index : Fin (Sorting.networkRecords depth)) : Fin (groupWidth + (1 + keyWidth)) → DeMorgan.Wiring inputs

Group and validity tags precede the point address in the collision key.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.PointConflicts.taggedKeys_eq_iff {depth groupWidth inputs keyWidth : ℕ} (groups : Fin (Sorting.networkRecords depth) → Fin groupWidth → Bool) (valid : Fin (Sorting.networkRecords depth) → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (left right : Fin (Sorting.networkRecords depth)) : ((fun (bit : Fin (groupWidth + (1 + keyWidth))) => DeMorgan.Wiring.eval input (taggedKeys groups valid keys left bit)) = fun (bit : Fin (groupWidth + (1 + keyWidth))) => DeMorgan.Wiring.eval input (taggedKeys groups valid keys right bit)) ↔ groups left = groups right ∧ DeMorgan.Wiring.eval input (valid left) = DeMorgan.Wiring.eval input (valid right) ∧ (fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys left bit)) = fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys right bit)

Equality of collision keys means equality of each of their three fields.

noncomputable def Algebraic.MassProduction.Nonuniform.PointConflicts.occupancyCircuit {sources keyWidth inputs depth padding routingDepth : ℕ} (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (recordCount : sources + Sorting.networkRecords depth + padding = Sorting.networkRecords routingDepth) : Circuit DeMorgan.signature inputs (Sorting.networkRecords depth)

One shared occupied-point lookup, with one Boolean flag per query.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.PointConflicts.occupancyCircuit_size {sources keyWidth inputs depth padding routingDepth : ℕ} (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (recordCount : sources + Sorting.networkRecords depth + padding = Sorting.networkRecords routingDepth) : (occupancyCircuit sourceKeys sourceFlags keys recordCount).size = (BatchOr.circuit sourceKeys (fun (source : Fin sources) (x : Fin 1) => sourceFlags source) keys recordCount).size

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

theorem Algebraic.MassProduction.Nonuniform.PointConflicts.occupancyCircuit_eval_iff {sources keyWidth inputs depth padding routingDepth : ℕ} (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (recordCount : sources + Sorting.networkRecords depth + padding = Sorting.networkRecords routingDepth) (input : Fin inputs → Bool) (index : Fin (Sorting.networkRecords depth)) : (occupancyCircuit sourceKeys sourceFlags keys recordCount).eval DeMorgan.interpretation input index = true ↔ ∃ (source : Fin sources), ((fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (sourceKeys source bit)) = fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys index bit)) ∧ DeMorgan.Wiring.eval input (sourceFlags source) = true

Occupancy is exactly the existence of an active matching source.

noncomputable def Algebraic.MassProduction.Nonuniform.PointConflicts.circuit {depth groupWidth inputs keyWidth sources padding routingDepth : ℕ} (groups : Fin (Sorting.networkRecords depth) → 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 (Sorting.networkRecords depth)

Detect every valid point conflict for all candidates at once.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.PointConflicts.circuit_size {depth groupWidth inputs keyWidth sources padding routingDepth : ℕ} (groups : Fin (Sorting.networkRecords depth) → 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 groups valid keys sourceKeys sourceFlags recordCount).size = (MaskedOr.circuit (DuplicateFlags.circuit (taggedKeys groups valid keys)) (occupancyCircuit sourceKeys sourceFlags keys recordCount) (DeMorgan.Wiring.circuit valid)).size

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

theorem Algebraic.MassProduction.Nonuniform.PointConflicts.circuit_eval_iff {depth groupWidth inputs keyWidth sources padding routingDepth : ℕ} (groups : Fin (Sorting.networkRecords depth) → 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) (input : Fin inputs → Bool) (index : Fin (Sorting.networkRecords depth)) : (circuit groups valid keys sourceKeys sourceFlags recordCount).eval DeMorgan.interpretation input index = true ↔ DeMorgan.Wiring.eval input (valid index) = true ∧ ((∃ (other : Fin (Sorting.networkRecords depth)), other ≠ index ∧ groups other = groups index ∧ DeMorgan.Wiring.eval input (valid other) = true ∧ (fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys other bit)) = fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys index bit)) ∨ ∃ (source : Fin sources), ((fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (sourceKeys source bit)) = fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys index bit)) ∧ DeMorgan.Wiring.eval input (sourceFlags source) = true)

Exact conflict semantics, with invalid slots and different candidates excluded.

theorem Algebraic.MassProduction.Nonuniform.PointConflicts.circuit_cost_le {depth groupWidth inputs keyWidth sources padding routingDepth : ℕ} (groups : Fin (Sorting.networkRecords depth) → 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 groups 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

The entire menu shares one occupancy scan and one duplicate-detection circuit.