refactor(QueryTracking/Birthday): extract pair-count lemma to ToMathlib

[BoltonBailey]

This PR refactors a result in the birthday file. It reduces the quantity of code in that file by refactoring out a the fact that the number of pairs of type Fin n such that p.1 < p.2 is n.choose 2 to another file.

🤖 Generated with Claude Code

[github-actions]

🤖 PR Summary

Formalization and Lemma Extraction

• Adds ToMathlib/Combinatorics/FinPairs.lean providing results for counting strictly increasing pairs (i, j) in Fin n where i < j.
• Finset.card_filter_fst_lt_snd_eq_sum_range: Relates pair cardinality to the Gauss sum $\sum_{k &lt; n} k$.
• Finset.card_filter_fst_lt_snd: Establishes the cardinality as n.choose 2.

Proof Completion

• Fills the final sorry in probEvent_logCollision_le_birthday_total_tight, completing the ROM birthday-bound formalization.
• The log-collision bound is now a fully verified tight result ($\binom{n}{2} / |C|$), allowing the standard $n^2 / (2|C|)$ bound to be derived rigorously.

Refactoring

• Replaces an ~80-line inline induction in the birthday-bound proof with calls to the extracted combinatorial lemmas.

---

Statistics

Metric	Count
📝 Files Changed	3
✅ Lines Added	145
❌ Lines Removed	95

---

Lean Declarations

✏️ **Added:** 4 declaration(s)

• theorem card_filter_fst_lt_snd (n : ℕ) : in ToMathlib/Combinatorics/FinPairs.lean
• theorem probEvent_logCollision_le_birthday_total {α : Type} in VCVio/OracleComp/QueryTracking/Birthday.lean
• theorem card_filter_fst_lt_snd_eq_sum_range (m : ℕ) : in ToMathlib/Combinatorics/FinPairs.lean
• theorem probEvent_logCollision_le_birthday_total_tight {α : Type} in VCVio/OracleComp/QueryTracking/Birthday.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Attribution and File Headers * Header Year: In ToMathlib/Combinatorics/FinPairs.lean, the copyright year is set to 2026. Verify if this should be the current calendar year. * Prologue Layout: There is no blank line between the header and the code in FinPairs.lean. Additionally, the stray word 'module' on line 7 is a syntax error and violates the layout rules. ### Documentation Expectations * Section Headers: FinPairs.lean uses '@[expose] public section' (line 21). Project instructions require using '/-! ## Section title -/' for inline section breaks. Note that 'public section' and '@[expose]' are not standard Lean 4 syntax. ### Style Notes * Syntax Errors: The keyword 'module' on line 7 of FinPairs.lean must be removed. * Imports: FinPairs.lean uses 'public import'. Ordinary source files should use standard 'import' unless re-exporting is explicitly required by the architecture. * Naming: The new theorem 'probEvent_logCollision_le_birthday_total_tight' in Birthday.lean uses mixed lowerCamelCase and snake_case. While it follows existing naming in that file, Mathlib convention for theorems is pure snake_case. * TODOs: A '-- TODO' comment remains on line 32 of FinPairs.lean regarding proof simplification. Ensure this is resolved or intentionally preserved.

---

📄 **Per-File Summaries**

• ToMathlib.lean: This change updates the ToMathlib.lean central module by adding an import for ToMathlib.Combinatorics.FinPairs. This modification exposes additional combinatorial definitions and theorems related to finite pairs to the project's local mathlib extension library.
• ToMathlib/Combinatorics/FinPairs.lean: This file introduces new theorems counting strictly increasing pairs in Fin n × Fin n, specifically proving that their cardinality equals the binomial coefficient n.choose 2. It includes two main results that equate this count to both a Gauss sum and a binomial coefficient using induction and Finset manipulations.
• VCVio/OracleComp/QueryTracking/Birthday.lean: This update introduces a tighter birthday bound theorem (probEvent_logCollision_le_birthday_total_tight) based on the exact number of unordered query pairs and refactors the existing $n^2/2|C|$ bound as a corollary. The proof is significantly simplified by leveraging new combinatorial lemmas from the FinPairs import, replacing a manual inductive proof for counting pairs.

---

Last updated: 2026-05-31 16:01 UTC.