Formalize the geometric 3-chain support theorem for planar point sets

[lyfar]

This adds LeanPool/Erdos132ThreeChain: a self-contained, unconditional
formalization about finite planar point sets whose non-diameter squared
distances are confined to a geometric progression of ratio three.

Main declaration. Erdos132ThreeChain.nonDiameterSqDists_ne_chain — for
n ≥ 13 and a > 0, a set of n points of the plane with squared diameter
D never has its set of non-diameter squared distances equal to the geometric
3-chain {a · 3^j : j < h}, for any chain length h.

threeChain_support_empty is the thin 2 ≤ h wrapper, kept so that a
statement matching the informal phrasing "a 3-chain of length at least two" is
available directly. Its _hh argument is unused, which is exactly why the
unbounded form is the main declaration.

Two theorems carry it:

Chain-quadruple theorem. four_chain_adjacent — if the six pairwise
squared distances of four plane points all equal a · 3^j for varying j ∈ ℕ
and fixed a > 0, then they all lie in a single adjacent pair {r, 3r} of the
chain, with r itself in the chain. pair_classification refines this to the
seven labelled patterns of the inductive ChainPattern.

Five-point obstruction. no_five_chain_finset — no five-element planar set
has all ten of its pairwise squared distances inside such a chain.

The lift from five points to n ≥ 13 is exists_independent_five, the Caro–Wei
bound specialized to a degree-sum hypothesis. That hypothesis is the
Hopf–Pannwitz edge bound, which hopfPannwitz supplies. Hopf–Pannwitz is not
claimed as new here: the same bound is already in the pool as
LeanPool.Erdos132N14.diameterEdges_card_le, and this project reproves it in its
own model only because pool projects do not import one another. It is a
supporting lemma, and it is not listed among the card's main results. The
overlap is set out with both statements verbatim under Prior art.

Provenance and scope

• There is no prior write-up behind the 3-chain statement. It was produced by
  the author's automated research pipeline in August 2026.
• The cited source is the ambient Erdős problem page. It poses the problem and
  states nothing about geometric 3-chains. This PR does not resolve that
  problem: its distance spectra need not be geometric 3-chains.
• The descriptive labels in the Lean docstrings — "chain-quadruple theorem",
  "five-point obstruction" — are internal names for results of this development.
  They do not refer to a numbered result anywhere else. The earlier draft of
  this PR used "Theorem 4" / "Theorem 5" and spoke of "the source's" determinant
  and counts; that numbering was internal and the phrasing was wrong, and both
  are gone.
• Hopf–Pannwitz and Caro–Wei are classical statements. Caro–Wei has no Lean
  version in Mathlib or the pool, so it is proved here. Hopf–Pannwitz does have
  one in the pool, and the copy here is a self-containment lemma, not a claim
  (see Prior art).
• Lean proofs are AI-written (provenance: AI).

Prior art

Commands were run against the pinned Mathlib
(.lake/packages/mathlib/Mathlib, v4.34.0-rc1) and against LeanPool/, with
grep -rEil <pattern>. Counts are files matched.

pattern	Mathlib	pool
caro.?wei	0	0 (outside this project)
hopf.?pannwitz|pannwitz	0	LeanPool/Erdos132N14/{HopfPannwitz,HopfPannwitzGeometry,DiameterDescent,Main,PublishedInputs}.lean
diameter.?graph, diameterEdges	0	LeanPool/Erdos132N14/HopfPannwitz.lean
few.?distance, two.?distance.?set, three.?distance.?set	0	LeanPool/Erdos132N14/PublishedInputs.lean (multiplicity inputs, not a distance-set classification)
cayley.?menger	0	LeanPool/DistanceGeometry/CayleyMengerVolume.lean, LeanPool/Erdos97ConvexOctagon/CayleyMenger.lean
schoenberg	0	LeanPool/DistanceGeometry/Schoenberg.lean
geometric.?progression.*distance, distanceSet, distanceSpectrum	0	0
independenceNumber|indepNum	Mathlib/Combinatorics/SimpleGraph/Clique.lean	0
isTuranMaximal	Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean	0

What the hits are, declaration by declaration:

• hopfPannwitz duplicates LeanPool.Erdos132N14.diameterEdges_card_le, and
  is not claimed as new. The two statements, verbatim:

  -- LeanPool/Erdos132N14/HopfPannwitz.lean
  theorem diameterEdges_card_le
      (P : Configuration ι) (S : Finset ι) {d : ℝ}
      (hd : 0 < d)
      (hmax : ∀ f ∈ pairs S, P.pairDistance f ≤ d) :
      (diameterEdges P S d).card ≤ S.card
  
  -- LeanPool/Erdos132ThreeChain/HopfPannwitz.lean
  theorem hopfPannwitz {X : Finset Point} {D : ℝ} (hD : IsSqDiameter X D) :
      ∑ v ∈ X, degree (DiameterAdj D) X v ≤ 2 * X.card

  Same mathematical content — a positive maximal distance is realised at most as
  often as there are points. The existing one is stated for a Configuration ι
  (an injective map from a LinearOrder index type into ℂ) and bounds the
  cardinality of a Finset of unordered pairs, proved by Perles charging. The
  version here works over a Finset (ℝ × ℝ), in squared distances, in handshake
  form, by pendant-deletion induction driven by Cramer's rule. Neither statement
  is an instance of the other without a model bridge (a LinearOrder on
  ℝ × ℝ, a dist-to-sqDist transfer, and a handshake lemma). It is reproved
  rather than imported because no project in the pool imports another —
  CONTRIBUTING.md states the projects are independent, and a check of every
  import LeanPool.* line in LeanPool/ finds zero cross-project imports today.
  It is a supporting lemma of this development and is deliberately absent from
  the card's main_results.

• Erdos97ConvexOctagon.cm4_sqDist_eq_zero is the same four-point
  Cayley–Menger vanishing as Erdos132ThreeChain.gramDet_eq_zero, over
  EuclideanSpace ℝ (Fin 2) rather than ℝ × ℝ. Both are one-line ring
  identities; the same independence reason applies.

