Duplicate flags with shared comparisons and saved swaps

A sorted array has a repeated key at a position exactly when that key equals a neighbor. adjacentDuplicateCircuit computes each adjacent equality once and shares it between the neighbors. It adds one OR gate per record; the last record reuses the first equality output, which is false, for its missing successor. The empty array uses no gates.

duplicateFlagsCircuit accepts an arbitrary array of 2 ^ d records. It sorts by selected key coordinates, computes the flags, then reverses the saved swaps on the flags alone. Outputs refer to the original positions, including when complete records repeat. No record identifiers or second sort are needed. Header and payload bits can be retained by free input wiring.

Costs include constants and negations. Gate counts do not certify construction runtime.

Main definitions

• Cslib.Circuits.Boolean.adjacentDuplicateCircuit: share adjacent-key equality tests.
• Cslib.Circuits.Boolean.duplicateFlagsCircuit: duplicate flags in original input order.

Main results

• Cslib.Circuits.Boolean.eval_adjacentDuplicateCircuit_iff: exact detection on sorted keys.
• Cslib.Circuits.Boolean.eval_duplicateFlagsCircuit_iff: exact detection on arbitrary inputs.
• Cslib.Circuits.Boolean.cost_program_duplicateFlagsCircuit: exact weighted gate cost.
• Cslib.Circuits.Boolean.size_duplicateFlagsCircuit: exact total gate count.

References

Simplifies MassProduction/Nonuniform/AdjacentDuplicates.lean and the conflict-detection construction in S. Schlesinger, Boolean circuit mass production formalization, using the saved decisions of K. E. Batcher, Sorting Networks and Their Applications.

def Cslib.Circuits.Boolean.adjacentDuplicateCircuit {input count k : ℕ} (key : Fin count → Fin k → Fin input) : Circuit signature input count

Test both neighbors, sharing each adjacent equality once.

theorem Cslib.Circuits.Boolean.eval_adjacentDuplicateCircuit_iff {input count k : ℕ} (key : Fin count → Fin k → Fin input) (x : BitString input) (ordered : Monotone fun (i : Fin count) => toLex (x ∘ key i)) (i : Fin count) : (adjacentDuplicateCircuit key).eval interpretation x i = true ↔ ∃ (j : Fin count), j ≠ i ∧ x ∘ key j = x ∘ key i

On sorted keys, adjacent equality detects every repeated key.

theorem Cslib.Circuits.Boolean.cost_program_adjacentDuplicateCircuit {input count k : ℕ} (key : Fin count → Fin k → Fin input) (cost : signature.Op → ℕ) : (adjacentDuplicateCircuit key).program.cost cost = (adjacentEqualityCircuit key).program.cost cost + count * cost Op.or

Sharing the equality outputs adds exactly one OR gate per record.

def Cslib.Circuits.Boolean.duplicateFlagsCircuit.rows (count : ℕ) : Circuit signature count (count * 1)

Regard a vector of flags as an array of one-bit records.

def Cslib.Circuits.Boolean.duplicateFlagsCircuit.outputs (count : ℕ) : Circuit signature (count * 1) count

Select the flag from each one-bit record.

def Cslib.Circuits.Boolean.duplicateFlagsCircuit {r k : ℕ} (key : Fin k → Fin r) (d : ℕ) : Circuit signature (BitonicSort.arity d * r) (BitonicSort.arity d)

Sort once, flag repeated selected keys, and return flags to original positions.

theorem Cslib.Circuits.Boolean.eval_duplicateFlagsCircuit_iff {r k : ℕ} (key : Fin k → Fin r) (d : ℕ) (x : BitString (BitonicSort.arity d * r)) (i : Fin (BitonicSort.arity d)) : (duplicateFlagsCircuit key d).eval interpretation x i = true ↔ ∃ (j : Fin (BitonicSort.arity d)), j ≠ i ∧ directProductInput x j ∘ key = directProductInput x i ∘ key

A flag is true exactly when another original record has the same selected key.

theorem Cslib.Circuits.Boolean.cost_program_duplicateFlagsCircuit {r k : ℕ} (key : Fin k → Fin r) (d : ℕ) (cost : signature.Op → ℕ) : (duplicateFlagsCircuit key d).program.cost cost = (bitonicSortTraceCircuit key d true).program.cost cost + (adjacentEqualityCircuit fun (row : Fin (BitonicSort.arity d)) (bit : Fin k) => finProdFinEquiv (row, key bit)).program.cost cost + BitonicSort.arity d * cost Op.or + BitonicSort.sortTraceSize d * (2 * (2 * cost Op.and + cost Op.or))

Exact weighted cost of one sort, shared adjacent tests, OR gates, and flag restoration.

theorem Cslib.Circuits.Boolean.size_duplicateFlagsCircuit {r k : ℕ} (key : Fin k → Fin r) (d : ℕ) : (duplicateFlagsCircuit key d).size = BitonicSort.sortTraceSize d * (6 * k + 6 * r + 8) + (1 + (BitonicSort.arity d - 1) * (6 * k + 1)) + BitonicSort.arity d

Exact total gate count, including empty keys and zero-width records.