Size bounds for the Chan–He selectors, including their default

Bounding the modulus does not require either filter to succeed: a failed filter returns one. These bounds therefore apply to native execution with arbitrary nonnegative collision thresholds, including empty input sets. They do not assert the collision-shrinking property of a successful search.

Main results

• minOrOne_filter_bounds: a positive bounded candidate set keeps its filtered selector bounded.
• modulus_bounds_of_candidates: both selections, including defaults, have product in [1,m²].

The bounds are original elementary consequences of the existing finite selectors.

theorem Cslib.Algorithms.ThreeSum.ChanHe.minOrOne_filter_bounds {Q : Finset ℕ} {m : ℕ} (hm : 1 ≤ m) (hpos : ∀ q ∈ Q, 1 ≤ q) (hle : ∀ q ∈ Q, q ≤ m) (A : ℕ → Prop) [DecidablePred A] : 1 ≤ minOrOne ({q ∈ Q | A q}) ∧ minOrOne ({q ∈ Q | A q}) ≤ m

Filtering positive candidates bounded by m keeps the default-one selector in [1,m]. The candidate set and the filtered set may both be empty.

theorem Cslib.Algorithms.ThreeSum.ChanHe.modulus_bounds_of_candidates {Q : Finset ℕ} {m : ℕ} (hm : 1 ≤ m) (hpos : ∀ q ∈ Q, 1 ≤ q) (hle : ∀ q ∈ Q, q ≤ m) (Λ : ℕ) (S₁ S₂ S₃ : Finset ℤ) : 1 ≤ modulus Q Λ S₁ S₂ S₃ ∧ modulus Q Λ S₁ S₂ S₃ ≤ m ^ 2

Positive bounded candidates bound the modulus regardless of whether either filter succeeds. This is a size bound only; no magnitude or successful-search premise is needed.