• DistanceGeometry.schoenberg characterizes Euclidean distance matrices in
  general dimension. This project never invokes Schoenberg: the four-point
  condition is used directly as a ring identity, and the five-point
  obstruction is a sum-of-squares contradiction.

• SimpleGraph.indepNum is a definition plus complement lemmas; it carries
  no lower bound, so it cannot supply Caro–Wei. isTuranMaximal is the
  extremal-graph characterization, not an independence-number bound.

• No Mathlib match was found for the remaining headline notions
  (nonDiameterSqDists_ne_chain, four_chain_adjacent, pair_classification,
  no_four_on_circle, carowei, exists_independent_five,
  chainTwo_nonDiameter_support). The patterns searched are the ones
  tabulated above; a zero count is a zero count, not a claim that no
  reformulation exists.

Structure

file	content
Basic.lean	Point = ℝ × ℝ, sqDist, chain a h, IsChainValue
Plane.lean	Heron / the triangle inequality without radicals, the anchored 3 × 3 Gram (Cayley–Menger) determinant vanishing for four coplanar points, the 3-vector Gram determinant, the expanded square of a linear combination
PowerThree.lean	exponent rigidity of a chain triangle, and the three Diophantine facts the catalogue needs (3^ℓ = 4·3^j − 1; (3^j − 3^ℓ)² − 3·3^ℓ + 3 = 0; 3^ℓ ∉ {4, 7})
FourPoints.lean	ChainPos, the inductive ChainPattern, the structure ChainQuadruple, and pair_classification
FivePoints.lean	the five-point Gram obstruction and no_five_chain_points
Support.lean	shortest-edge selection; four_chain_adjacent and no_five_chain_finset
CaroWei.lean	Caro–Wei by minimum-degree induction, and exists_independent_five
HopfPannwitz.lean	IsSqDiameter, the diameter graph, and the Hopf–Pannwitz edge bound
Statement.lean	non-diameter support, nonDiameterSqDists_ne_chain, and the 2 ≤ h wrapper
Witnesses.lean	non-vacuity witnesses and the −27 r⁴ determinant record

How the geometry is done

Everything planar reduces to polynomial identities in point coordinates, so
ring discharges them and no square roots appear:

• the triangle inequality is (z − x − y)² ≤ 4xy, i.e. Heron's formula
  4xy − (z−x−y)² = 4·(2·area)²;
• four-point coplanarity is the vanishing of the doubled anchored Gram
  determinant H_ij = d_{0i} + d_{0j} − d_{ij}, H_ii = 2 d_{0i};
• the five-point obstruction is a PSD failure. Four points at squared distance
  c from a common centre with pairwise squared distances in {c, 3c} give
  vectors with ⟪uᵢ,uⱼ⟫ = ±c/2; singularity of every 3-vector Gram forces each
  triple product to be −c³/8, and the explicit combination
  c·u₁ − 2⟪u₁,u₂⟫·u₂ − 2⟪u₁,u₃⟫·u₃ − 2⟪u₁,u₄⟫·u₄ has squared length −2c³ < 0.
  A sum-of-squares contradiction cannot miss a principal minor the way an
  enumerated PSD test can. The equivalent determinant value is recorded as
  symDet4_chain_five (−27 r⁴) alongside symDet4_dotp_eq_zero.

How the supporting Hopf–Pannwitz proof goes

The textbook proof argues that two diameter segments must intersect, then that a
vertex of degree ≥ 3 has a degree-1 neighbour by an angular argument on the
60° arc. Neither step is needed here.

sum_degree_le deletes a pendant vertex using one identity. Let A, B, C be
the vectors from a point v to three points at squared distance D, and let
X = A × B, Y = B × C, Z = A × C be the plane cross products. Cramer's rule
is the polynomial identity Z • B = Y • A + X • C, and comparing squared lengths
turns maximality of D into Z < X + Y. If X, Y > 0 — that is, if B lies
strictly between A and C, which exists_middle always arranges for one of
the three — then any w with sqDist b w = D satisfies ⟪B, w−v⟫ = |w−v|²/2
while ⟪A, w−v⟫ and ⟪C, w−v⟫ are at least that, purely because D dominates
every squared distance. Pairing Cramer's identity with w − v gives
(X + Y − Z)·|w−v|² ≤ 0, hence w = v. Induction on #X removes that pendant
vertex, which costs exactly two from the degree sum.

sum_degree_le is stated for any D > 0 dominating the squared distances of
X; it never needs D to be attained. hopfPannwitz is the corollary for an
actual squared diameter.

Non-vacuity

chainTwo_nonDiameter_support is a five-point set — the rhombus of two glued
equilateral triangles together with the reflection of one vertex, at
(0,0), (1,0), (−½, √3/2), (½, √3/2), (0, √3) — whose squared diameter
is 4 and whose non-diameter squared-distance set is exactly
chain 1 2 = {1, 3}. So the configuration the headline forbids for n ≥ 13 is
realisable at n = 5 with h = 2: the theorem is not vacuous inside its own
h ≥ 2 regime, and the bound on n is doing the work.

rhombus_nonDiameter_support is the same kind of witness at chain length one,
and rhombus_chain_config / centroid_chain_config exhibit the two planar
patterns the chain-quadruple theorem classifies.

Card metadata

source.github_repo is set to lyfar/lean-pool. This formalization has no
upstream project — the Lean was written directly for the pool — but
quality.py requires the field, so it points at the fork the branch lives in.
The partial-port audit that consumes it is advisory.

Receipts

On upstream/main 3fc79f0a, toolchain and Mathlib v4.34.0-rc1.

• lake exe mk_all --check — No update necessary
• lake build LeanPool — Build completed successfully (8906 jobs), zero
  error: / warning: lines in the log (whole pool)
• lake build LeanPool Challenge Solution — Build completed successfully (8928 jobs); the only warnings are the three declaration uses 'sorry' lines
  from the pre-existing Challenge/ statements
