Import bannai-bannai-stanton: bound on distance sets

[Vilin97]

Vendors AntoineduFresne/Bannai-Bannai-Stanton_Theorem (Apache-2.0).

What it proves

The Bannai-Bannai-Stanton theorem: a distance set S in Euclidean space ℝ^d that realizes s distinct distances has size at most Nat.choose (d + s) s (BannaiBannaiStanton.bannai_bannai_stanton_bound : S.encard ≤ Nat.choose (d + s) s). The proof follows the short polynomial-method argument of Petrov and Pohoata via a generalized Croot-Lev-Pach rank lemma, with auxiliary results on diagonal linear-independence of polynomials, monomial counting of bounded degree, and a rank bound for sums of matrices.

Import notes

• Single 1030-line upstream file, already on the pool toolchain (v4.32.0-rc1), builds warning-free against Mathlib with no API changes needed.
• Wrapped all declarations in a BannaiBannaiStanton namespace (upstream used root-level sections — a whole-pool collision risk; dim, distances etc. would clash). Renamed the one Set.distances extension to distanceSet and a handful of underscored defs to camelCase to satisfy the naming linter; theorem statements are preserved verbatim.
• Sorry-free; #print axioms bannai_bannai_stanton_bound = {propext, Classical.choice, Quot.sound}.

All local gates pass: warning-free lake build, mk_all --check, runLinter, lint-style, and the quality checker.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

[github-actions]

Proof profile (new / modified Lean files)

lake build LeanPool wall time: 27.94 s (= 0.47 min) — user 28.75 s, sys 6.36 s.

This is the parallel build wall clock and is the compile-time answer for this PR. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 118 maxHeartbeats units across 2 files (1,055 added LOC).

Sum of lean --profile: 19018.8 ms (= 19.02 s). Import-excluded time: 16138.8 ms (= 16.14 s).

Count-heartbeats wall-clock total: 8.64 s. Repeated import cost inside lean --profile: 2880.0 ms (= 2.88 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Decls	Errors
LeanPool/BannaiBannaiStanton/BoundOnDistanceSet.lean	1,038	118	6.34	17.38	15.93	1.45	30	0
LeanPool/BannaiBannaiStanton.lean	17	0	2.30	1.63	0.20	1.43	0	0
Total	1,055	118	8.64	19.02	16.14	2.88	30	0

Aggregate phase totals

Phase	Time
typeclass inference	7540.0 ms (= 7.54 s)
import	2880.0 ms (= 2.88 s)
tactic execution	2480.0 ms (= 2.48 s)
simp	2360.0 ms (= 2.36 s)
interpretation	1741.0 ms (= 1.74 s)
type checking	675.0 ms (= 0.68 s)
elaboration	356.2 ms (= 0.36 s)
tacticAnalysis	184.4 ms (= 0.18 s)
linting	130.3 ms (= 0.13 s)
ring	110.0 ms (= 0.11 s)
process pre-definitions	96.3 ms (= 0.10 s)
share common exprs	85.7 ms (= 0.09 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.BannaiBannaiStanton.BoundOnDistanceSet	9.70 s
LeanPool.BannaiBannaiStanton	1.60 s

Per-file `lean --profile` output

LeanPool/BannaiBannaiStanton.lean

import took 1.43s
cumulative profiling times:
	elaboration 0.18ms
	import 1.43s
	initialization 30.7ms
	interpretation 171ms
	linting 0.267ms
	module linting 0.00105ms
	overlappingInstancesLinter 0.193ms
	parsing 0.0571ms
	tacticAnalysis 1.45ms
real 2.36
user 1.30
sys 0.99

LeanPool/BannaiBannaiStanton/BoundOnDistanceSet.lean

import took 1.45s
simp took 131ms
simp took 138ms
typeclass inference of Nonempty took 161ms
typeclass inference of Nonempty took 163ms
typeclass inference of Nonempty took 162ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 109ms
simp took 201ms
typeclass inference of Nonempty took 161ms
simp took 133ms
cumulative profiling times:
	attribute application 0.782ms
	compilation (IR) 0.232ms
	compilation (LCNF base) 2.56ms
	compilation (LCNF impure) 1.19ms
	compilation (LCNF mono) 2.11ms
	congr simp thm 59.8ms
	dsimp 11.2ms
	elaboration 356ms
	fix level params 19.3ms
	import 1.45s
	initialization 37.6ms
	instantiate metavars 44.7ms
	interpretation 1.57s
	let-to-have transformation 56ms
	linting 130ms
	module linting 0.00108ms
	norm_num 14.2ms
	overlappingInstancesLinter 33.4ms
	parsing 65.9ms
	process pre-definitions 96.3ms
	ring 110ms
	share common exprs 85.7ms
	simp 2.36s
	tactic execution 2.48s
	tacticAnalysis 183ms
	type checking 675ms
	typeclass inference 7.54s
real 6.52
user 16.74
sys 1.11

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[github-actions]

🤖 LLM review (gpt-5.5)

Reviewed head: 26f741e1a895a4ed38d407c9ae41db7e37e68632

Verdict: 🛑 request_changes

This PR formalizes the Bannai-Bannai-Stanton bound for finite-distance subsets of Euclidean space, developing the polynomial-method setup, bounded-degree monomial counting, a Croot-Lev-Pach-style inertia/rank lemma, and the final bound S.encard ≤ Nat.choose (d + s) s. The mathematical target is a named research-level theorem and the formalization is self-contained enough to be worth merging, but the project card/source metadata currently cite only the author’s GitHub repository rather than a mathematical source for the theorem/proof.

Aspect	Value
Fit	✅ good_fit
Level	research
Branch	discrete geometry
Mode	theory_building
Obscure problem	no
Code quality	3 / 5

The contribution is a completed formalization of the Bannai-Bannai-Stanton polynomial-method bound on the size of Euclidean distance sets.

Findings (1)

• source-anchor — LeanPool/BannaiBannaiStanton.lean:11
  The project card lists the source as the formalization GitHub repository; add a mathematical citation for the Bannai-Bannai-Stanton theorem and/or the Petrov-Pohoata proof being followed, preferably with title, authors, and publication/arXiv data. The GitHub repo can remain as provenance, but it should not be the only source anchor.

---

Tokens: 19,979 in / 1,906 out · Tier: flex · Cost: $0.0785
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.