Duplicate flags with automatic ordering identifiers

Keys are supplied by wires or constants. The circuit adds unique increasing identifiers, sorts and marks equal keys, restores input order, and extracts one duplicate flag per key. No ordering premise is required from callers.

def Algebraic.MassProduction.Nonuniform.DuplicateFlags.keyCircuit (depth keyWidth : ℕ) : Circuit DeMorgan.signature (keyWidth + depth) keyWidth

Read the key prefix of an identified record.

Equations

• Algebraic.MassProduction.Nonuniform.DuplicateFlags.keyCircuit depth keyWidth = (Cslib.Circuits.Circuit.id Algebraic.DeMorgan.signature (keyWidth + depth)).mapOutputs (Fin.castAdd depth)

@[simp]

theorem Algebraic.MassProduction.Nonuniform.DuplicateFlags.keyCircuit_size (depth keyWidth : ℕ) : (keyCircuit depth keyWidth).size = 0

keyCircuit is pure wiring: it has no gates.

def Algebraic.MassProduction.Nonuniform.DuplicateFlags.identifierCircuit (depth keyWidth : ℕ) : Circuit DeMorgan.signature (keyWidth + depth) depth

Read the ordering identifier after the key.

Equations

• Algebraic.MassProduction.Nonuniform.DuplicateFlags.identifierCircuit depth keyWidth = (Cslib.Circuits.Circuit.id Algebraic.DeMorgan.signature (keyWidth + depth)).mapOutputs (Fin.natAdd keyWidth)

@[simp]

theorem Algebraic.MassProduction.Nonuniform.DuplicateFlags.identifierCircuit_size (depth keyWidth : ℕ) : (identifierCircuit depth keyWidth).size = 0

identifierCircuit is pure wiring: it has no gates.

noncomputable def Algebraic.MassProduction.Nonuniform.DuplicateFlags.layoutWiring {depth keyWidth inputs : ℕ} (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (output : Fin (Sorting.networkBits depth (keyWidth + depth))) : DeMorgan.Wiring inputs

Add the original record index as hardwired metadata.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.DuplicateFlags.layoutWiring_eval_record {depth keyWidth inputs : ℕ} (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (record : Fin (Sorting.networkRecords depth)) : Sorting.flatRecords (fun (bit : Fin (Sorting.networkBits depth (keyWidth + depth))) => DeMorgan.Wiring.eval input (layoutWiring keys bit)) record = Fin.append (fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys record bit)) (lexBitVectorAt (Fin.cast ⋯ record))

Each prepared record contains exactly its supplied key and fixed identifier.

noncomputable def Algebraic.MassProduction.Nonuniform.DuplicateFlags.circuit {depth keyWidth inputs : ℕ} (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) : Circuit DeMorgan.signature inputs (Sorting.networkRecords depth)

Concrete duplicate detection in original key order.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.DuplicateFlags.circuit_size {depth keyWidth inputs : ℕ} (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) : (circuit keys).size = (DeMorgan.Wiring.circuit (layoutWiring keys)).size + (MarkDuplicates.circuit depth (keyCircuit depth keyWidth) (identifierCircuit depth keyWidth)).size

The exact gate count of circuit.

theorem Algebraic.MassProduction.Nonuniform.DuplicateFlags.circuit_eval_iff {depth keyWidth inputs : ℕ} (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (record : Fin (Sorting.networkRecords depth)) : (circuit keys).eval DeMorgan.interpretation input record = true ↔ ∃ (other : Fin (Sorting.networkRecords depth)), other ≠ record ∧ (fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys other bit)) = fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys record bit)

A flag is true precisely when a distinct input record has the same key.

theorem Algebraic.MassProduction.Nonuniform.DuplicateFlags.circuit_cost_le {depth keyWidth inputs : ℕ} (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) : (circuit keys).cost DeMorgan.standardCost ≤ 256 * Sorting.networkRecords depth * (depth + keyWidth + 1) ^ 5

Sorting and scanning remain linear in the number of keys.