• lake exe runLinter LeanPool.Erdos132ThreeChain — Linting passed
• lake exe lint-style LeanPool — exit 0, no findings
• python -m lean_pool.quality --repo .. — Quality checks passed.
• grep -nE '\b(sorry|admit|axiom|native_decide|unsafe|partial|opaque|constant|set_option|nolint|#check|#print|#eval|#reduce|#guard_msgs|#lint)\b'
  over the namespace — no matches; no bare import Mathlib; every line ≤ 100
  characters; all eleven files carry the four-line header
• #print axioms on nonDiameterSqDists_ne_chain, threeChain_support_empty,
  four_chain_adjacent, pair_classification, no_five_chain_finset,
  no_five_chain_points, no_four_on_circle, carowei,
  exists_independent_five, hopfPannwitz, sum_degree_le, exists_pendant,
  middle_no_other_neighbour, chainTwo_nonDiameter_support,
  chainTwo_config, rhombus_nonDiameter_support, symDet4_chain_five,
  rhombus_chain_config, centroid_chain_config — every one is exactly
  [propext, Classical.choice, Quot.sound]

1713 lines of Lean across eleven files.

Known gaps

1. sum_degree_le proves the Hopf–Pannwitz edge bound, not the extremal
   characterization (odd cycles with pendant trees).
2. pair_classification exports the seven labelled patterns relative to a
   shortest edge; dropping the choice of shortest edge these are the 6 + 4 = 10
   labelled assignments per adjacent pair, i.e. 10(h−1) over a chain of length
   h. A labelling-free set-level restatement of that count is not exported;
   four_chain_adjacent exports only the coarser "all six lie in {r, 3r}".

🤖 Generated with Claude Code

[greptile-apps]

Greptile Summary

The PR adds a self-contained Lean formalization ruling out geometric ratio-three chains as the complete non-diameter squared-distance support of sufficiently large planar point sets.

• Adds coordinate geometry, power-of-three rigidity, four- and five-point obstruction modules.
• Adds Caro–Wei and Hopf–Pannwitz supporting arguments.
• Registers the project and exposes it through the aggregate LeanPool entry point.

Important Files Changed

Filename	Overview
LeanPool/Erdos132ThreeChain/Statement.lean	States the headline theorem with quantifiers and definitions matching the project-card description.
LeanPool/Erdos132ThreeChain/FourPoints.lean	Formalizes the four-point chain classification and its seven labelled patterns.
LeanPool/Erdos132ThreeChain/FivePoints.lean	Derives the five-point obstruction from the planar Gram identities and four-point classification.
LeanPool/Erdos132ThreeChain/HopfPannwitz.lean	Supplies the diameter-graph degree bound used by the headline theorem.
LeanPool/Erdos132ThreeChain/CaroWei.lean	Proves the independence bound and specializes it to obtain five independent vertices.
LeanPool/Erdos132ThreeChain/Witnesses.lean	Provides non-vacuity witnesses for the chain configurations discussed by the project.
LeanPool/Erdos132ThreeChain.lean	Defines the project entry module and exposes the headline, supporting bound, and witnesses.
LeanPool/projects.yml	Registers the formalization, provenance, prior-art disclosure, and exact informal headline.
LeanPool.lean	Adds the project and all of its modules to the aggregate library entry point.

_{Reviews (10): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile}

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 130.12 s (= 2.17 min) — user 149.79 s, sys 13.94 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 190 maxHeartbeats units across 11 files (1,595 added LOC).

Sum of lean --profile: 119644.8 ms (= 119.64 s). Import-excluded time: 107064.8 ms (= 107.06 s).

