Exact duplicate detection by adjacent comparisons

In a sorted sequence, a record has another equal key exactly when it has an equal-key predecessor or successor. Computing keys once and comparing each adjacent pair gives a concrete linear-size duplicate detector.

theorem Algebraic.MassProduction.Nonuniform.AdjacentDuplicates.neighbor_iff {count : ℕ} {Key : Type u_1} [LinearOrder Key] (key : Fin count → Key) (ordered : Monotone key) (index : Fin count) : ((∃ (positive : 0 < ↑index), key ⟨↑index - 1, ⋯⟩ = key index) ∨ ∃ (fits : ↑index + 1 < count), key ⟨↑index + 1, fits⟩ = key index) ↔ ∃ (other : Fin count), other ≠ index ∧ key other = key index

Every duplicate in a sorted sequence has an adjacent witness.

def Algebraic.MassProduction.Nonuniform.AdjacentDuplicates.equalExpression (depth keyWidth : ℕ) (left right : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression (Sorting.networkBits depth keyWidth)

Equality of two keys in a flat key array.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.AdjacentDuplicates.equalExpression_eval_iff {depth keyWidth : ℕ} (input : Fin (Sorting.networkBits depth keyWidth) → Bool) (left right : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression.eval input (equalExpression depth keyWidth left right) = true ↔ Sorting.flatRecords input left = Sorting.flatRecords input right

Key equality is tested exactly.

theorem Algebraic.MassProduction.Nonuniform.AdjacentDuplicates.equalExpression_cost {depth keyWidth : ℕ} (left right : Fin (Sorting.networkRecords depth)) : (equalExpression depth keyWidth left right).standardCost = 6 * keyWidth

One adjacent-key equality uses six charged gates per key bit.

def Algebraic.MassProduction.Nonuniform.AdjacentDuplicates.expression (depth keyWidth : ℕ) (index : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression (Sorting.networkBits depth keyWidth)

Missing neighbors contribute false; existing neighbors are compared.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.AdjacentDuplicates.expression_eval_iff {depth keyWidth : ℕ} (input : Fin (Sorting.networkBits depth keyWidth) → Bool) (index : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression.eval input (expression depth keyWidth index) = true ↔ (∃ (positive : 0 < ↑index), Sorting.flatRecords input ⟨↑index - 1, ⋯⟩ = Sorting.flatRecords input index) ∨ ∃ (fits : ↑index + 1 < Sorting.networkRecords depth), Sorting.flatRecords input ⟨↑index + 1, fits⟩ = Sorting.flatRecords input index

The local circuit tests precisely the two possible adjacent witnesses.

def Algebraic.MassProduction.Nonuniform.AdjacentDuplicates.flagsCircuit (depth keyWidth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits depth keyWidth) (Sorting.networkRecords depth)

Duplicate flags from an already-computed array of keys.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.AdjacentDuplicates.flagsCircuit_size (depth keyWidth : ℕ) : (flagsCircuit depth keyWidth).size = ∑ record : Fin (Sorting.networkRecords depth), (expression depth keyWidth record).gateCount

The exact gate count of flagsCircuit.

theorem Algebraic.MassProduction.Nonuniform.AdjacentDuplicates.flagsCircuit_eval_iff {depth keyWidth : ℕ} (input : Fin (Sorting.networkBits depth keyWidth) → Bool) (ordered : Monotone fun (record : Fin (Sorting.networkRecords depth)) => toLex (Sorting.flatRecords input record)) (index : Fin (Sorting.networkRecords depth)) : (flagsCircuit depth keyWidth).eval DeMorgan.interpretation input index = true ↔ ∃ (other : Fin (Sorting.networkRecords depth)), other ≠ index ∧ Sorting.flatRecords input other = Sorting.flatRecords input index

Sorted key arrays yield exact global duplicate flags.

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

Compute each key once for subsequent adjacent comparisons.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.AdjacentDuplicates.keysCircuit_size {recordWidth keyWidth : ℕ} (depth : ℕ) (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) : (keysCircuit depth keyCircuit).size = Sorting.networkRecords depth * keyCircuit.size

Computing the keys costs exactly one key evaluation per record.

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

The key array contains the computed key of each original record.

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

Complete duplicate detector, including key computation.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.AdjacentDuplicates.circuit_size {recordWidth keyWidth : ℕ} (depth : ℕ) (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) : (circuit depth keyCircuit).size = (keysCircuit depth keyCircuit).size + (flagsCircuit depth keyWidth).size

The detector has exactly the gates of its key computation followed by its local comparisons.

theorem Algebraic.MassProduction.Nonuniform.AdjacentDuplicates.circuit_eval_iff {recordWidth keyWidth depth : ℕ} (keyCircuit : Circuit DeMorgan.signature recordWidth keyWidth) (input : Fin (Sorting.networkBits depth recordWidth) → Bool) (ordered : Monotone fun (record : Fin (Sorting.networkRecords depth)) => toLex (keyCircuit.eval DeMorgan.interpretation (Sorting.flatRecords input record))) (index : Fin (Sorting.networkRecords depth)) : (circuit depth keyCircuit).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)

Exact global duplicate detection whenever the computed keys are sorted.

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

Linear record-count cost, including the two local comparisons.