Collision flags returned to their original records

Sort by a collision key, mark adjacent duplicates, and sort by a preserved identifier. Every original record returns to its literal input position, together with a flag reporting whether another original record has its key.

def Algebraic.MassProduction.Nonuniform.MarkDuplicates.flag {recordWidth : ℕ} (record : Fin (1 + recordWidth) → Bool) : Bool

Duplicate flag prepended to a marked record.

Equations

• Algebraic.MassProduction.Nonuniform.MarkDuplicates.flag record = record (Fin.castAdd recordWidth 0)

def Algebraic.MassProduction.Nonuniform.MarkDuplicates.body {recordWidth : ℕ} (record : Fin (1 + recordWidth) → Bool) : Fin recordWidth → Bool

Original bits carried by a marked record.

Equations

• Algebraic.MassProduction.Nonuniform.MarkDuplicates.body record bit = record (Fin.natAdd 1 bit)

def Algebraic.MassProduction.Nonuniform.MarkDuplicates.flagsArrayCircuit {recordWidth keyWidth : ℕ} (depth : ℕ) (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) : Circuit DeMorgan.signature (Sorting.networkRecords depth * recordWidth) (Sorting.networkRecords depth * 1)

Regard one Boolean duplicate flag per record as a width-one array.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.MarkDuplicates.flagsArrayCircuit_size {recordWidth keyWidth : ℕ} (depth : ℕ) (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) : (flagsArrayCircuit depth keyCircuit).size = (AdjacentDuplicates.circuit depth keyCircuit).size

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

def Algebraic.MassProduction.Nonuniform.MarkDuplicates.markCircuit {recordWidth keyWidth : ℕ} (depth : ℕ) (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) : Circuit DeMorgan.signature (Sorting.networkRecords depth * recordWidth) (Sorting.networkRecords depth * (1 + recordWidth))

Attach the global duplicate flags to complete original records.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.MarkDuplicates.markCircuit_size {recordWidth keyWidth : ℕ} (depth : ℕ) (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) : (markCircuit depth keyCircuit).size = (RecordArray.combine (flagsArrayCircuit depth keyCircuit) (Circuit.id DeMorgan.signature (Sorting.networkRecords depth * recordWidth))).size

markCircuit has exactly the gates of RecordArray.combine; the surrounding wiring adds none.

theorem Algebraic.MassProduction.Nonuniform.MarkDuplicates.markCircuit_eval_record {recordWidth keyWidth depth : ℕ} (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) (input : Fin (Sorting.networkBits depth recordWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : Sorting.flatRecords ((markCircuit depth keyCircuit).eval DeMorgan.interpretation input) record = Fin.append (fun (x : Fin 1) => (AdjacentDuplicates.circuit depth keyCircuit).eval DeMorgan.interpretation input record) (Sorting.flatRecords input record)

Marking adds one flag and preserves every original bit.

@[simp]

theorem Algebraic.MassProduction.Nonuniform.MarkDuplicates.markCircuit_body {recordWidth keyWidth depth : ℕ} (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) (input : Fin (Sorting.networkBits depth recordWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : body (Sorting.flatRecords ((markCircuit depth keyCircuit).eval DeMorgan.interpretation input) record) = Sorting.flatRecords input record

@[simp]

theorem Algebraic.MassProduction.Nonuniform.MarkDuplicates.markCircuit_flag {recordWidth keyWidth depth : ℕ} (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) (input : Fin (Sorting.networkBits depth recordWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : flag (Sorting.flatRecords ((markCircuit depth keyCircuit).eval DeMorgan.interpretation input) record) = (AdjacentDuplicates.circuit depth keyCircuit).eval DeMorgan.interpretation input record

def Algebraic.MassProduction.Nonuniform.MarkDuplicates.circuit {recordWidth keyWidth identifierWidth : ℕ} (depth : ℕ) (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) (identifierCircuit : Circuit DeMorgan.signature recordWidth identifierWidth) : Circuit DeMorgan.signature (Sorting.networkRecords depth * recordWidth) (Sorting.networkRecords depth * (1 + recordWidth))

The complete sort-mark-restore circuit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.MarkDuplicates.circuit_size {recordWidth keyWidth identifierWidth : ℕ} (depth : ℕ) (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) (identifierCircuit : Circuit DeMorgan.signature recordWidth identifierWidth) : (circuit depth keyCircuit identifierCircuit).size = (KeyedSort.circuit depth true keyCircuit).size + ((markCircuit depth keyCircuit).size + (KeyedSort.circuit depth true (identifierCircuit.mapInputs (Fin.natAdd 1))).size)

The exact gate count of circuit.

theorem Algebraic.MassProduction.Nonuniform.MarkDuplicates.circuit_correct {recordWidth keyWidth identifierWidth depth : ℕ} (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) (identifierCircuit : Circuit DeMorgan.signature recordWidth identifierWidth) (input : Fin (Sorting.networkBits depth recordWidth) → Bool) (identifiersOrdered : StrictMono fun (index : Fin (Sorting.networkRecords depth)) => toLex (identifierCircuit.eval DeMorgan.interpretation (Sorting.flatRecords input index))) (index : Fin (Sorting.networkRecords depth)) : body (Sorting.flatRecords ((circuit depth keyCircuit identifierCircuit).eval DeMorgan.interpretation input) index) = Sorting.flatRecords input index ∧ (flag (Sorting.flatRecords ((circuit depth keyCircuit identifierCircuit).eval DeMorgan.interpretation input) index) = true ↔ ∃ (other : Fin (Sorting.networkRecords depth)), other ≠ index ∧ keyCircuit.eval DeMorgan.interpretation (Sorting.flatRecords input other) = keyCircuit.eval DeMorgan.interpretation (Sorting.flatRecords input index))

Distinct increasing input identifiers restore both the original records and their exact duplicate flags to fixed output positions.

theorem Algebraic.MassProduction.Nonuniform.MarkDuplicates.circuit_cost_le {recordWidth keyWidth identifierWidth depth : ℕ} (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) (identifierCircuit : Circuit DeMorgan.signature recordWidth identifierWidth) : (circuit depth keyCircuit identifierCircuit).cost DeMorgan.standardCost ≤ Sorting.networkRecords depth * keyCircuit.cost DeMorgan.standardCost + depth * depth * Sorting.networkRecords depth * (2 * (keyWidth + recordWidth) * (2 * (keyWidth * (6 * keyWidth + 4)) + 4)) + (Sorting.networkRecords depth * (keyCircuit.cost DeMorgan.standardCost + 12 * keyWidth + 1) + (Sorting.networkRecords depth * identifierCircuit.cost DeMorgan.standardCost + depth * depth * Sorting.networkRecords depth * (2 * (identifierWidth + (1 + recordWidth)) * (2 * (identifierWidth * (6 * identifierWidth + 4)) + 4))))

Sorting and marking costs are additive, with linear record-count dependence throughout all three stages.