Count-heartbeats wall-clock total: 120.04 s. Repeated import cost inside lean --profile: 12580.0 ms (= 12.58 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

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/Erdos132ThreeChain/HopfPannwitz.lean	301	38	10.43	7.53	6.47	1.06	18	0
LeanPool/Erdos132ThreeChain/PowerThree.lean	179	32	5.35	5.85	4.80	1.05	16	0
LeanPool/Erdos132ThreeChain/FourPoints.lean	312	30	5.11	5.48	4.42	1.06	15	0
LeanPool/Erdos132ThreeChain/Basic.lean	80	28	3.07	2.32	1.24	1.08	13	0
LeanPool/Erdos132ThreeChain/Plane.lean	88	20	5.04	3.63	2.60	1.03	10	0
LeanPool/Erdos132ThreeChain/Witnesses.lean	131	14	73.20	84.03	82.51	1.52	7	0
LeanPool/Erdos132ThreeChain/CaroWei.lean	152	8	3.81	2.54	1.48	1.06	4	0
LeanPool/Erdos132ThreeChain/FivePoints.lean	120	8	3.71	2.08	1.01	1.07	4	0
LeanPool/Erdos132ThreeChain/Support.lean	155	8	4.10	3.15	2.09	1.06	4	0
LeanPool/Erdos132ThreeChain/Statement.lean	57	4	2.82	1.30	0.24	1.06	2	0
LeanPool/Erdos132ThreeChain.lean	20	0	3.40	1.73	0.20	1.53	0	0
Total	1,595	190	120.04	119.64	107.06	12.58	93	0

Aggregate phase totals

Phase	Time
type checking	22054.7 ms (= 22.05 s)
process pre-definitions	18457.2 ms (= 18.46 s)
share common exprs	14788.0 ms (= 14.79 s)
interpretation	13889.0 ms (= 13.89 s)
ring	13441.3 ms (= 13.44 s)
import	12580.0 ms (= 12.58 s)
tactic execution	8363.3 ms (= 8.36 s)
elaboration	8176.4 ms (= 8.18 s)
typeclass inference	3538.9 ms (= 3.54 s)
fix level params	1041.9 ms (= 1.04 s)
norm_num	1015.9 ms (= 1.02 s)
simp	624.8 ms (= 0.62 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.Erdos132ThreeChain.Witnesses	102.00 s
LeanPool.Erdos132ThreeChain.HopfPannwitz	7.10 s
LeanPool.Erdos132ThreeChain.CaroWei	4.40 s
LeanPool.Erdos132ThreeChain.FourPoints	4.30 s
LeanPool.Erdos132ThreeChain.PowerThree	4.20 s
LeanPool.Erdos132ThreeChain.Plane	4.10 s
LeanPool.Erdos132ThreeChain.Basic	3.70 s
LeanPool.Erdos132ThreeChain.Support	3.00 s
LeanPool.Erdos132ThreeChain.FivePoints	1.90 s
LeanPool.Erdos132ThreeChain	1.80 s
LeanPool.Erdos132ThreeChain.Statement	1.30 s

Per-file `lean --profile` output

LeanPool/Erdos132ThreeChain.lean

import took 1.53s
cumulative profiling times:
	elaboration 0.164ms
	import 1.53s
	initialization 30.3ms
	interpretation 168ms
	linting 0.293ms
	module linting 0.00171ms
	overlappingInstancesLinter 0.547ms
	parsing 0.0325ms
	tacticAnalysis 2.33ms
real 2.54
user 1.44
sys 1.11

LeanPool/Erdos132ThreeChain/Basic.lean

import took 1.08s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 106ms
cumulative profiling times:
	attribute application 0.363ms
	blocked (unaccounted) 382ms
	compilation (IR) 0.105ms
	compilation (LCNF base) 2.09ms
	compilation (LCNF impure) 1.28ms
	compilation (LCNF mono) 1.55ms
	congr simp thm 1.22ms
	elaboration 34.2ms
	fix level params 0.571ms
	import 1.08s
	initialization 36.5ms
	instantiate metavars 1.22ms
	interpretation 477ms
	let-to-have transformation 0.129ms
	linting 7.05ms
	module linting 0.0017ms
	norm_num 10.3ms
	overlappingInstancesLinter 3.88ms
	parsing 5.74ms
	process pre-definitions 6.13ms
	ring 37.8ms
	share common exprs 9.06ms
	simp 18.2ms
	tactic execution 33.6ms
	tacticAnalysis 16.2ms
	type checking 30.1ms
	typeclass inference 120ms
real 2.40
user 1.68
sys 0.94

LeanPool/Erdos132ThreeChain/CaroWei.lean

import took 1.06s
cumulative profiling times:
	attribute application 0.0497ms
	compilation (IR) 0.0571ms
	compilation (LCNF base) 0.451ms
	compilation (LCNF impure) 0.238ms
	compilation (LCNF mono) 0.452ms
	congr simp thm 6ms
	elaboration 27.2ms
	fix level params 1.94ms
	import 1.06s
	initialization 31ms
	instantiate metavars 3.03ms
	interpretation 540ms
	let-to-have transformation 0.0674ms
	linting 25ms
	module linting 0.0015ms
	norm_num 84.5ms
	overlappingInstancesLinter 3.92ms
	parsing 10.3ms
	process pre-definitions 12.5ms
	ring 29.8ms
	share common exprs 10.1ms
	simp 188ms
	tactic execution 182ms
	tacticAnalysis 30.5ms
	type checking 55ms
	typeclass inference 240ms
real 2.65
user 2.33
sys 0.94

LeanPool/Erdos132ThreeChain/FivePoints.lean

import took 1.07s
cumulative profiling times:
	attribute application 0.055ms
	congr simp thm 0.552ms
	elaboration 30ms
	fix level params 1.12ms
	import 1.07s
	initialization 32.4ms
	instantiate metavars 3.33ms
	interpretation 358ms
	let-to-have transformation 0.0957ms
	linting 22.1ms
	module linting 0.00141ms
	norm_num 73.3ms
	overlappingInstancesLinter 2.11ms
	parsing 7.72ms
	process pre-definitions 12.2ms
	ring 72ms
	share common exprs 15.6ms
	simp 2.94ms
	tactic execution 126ms
	tacticAnalysis 23ms
	type checking 67.6ms
	typeclass inference 162ms
real 2.34
user 1.90
sys 0.90

LeanPool/Erdos132ThreeChain/FourPoints.lean

import took 1.06s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 446ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 298ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 251ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 166ms
cumulative profiling times:
	attribute application 0.182ms
	blocked (unaccounted) 0.77ms
	congr simp thm 2.27ms
	elaboration 129ms
	fix level params 3.9ms
	import 1.06s
	initialization 36.3ms
	instantiate metavars 12.1ms
	interpretation 1.98s
	let-to-have transformation 0.368ms
	linting 90.1ms
	module linting 0.0017ms
	norm_num 21.9ms
	overlappingInstancesLinter 6.2ms
	parsing 29.6ms
	process pre-definitions 39.4ms
	ring 263ms
	share common exprs 92.3ms
	simp 80.2ms
	tactic execution 675ms
	tacticAnalysis 86.1ms
	type checking 279ms
	typeclass inference 594ms
real 3.45
user 5.26
sys 0.88

LeanPool/Erdos132ThreeChain/HopfPannwitz.lean

import took 1.06s
ring took 201ms
share common exprs took 140ms
type checking took 185ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 301ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 767ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 649ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 477ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.12s
cumulative profiling times:
	attribute application 0.456ms
	congr simp thm 2.56ms
	elaboration 181ms
	fix level params 13.2ms
	import 1.06s
	initialization 31.1ms
	instantiate metavars 7.75ms
	interpretation 3.96s
	let-to-have transformation 0.26ms
	linting 69.9ms
	module linting 0.00206ms
	norm_num 15.5ms
	overlappingInstancesLinter 7.17ms
	parsing 22.6ms
	process pre-definitions 106ms
	ring 410ms
	share common exprs 218ms
	simp 49.6ms
	tactic execution 351ms
	tacticAnalysis 68.5ms
	type checking 411ms
	typeclass inference 549ms
real 5.82
user 7.31
sys 0.92

LeanPool/Erdos132ThreeChain/Plane.lean

import took 1.03s
ring took 289ms
share common exprs took 162ms
type checking took 208ms
ring took 241ms
share common exprs took 134ms
type checking took 210ms
cumulative profiling times:
	attribute application 0.122ms
	compilation (IR) 0.328ms
	compilation (LCNF base) 8.11ms
	compilation (LCNF impure) 1.43ms
	compilation (LCNF mono) 3.81ms
	congr simp thm 0.641ms
	elaboration 227ms
	fix level params 17.4ms
	import 1.03s
	initialization 30.7ms
	instantiate metavars 0.841ms
	interpretation 336ms
	let-to-have transformation 0.168ms
	linting 7.97ms
	module linting 0.00164ms
	norm_num 13.1ms
	overlappingInstancesLinter 3.14ms
	parsing 7.34ms
	process pre-definitions 134ms
	ring 706ms
	share common exprs 357ms
	simp 16.8ms
	tactic execution 13.6ms
	tacticAnalysis 17.8ms
	type checking 570ms
	typeclass inference 127ms
real 3.06
user 3.42
sys 0.93

LeanPool/Erdos132ThreeChain/PowerThree.lean

import took 1.05s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 258ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 323ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 132ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 592ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 369ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 156ms
cumulative profiling times:
	attribute application 0.193ms
	blocked (unaccounted) 0.899ms
	congr simp thm 1.05ms
	elaboration 84.8ms
	fix level params 2.67ms
	import 1.05s
	initialization 30.3ms
	instantiate metavars 12.8ms
	interpretation 2.56s
	let-to-have transformation 0.245ms
	linting 45.2ms
	module linting 0.00163ms
	norm_num 36.1ms
	overlappingInstancesLinter 5.28ms
	parsing 15.8ms
	process pre-definitions 31.8ms
	ring 317ms
	share common exprs 77.7ms
	simp 84.4ms
	tactic execution 262ms
	tacticAnalysis 38.9ms
	type checking 370ms
	typeclass inference 820ms
real 3.52
user 5.61
sys 0.91

LeanPool/Erdos132ThreeChain/Statement.lean

import took 1.06s
cumulative profiling times:
	attribute application 0.0217ms
	elaboration 5.04ms
	fix level params 0.0527ms
	import 1.06s
	initialization 30.3ms
	instantiate metavars 0.141ms
	interpretation 162ms
	let-to-have transformation 0.023ms
	linting 2.64ms
	module linting 0.00166ms
	overlappingInstancesLinter 1.42ms
	parsing 2.05ms
	process pre-definitions 0.79ms
	share common exprs 0.264ms
	tactic execution 12.1ms
	tacticAnalysis 8.33ms
	type checking 7.86ms
	typeclass inference 2.91ms
real 1.94
user 1.08
sys 0.91

LeanPool/Erdos132ThreeChain/Support.lean

import took 1.06s
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 229ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 364ms
cumulative profiling times:
	attribute application 0.0568ms
	congr simp thm 2.45ms
	elaboration 28ms
	fix level params 1.08ms
	import 1.06s
	initialization 30.2ms
	instantiate metavars 7.02ms
	interpretation 888ms
	let-to-have transformation 0.103ms
	linting 23.7ms
	module linting 0.00153ms
	norm_num 2.24ms
	overlappingInstancesLinter 2.96ms
	parsing 11.8ms
	process pre-definitions 14.4ms
	ring 5.72ms
	share common exprs 7.94ms
	simp 83.7ms
	tactic execution 738ms
	tacticAnalysis 37.4ms
	type checking 64.1ms
	typeclass inference 142ms
real 3.32
user 2.95
sys 0.90

LeanPool/Erdos132ThreeChain/Witnesses.lean

import took 1.52s
ring took 11.4s
share common exprs took 13.9s
fix level params took 1s
process pre-definitions took 18s
elaboration took 7.36s
type checking took 20.1s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 126ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 129ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 131ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 131ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 115ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 121ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 124ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 106ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 106ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 110ms
tactic execution of Lean.Parser.Tactic.exact took 690ms
tactic execution of Lean.Parser.Tactic.exact took 694ms
tactic execution of Lean.Parser.Tactic.exact took 606ms
tactic execution of Lean.Parser.Tactic.exact took 413ms
tactic execution of Lean.Parser.Tactic.exact took 412ms
tactic execution of Lean.Parser.Tactic.exact took 409ms
tactic execution of Lean.Parser.Tactic.exact took 411ms
tactic execution of Lean.Parser.Tactic.exact took 407ms
tactic execution of Lean.Parser.Tactic.exact took 414ms
tactic execution of Lean.Parser.Tactic.exact took 416ms
tactic execution of Lean.Parser.Tactic.exact took 409ms
tactic execution of Lean.Parser.Tactic.exact took 417ms
cumulative profiling times:
	attribute application 0.105ms
	compilation (IR) 0.24ms
	compilation (LCNF base) 6.96ms
	compilation (LCNF impure) 0.782ms
	compilation (LCNF mono) 3.34ms
	congr simp thm 3.82ms
	elaboration 7.43s
	fix level params 1s
	import 1.52s
	initialization 31.1ms
	instantiate metavars 3.41ms
	interpretation 2.46s
	let-to-have transformation 0.193ms
	linting 14.4ms
	module linting 0.00167ms
	norm_num 759ms
	overlappingInstancesLinter 3.03ms
	parsing 10.9ms
	process pre-definitions 18.1s
	ring 11.6s
	share common exprs 14s
	simp 101ms
	tactic execution 5.97s
	tacticAnalysis 31.8ms
	type checking 20.2s
	typeclass inference 782ms
real 74.65
user 82.87
sys 1.88

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

[github-actions]

🤖 LLM review (gpt-5.6-sol, 5 rubrics)

Reviewed head: 05938920404900f808c553decc9cc10bf6a2ab8e

Verdict: 🤔 needs_discussion — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	Each listed declaration matches its card informal, and the main theorem is unconditional beyond the explicitly stated geometric and cardinality hypotheses.
Novelty	🤔 discuss	No headline duplicate is identified, but Mathlib prior art is unverifiable for seven of the eight headlines because their searches failed.
Significance	✅ pass	The project is a research-level discrete-geometry development with a clear 13-point support theorem, a four-point classification, and a five-point obstruction.
Sources	✅ pass	The cited Erdős problem is explicitly identified as ambient context rather than the source of the new 3-chain result, and the disclosed classical and prior Lean results are credited.
Code quality (advisory)	✅ pass	The Lean is modular, with reusable geometric and arithmetic lemmas and the finite case analyses localized to classification and witness proofs.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The headline assumes 13 ≤ n, 0 < a, X.card = n, and IsSqDiameter X D; the card states all four, and the supporting results introduce no undisclosed mathematical inputs.
Matches cited source	➖ not_a_known_result
Fit	✅ good_fit
Level	research
Branch	discrete geometry
Mode	theory_building
Code quality	4 / 5

Statement check: The main theorem proves that for 13 ≤ n, 0 < a, X.card = n, and IsSqDiameter X D, the set nonDiameterSqDists X D differs from chain a h for every natural-number chain length h.

It proves an unconditional obstruction to geometric 3-chain distance spectra in planar point sets, supported by a classification of four-point configurations and the theorem that no five-point planar set has all squared distances in one such chain.

Novelty findings (1)

• prior-art-unchecked — PR-wide
  Mathlib novelty is unchecked for Erdos132ThreeChain.nonDiameterSqDists_ne_chain, Erdos132ThreeChain.pair_classification, Erdos132ThreeChain.no_five_chain_finset, Erdos132ThreeChain.no_four_on_circle, Erdos132ThreeChain.carowei, Erdos132ThreeChain.exists_independent_five, and Erdos132ThreeChain.chainTwo_nonDiameter_support. The completed search for Erdos132ThreeChain.four_chain_adjacent returned only unrelated declarations.
  Evidence: The supplied Prior art section marks the Mathlib search as failed for each of those seven declarations, so no existing declaration is available for comparison.

---

Tokens: 218,315 in / 10,579 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $0.7045
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[lyfar]

Thanks — all six findings are addressed at the new head 219cfd42. Summary of what changed.

overclaimed-headline (faithfulness, blocking). Fixed twice over.

The card sentence that identified the h = 1 rhombus with the headline's
forbidden regime is gone. More usefully, there is now a genuine witness inside
the h ≥ 2 regime:

theorem chainTwo_nonDiameter_support :
    ∃ X : Finset Point, X.card = 5 ∧ IsSqDiameter X 4 ∧ nonDiameterSqDists X 4 = chain 1 2

The set is (0,0), (1,0), (−½, √3/2), (½, √3/2), (0, √3) — the rhombus
of two glued equilateral triangles plus the reflection of one vertex. Its ten
squared distances are 1 seven times, 3 twice and 4 once, so the squared
diameter is 4 and the non-diameter support is exactly {1, 3} = chain 1 2.
The configuration the headline forbids at n ≥ 13 is therefore realisable at
n = 5 with h = 2: the bound on n is what is doing the work, not vacuity.

rhombus_nonDiameter_support is kept as the chain-length-one witness and the
card now says so in those words.

partial-overlap (novelty). Confirmed, and disclosed in both the card and
the PR body. LeanPool.Erdos132N14.diameterEdges_card_le proves the same
mathematical statement — a positive maximal distance is realised at most #S
times — by Perles charging, assigning each diameter edge to a clockwise-extreme
endpoint, stated for a Configuration ι (an injective map from a LinearOrder
index type into ℂ) as a bound on the cardinality of a Finset of unordered
pairs. Erdos132ThreeChain.hopfPannwitz works over a Finset (ℝ × ℝ), in
squared distances, and concludes in handshake form
∑ v ∈ X, degree (DiameterAdj D) X v ≤ 2 * #X; the proof is a pendant-deletion
induction driven by Cramer's rule rather than a charging argument. Neither
statement is an instance of the other without a model bridge (a LinearOrder on
ℝ × ℝ, a dist-to-sqDist transfer, and a handshake lemma).

It is reproved rather than imported because no project in the pool imports
another: CONTRIBUTING.md states the projects are independent, and a scan of
every import LeanPool.* line under LeanPool/ finds zero cross-project
imports today. If the maintainers would rather this project depend on
Erdos132N14, that is a small change and I will make it.

prior-art-unverifiable (novelty). The prior-art section is rewritten as a
table of the exact grep -rEil patterns run against the pinned Mathlib and
against LeanPool/, with the file counts and the actual files hit, so it can be
rerun. Three pool hits that the earlier draft did not surface are now named:
Erdos97ConvexOctagon.cm4_sqDist_eq_zero (same four-point Cayley–Menger
vanishing, over EuclideanSpace ℝ (Fin 2)), DistanceGeometry.schoenberg
(never invoked here — the four-point condition is used as a ring identity and
the five-point step is a sum-of-squares contradiction), and the Erdos132N14
diameter modules above. The section also says plainly that a zero count is a
zero count for the patterns listed, not a claim that no reformulation exists.

source-inconsistency (sources). The "Theorem 4" / "Theorem 5" labels were
internal numbering carried over from working notes, and the PR text calling the
determinant and the counts "the source's" was simply wrong. Both are gone. The
docstrings now read "the chain-quadruple theorem" and "the five-point
obstruction", the module docstring states that these are internal names
referring to no numbered result elsewhere, and the card says the same. There is
no prior write-up: the 3-chain statement was produced by the author's automated
research pipeline in August 2026, and the cited page poses the ambient problem
and states nothing about geometric 3-chains. Hopf–Pannwitz (1934) and Caro–Wei
are classical statements whose Lean proofs here are written from scratch.

unused-hypothesis (code quality). Taken as suggested. The main declaration
is now the unbounded form

theorem nonDiameterSqDists_ne_chain {X : Finset Point} {D a : ℝ} {n h : ℕ}
    (hn : 13 ≤ n) (ha : 0 < a) (hcard : X.card = n) (hD : IsSqDiameter X D) :
    nonDiameterSqDists X D ≠ chain a h

and threeChain_support_empty is a one-line wrapper carrying 2 ≤ h for
statement fidelity. The card's main_declarations points at the unbounded form.

agent-slop (code quality). ChainPattern is now an inductive Prop with
seven named constructors (longCD, longBD, longAD, longBC, longAC,
centreA, centreB), each documented; the deep Or.inr chains are gone and the
branches read .longBD hx1 hx2 hd1 hd2 hl. pair_classification returns a
structure ChainQuadruple with named fields (posC, posD, distCD,
sharedLeft, sharedRight, pattern), and ChainPos is a structure with
fields fromLeft, fromRight, nearEnd. Downstream proofs use the field names
instead of positional projections. The mathematical content is unchanged.

prompt-injection (all three rubrics). Fair, and my mistake. The PR body no
longer addresses the reviewer, and the claims of prior independent verification
are removed. Provenance is now a plain statement of who produced the statement
and when, with no request attached.

Receipts at the new head. lake exe mk_all --check clean; lake build LeanPool 8906 jobs with zero error/warning lines; lake exe runLinter LeanPool.Erdos132ThreeChain passed; lake exe lint-style LeanPool exit 0;
python -m lean_pool.quality --repo .. passed; #print axioms on nineteen
declarations, including every headline, is exactly
[propext, Classical.choice, Quot.sound].

[lyfar]

partial-overlap: the card now carries the overlapping declaration's Lean
statement verbatim, so duplication is decidable from the card alone.

The summary quotes, exactly as they appear in the sources:

theorem diameterEdges_card_le
    (P : Configuration ι) (S : Finset ι) {d : ℝ}
    (hd : 0 < d)
    (hmax : ∀ f ∈ pairs S, P.pairDistance f ≤ d) :
    (diameterEdges P S d).card ≤ S.card

from LeanPool/Erdos132N14/HopfPannwitz.lean, together with the definitions it
depends on (Configuration ι carries an injective point : ι → ℂ;
pairs S = (S ×ˢ S).filter fun e ↦ e.1 < e.2 for a LinearOrder ι;
pairDistance P e = dist (P.point e.1) (P.point e.2);
diameterEdges P S d = (pairs S).filter fun e ↦ P.pairDistance e = d), and

theorem hopfPannwitz {X : Finset Point} {D : ℝ} (hD : IsSqDiameter X D) :
    ∑ v ∈ X, degree (DiameterAdj D) X v ≤ 2 * X.card

with Point = ℝ × ℝ, DiameterAdj D p q = (p ≠ q ∧ sqDist p q = D),
degree adj X v = (X.filter (adj v)).card, and IsSqDiameter X D asserting that
D is realised by two distinct points of X and dominates every squared
distance inside X. The model-difference explanation from the previous round is
unchanged and now sits directly beneath the two statements.

Checking the rest of the card for the same gap turned up two more named
overlaps that were previously only in the PR body, so both now appear in the
card with their statements as well:

theorem cm4_sqDist_eq_zero (a b c d : Plane) :
    cm4 (sqDist a b) (sqDist a c) (sqDist a d)
      (sqDist b c) (sqDist b d) (sqDist c d) = 0

from LeanPool/Erdos97ConvexOctagon/CayleyMenger.lean over
Plane = EuclideanSpace ℝ (Fin 2), quoted beside this project's
gramDet_eq_zero over Point = ℝ × ℝ — the same four-point Cayley–Menger
vanishing, both one-line ring identities; and

theorem schoenberg {D : Matrix (Fin n) (Fin n) ℝ} (hD : IsPreDistMatrix D) :
    EmbedsIn D k ↔ (centeredGram D).PosSemidef ∧ (centeredGram D).rank ≤ k

from LeanPool/DistanceGeometry/SchoenbergHard.lean, which this project never
invokes.

Every quoted block was checked back against its source file, line breaks
included. This is a card-only change; the Lean is byte-identical to the previous
head.

Receipts at da7defb6: lake exe mk_all --check — No update necessary;
lake build LeanPool — Build completed successfully (8906 jobs), zero
error: / warning: lines; python -m lean_pool.quality --repo .. —
Quality checks passed.

[lyfar]

partial-overlap: ruling accepted. hopfPannwitz is demoted — it is no longer
presented as a result of this project.

Card. Erdos132ThreeChain.hopfPannwitz is removed from main_results. The
summary now says outright that it is not offered as a new result: the same
bound already exists in the pool as
LeanPool.Erdos132N14.diameterEdges_card_le, the copy here exists only so this
project is self-contained under the pool's no-cross-project-imports convention
(CONTRIBUTING.md), and it is a supporting lemma rather than one of the
project's results. The verbatim statements of both declarations, and the model
difference between them, stay in the card exactly as added last round — the
disclosure is unchanged, only the claim attached to it is.

Its main_results slot is filled by Erdos132ThreeChain.exists_independent_five,
which the prior-art section already covers (indepNum is a definition with no
lower bound; isTuranMaximal is the extremal-graph characterization; neither
supplies this):

theorem exists_independent_five (adj : α → α → Prop) [DecidableRel adj]
    (hsymm : ∀ a b, adj a b → adj b a) (hirr : ∀ a, ¬ adj a a) (V : Finset α)
    (hcard : 13 ≤ V.card) (hdeg : ∑ v ∈ V, degree adj V v ≤ 2 * V.card) :
    ∃ S ⊆ V, S.card = 5 ∧ ∀ p ∈ S, ∀ q ∈ S, ¬ adj p q

main_results stays at eight and still covers main_declarations.

Code. The theorem stays where it is, because the proof of the headline needs
it. Two module docstrings now carry the same disclaimer as the card:
HopfPannwitz.lean states that nothing in it is claimed as new and names the
pooled declaration it reproves, and Statement.lean marks Hopf–Pannwitz as the
one supporting lemma among the ingredients. No proof changed.

PR body. The headline block now lists two theorems, not three. The lift is
described as exists_independent_five consuming a degree-sum bound that
hopfPannwitz supplies, with the duplication stated in bold at the point of
first mention. The prior-art entry now quotes both statements inline and ends by
saying the declaration is deliberately absent from main_results.

Receipts at 7581200d: lake exe mk_all --check — No update necessary;
lake build LeanPool — Build completed successfully (8906 jobs), zero
error: / warning: lines; python -m lean_pool.quality --repo .. —
Quality checks passed.

[Vilin97]

I reviewed head 7581200d429415ca8aecf5da2520707702513514 through the diameter-graph/Caro–Wei reduction, the four-point classification, the five-point obstruction, and the nonvacuity witnesses.

The formal mathematics checks out. The headline is unconditional, the h = 2 witness addresses the obvious vacuity concern, and I found no existing Mathlib/Lean Pool formalization of either the ratio-three headline or the general Caro–Wei lemma. The disclosed Hopf–Pannwitz and Cayley–Menger overlap is accurate. CI is green.

I am requesting changes for a severe avoidable compile cost. Witnesses.lean:30–57 is an unused expanded symDet4* appendix. CI attributes 84.0s profile time (82.5s excluding imports) to Witnesses.lean, versus at most 7.5s for every other module; the changed-module build spent 102s there. A focused cached run also peaked around 6.6 GB RSS. The determinant expansion and ring proof do not feed the headline, and no_four_on_circle already supplies the equivalent obstruction used by the development. Remove this appendix or refactor it substantially before imposing that cost on every pool build.

There is also a documentation error at Witnesses.lean:85–88: the rhombus has h = 1, so it cannot witness threeChain_support_empty, whose wrapper assumes 2 ≤ h. It witnesses the hypotheses of nonDiameterSqDists_ne_chain instead.

On fit, my opinion is borderline but favorable if the cost is fixed. This is substantial original discrete geometry, and Caro–Wei is genuinely reusable, but the ratio 3 is currently an ad hoc restriction with no prior write-up; the cited source does not state it and it does not resolve Erdős #132. Much of the remaining infrastructure is specialized, while roughly 300 lines reprove an existing pool diameter bound. I would accept it as a medium-sized research formalization, but the card should continue to be as explicit as it currently is about that limited relationship to the ambient problem.

[lyfar]

Both fixed, and the cost item is measured rather than asserted.

1. Witnesses.lean:30–57, the unused symDet4 appendix. Removed — symDet4,
symDet4_dotp_eq_zero, symDet4_chain_five, symDet4_chain_five_ne_zero are deleted. You were right
that nothing consumes them; no_four_on_circle supplies the obstruction the development uses, and a
branch-wide grep for symDet4 now returns nothing.

Measured by elaborating the module out of tree, /usr/bin/time -l lake env lean:

	before (7581200d)	after (head)
wall	126.45 s	14.58 s
peak RSS	6.31 GB	2.31 GB

Two caveats so the numbers are comparable to yours. My before/after are whole-module wall times on one
machine, not CI profile time, so they are not directly the 84.0 s figure you quoted — the 6.31 GB does
reproduce your ~6.6 GB peak. An earlier run of the same comparison on a differently loaded machine gave
64.8 s → 13.96 s; the absolute walls move with load, the collapse does not.

2. Witnesses.lean:85–88. Corrected. The docstring now says the rhombus has h = 1, that the
headline wrapper assumes 2 ≤ h so the rhombus cannot witness it, and that it witnesses the hypotheses
of nonDiameterSqDists_ne_chain.

3. Card. Unchanged and re-checked: ratio 3 is still called ad hoc, still noted as absent from the
cited source, and still stated not to resolve Erdős #132.

lake build LeanPool.Erdos132ThreeChain, runLinter LeanPool, lint-style LeanPool and
mk_all --check all pass; #print axioms on threeChain_support_empty,
nonDiameterSqDists_ne_chain and carowei gives [propext, Classical.choice, Quot.sound] for each.

[Vilin97]

Rereviewed at 6401538d.

The earlier requested changes are resolved. The unused expanded symDet4* appendix is gone; a fresh targeted build completed all 11 modules in 16.85s wall time at 2.67 GB peak RSS, and profiling Witnesses.lean took 6.50s rather than the previous 84s / roughly 6.6 GB. The rhombus documentation now correctly says that it has h = 1, cannot witness the 2 ≤ h wrapper, and deliberately fails the cardinality regime.

The substantive assessment passes. The headline theorem faithfully proves the card claim and has a genuine five-point, chain-length-two nonvacuity witness. I found no Mathlib or pool theorem subsuming the ratio-three classification or five-point obstruction; the closest overlaps are accurately disclosed. Fit is borderline but favorable: the ratio-three restriction is ad hoc and does not solve Erdős 132, but this is still research-level discrete geometry with a substantial classification/obstruction, plus reusable relation-level carowei and exists_independent_five infrastructure. The 308-line Hopf–Pannwitz reproof is disclosed and acceptable under the self-contained-project convention. Code organization and current compile cost are good for Lean Pool.

One small source-attribution blocker remains. In LeanPool/projects.yml, the cited source is “Erdos Problem #132” and its author list contains only Paul Erdős, but the cited page explicitly says “Asked by Erdős and Pach.” Please add János Pach to source.authors. After that citation correction and a green exact-head build, I would approve.

[Vilin97]

Maintainer follow-up at 05938920: the remaining citation issue is fixed by crediting both Paul Erdős and János Pach, and the compilation path has been materially optimized. The unused rhombus_nonDiameter_support theorem was removed; the retained chain-length-two witness now uses deterministic simplification instead of backtracking; and the lightweight diameter/support definitions moved into Basic without changing their names or types, allowing Witnesses to compile independently of the full theorem DAG. Independent measurements show Witnesses.lean at 6.39s → 3.30s median wall time and the registered witness at 5.954s → 0.318s. A current-main targeted build, declaration linter, style linter, generated-index check, and diff check all pass. Approved pending exact-head CI.