Finding and selecting a colliding pair

After sorting, two different records with equal keys force an adjacent pair of different records with that key, even when complete records repeat (adjacent_distinct_collision). A linear scan then retains the last flagged record (chooseRecord), at four gates per record bit (synthesis_chooseRecord). The scan works with any number of flagged records and avoids an all-pairs priority test.

Main definitions

• Cslib.Circuits.Boolean.Iteration.chooseRecord: the last flagged record, or a fallback.

Main results

• Cslib.Circuits.Boolean.Iteration.adjacent_distinct_collision: sorting makes a collision between different records adjacent.
• Cslib.Circuits.Boolean.Iteration.chooseRecord_spec: a flagged record is selected if any.
• Cslib.Circuits.Boolean.Iteration.synthesis_chooseRecord: the cost of the scan.
• Cslib.Circuits.Boolean.Iteration.synthesis_flaggedRecords: construct and select records, sharing each flag across the output bits.

References

• Adapted from lean/Proofs/{Collisions,Selection}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

Adjacent collisions

theorem Cslib.Circuits.Boolean.Iteration.adjacent_distinct_of_equal_keys {α : Type u} {R : ℕ} {β : Type v} [LinearOrder β] (records : Fin R → α) (key : α → β) (hs : Monotone (key ∘ records)) (i j : Fin R) (hij : i < j) (hne : records i ≠ records j) (heq : key (records i) = key (records j)) : ∃ (p : ℕ) (hp : p + 1 < R), records ⟨p, ⋯⟩ ≠ records ⟨p + 1, hp⟩ ∧ key (records ⟨p, ⋯⟩) = key (records ⟨p + 1, hp⟩) ∧ key (records ⟨p, ⋯⟩) = key (records i)

In an array with monotone keys, two different records with equal keys force an adjacent pair of different records with that key.

theorem Cslib.Circuits.Boolean.Iteration.adjacent_distinct_collision {α : Type u} {R : ℕ} {β : Type v} [LinearOrder β] (input output : Fin R → α) (key : α → β) (hperm : (List.ofFn output).Perm (List.ofFn input)) (hs : Monotone (key ∘ output)) (i j : Fin R) (hne : input i ≠ input j) (heq : key (input i) = key (input j)) : ∃ (p : ℕ) (hp : p + 1 < R), output ⟨p, ⋯⟩ ≠ output ⟨p + 1, hp⟩ ∧ key (output ⟨p, ⋯⟩) = key (output ⟨p + 1, hp⟩) ∧ key (output ⟨p, ⋯⟩) = key (input i)

A sorter preserving complete records makes some collision between different records adjacent, with the original key. Identical adjacent records can therefore be rejected safely.

Selecting a flagged record

def Cslib.Circuits.Boolean.Iteration.chooseRecord {α : Type u} {R : ℕ} (flags : Fin R → Bool) (records : Fin R → α) (fallback : α) : ℕ → α

The last flagged record among the first t positions, or the fallback if there is none.

theorem Cslib.Circuits.Boolean.Iteration.chooseRecord_map {α : Type u} {R : ℕ} {β : Type u_1} (g : α → β) (flags : Fin R → Bool) (records : Fin R → α) (fallback : α) (t : ℕ) : g (chooseRecord flags records fallback t) = chooseRecord flags (g ∘ records) (g fallback) t

Selection commutes with applying a function to every record.

theorem Cslib.Circuits.Boolean.Iteration.chooseRecord_of_forall_eq_false {α : Type u} {R : ℕ} (flags : Fin R → Bool) (records : Fin R → α) (fallback : α) (h : ∀ (j : Fin R), flags j = false) (t : ℕ) : chooseRecord flags records fallback t = fallback

If no record is flagged, the scan returns the fallback.

theorem Cslib.Circuits.Boolean.Iteration.chooseRecord_spec {α : Type u} {R : ℕ} (flags : Fin R → Bool) (records : Fin R → α) (fallback : α) (t : ℕ) (hex : ∃ (j : Fin R), ↑j < t ∧ flags j = true) : ∃ (j : Fin R), ↑j < t ∧ flags j = true ∧ chooseRecord flags records fallback t = records j

If some record among the first t is flagged, the scan returns a flagged record.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_chooseRecord {R n w : ℕ} (s : Set (BooleanFunction n)) (flags : BitString n → Fin R → Bool) (records : BitString n → Fin R → Fin w → Bool) (fallback : BitString n → Fin w → Bool) (hf : ∀ (j : Fin R), (fun (x : BitString n) => flags x j) ∈ s) (hr : ∀ (j : Fin R) (bit : Fin w), (fun (x : BitString n) => records x j bit) ∈ s) (hzero : ∀ (bit : Fin w), (fun (x : BitString n) => fallback x bit) ∈ s) : Synthesis interpretation s (Set.range fun (bit : Fin w) (x : Fin n → Bool) => chooseRecord (flags x) (records x) (fallback x) R bit) (R * (4 * w))

Selecting among available records costs four gates per record bit.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_flaggedRecords {R n w : ℕ} (s : Set (BooleanFunction n)) (flags : Fin R → (Fin n → Bool) → Bool) (records : Fin R → (Fin n → Bool) → Fin w → Bool) (K : ℕ) (hz : (fun (x : BitString n) => false) ∈ s) (hrows : ∀ (j : Fin R), Synthesis interpretation s ({flags j} ∪ Set.range fun (i : Fin w) (x : Fin n → Bool) => records j x i) K) : Synthesis interpretation s (Set.range fun (i : Fin w) (x : Fin n → Bool) => chooseRecord (fun (j : Fin R) => flags j x) (fun (j : Fin R) => records j x) (fun (x : Fin w) => false) R i) (R * (K + 4 * w))

Construct all flagged records and select one, sharing every flag across its output bits. The all-false fallback is an already available constant.