Repository navigation
Conversation
Proof profile (new / modified Lean files)
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: 135 maxHeartbeats units across 21 files (2,816 added LOC). Sum of Count-heartbeats wall-clock total: 90.55 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.RareDistanceFields.BipartiteDiameter |
16.00 s |
LeanPool.RareDistanceFields.OctagonalNorm |
11.00 s |
LeanPool.RareDistanceFields.DyadicNorm |
10.00 s |
LeanPool.RareDistanceFields.OrderedColors |
6.50 s |
LeanPool.RareDistanceFields.SplitCounts |
4.30 s |
LeanPool.RareDistanceFields.PureTranscendental |
3.80 s |
LeanPool.RareDistanceFields.DyadicCoordinates |
3.30 s |
LeanPool.RareDistanceFields.DyadicLevels |
3.20 s |
LeanPool.RareDistanceFields.DyadicSize |
3.10 s |
LeanPool.RareDistanceFields.RationalPlane |
2.80 s |
LeanPool.RareDistanceFields.IntegerPlane |
2.60 s |
LeanPool.RareDistanceFields.BinaryDescent |
2.60 s |
Per-file `lean --profile` output
LeanPool/RareDistanceFields.lean
import took 1.37s
cumulative profiling times:
attribute application 0.0119ms
elaboration 12.5ms
fix level params 0.0623ms
import 1.37s
initialization 41.2ms
instantiate metavars 0.0246ms
interpretation 193ms
let-to-have transformation 0.0258ms
linting 1.39ms
module linting 0.0013ms
overlappingInstancesLinter 1.89ms
parsing 1.41ms
process pre-definitions 0.194ms
share common exprs 0.182ms
tacticAnalysis 4.24ms
type checking 4.14ms
typeclass inference 82.8ms
real 2.41
user 1.43
sys 0.97
LeanPool/RareDistanceFields/BinaryDescent.lean
import took 1.3s
cumulative profiling times:
attribute application 0.0987ms
blocked (unaccounted) 1.13ms
congr simp thm 10.7ms
elaboration 49.1ms
fix level params 0.718ms
import 1.3s
initialization 29ms
instantiate metavars 3.06ms
interpretation 260ms
let-to-have transformation 0.0472ms
linting 12.4ms
module linting 0.00136ms
norm_num 1.37ms
overlappingInstancesLinter 3.81ms
parsing 17.9ms
process pre-definitions 4.31ms
share common exprs 2.67ms
simp 43.3ms
tactic execution 231ms
tacticAnalysis 30.2ms
type checking 128ms
typeclass inference 111ms
real 2.64
user 1.99
sys 0.91
LeanPool/RareDistanceFields/BinaryPalette.lean
import took 1.31s
cumulative profiling times:
attribute application 0.0785ms
congr simp thm 1.6ms
elaboration 35ms
fix level params 0.917ms
import 1.31s
initialization 34.2ms
instantiate metavars 0.913ms
interpretation 251ms
let-to-have transformation 0.124ms
linting 13.6ms
module linting 0.00142ms
overlappingInstancesLinter 4.01ms
parsing 7.89ms
process pre-definitions 4.93ms
share common exprs 2.38ms
simp 57.4ms
tactic execution 131ms
tacticAnalysis 24.3ms
type checking 43.5ms
typeclass inference 338ms
real 2.50
user 1.96
sys 0.95
LeanPool/RareDistanceFields/BinarySize.lean
import took 1.32s
cumulative profiling times:
attribute application 0.0449ms
compilation (IR) 0.0652ms
compilation (LCNF base) 0.652ms
compilation (LCNF impure) 0.326ms
compilation (LCNF mono) 0.945ms
congr simp thm 0.634ms
elaboration 18.8ms
fix level params 0.388ms
import 1.32s
initialization 33ms
instantiate metavars 1.08ms
interpretation 245ms
let-to-have transformation 0.0502ms
linting 9.45ms
module linting 0.00127ms
norm_num 0.967ms
overlappingInstancesLinter 3.96ms
parsing 10.9ms
process pre-definitions 3.71ms
share common exprs 1.43ms
simp 17.7ms
tactic execution 172ms
tacticAnalysis 23.2ms
type checking 162ms
typeclass inference 151ms
real 2.53
user 1.89
sys 0.95
LeanPool/RareDistanceFields/BipartiteDiameter.lean
import took 1.3s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.12s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.1s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 2.42s
cumulative profiling times:
attribute application 0.103ms
congr simp thm 6.08ms
dsimp 5.05ms
elaboration 54.1ms
fix level params 1.39ms
import 1.3s
initialization 39.8ms
instantiate metavars 4.35ms
interpretation 5s
let-to-have transformation 0.12ms
linting 24.6ms
module linting 0.00192ms
norm_num 6.69ms
overlappingInstancesLinter 7.17ms
parsing 16.1ms
process pre-definitions 15.7ms
ring 71.9ms
share common exprs 16.7ms
simp 264ms
tactic execution 234ms
tacticAnalysis 39.5ms
type checking 66.9ms
typeclass inference 1.21s
real 7.73
user 8.09
sys 0.96
LeanPool/RareDistanceFields/DistancePattern.lean
import took 1.33s
cumulative profiling times:
attribute application 0.081ms
congr simp thm 1.24ms
dsimp 22.3ms
elaboration 32.7ms
fix level params 0.575ms
import 1.33s
initialization 30ms
instantiate metavars 0.787ms
interpretation 245ms
let-to-have transformation 0.103ms
linting 12.2ms
module linting 0.00154ms
norm_num 1.63ms
overlappingInstancesLinter 4.17ms
parsing 6.94ms
process pre-definitions 3.65ms
share common exprs 1.62ms
simp 16.3ms
tactic execution 66.8ms
tacticAnalysis 16.7ms
type checking 25.3ms
typeclass inference 105ms
real 2.39
user 1.64
sys 0.95
LeanPool/RareDistanceFields/DyadicCoordinates.lean
import took 1.32s
cumulative profiling times:
attribute application 0.252ms
compilation (IR) 0.114ms
compilation (LCNF base) 1.63ms
compilation (LCNF impure) 0.574ms
compilation (LCNF mono) 0.844ms
congr simp thm 2.69ms
dsimp 30.5ms
elaboration 29.4ms
fix level params 0.631ms
import 1.32s
initialization 37.2ms
instantiate metavars 0.828ms
interpretation 284ms
let-to-have transformation 0.103ms
linting 16ms
module linting 0.00136ms
norm_num 10.4ms
overlappingInstancesLinter 3.52ms
parsing 8.09ms
process pre-definitions 9.1ms
ring 23.6ms
share common exprs 6.96ms
simp 64ms
tactic execution 231ms
tacticAnalysis 21.9ms
type checking 312ms
typeclass inference 307ms
real 2.61
user 2.42
sys 0.97
LeanPool/RareDistanceFields/DyadicLevels.lean
import took 1.36s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 160ms
cumulative profiling times:
attribute application 0.044ms
congr simp thm 4.46ms
elaboration 25.8ms
fix level params 0.883ms
import 1.36s
initialization 40.3ms
instantiate metavars 3.89ms
interpretation 500ms
let-to-have transformation 0.0604ms
linting 19.8ms
module linting 0.0015ms
norm_num 4.96ms
overlappingInstancesLinter 3.81ms
parsing 13.6ms
process pre-definitions 7.03ms
ring 19.7ms
share common exprs 7.17ms
simp 71.1ms
tactic execution 277ms
tacticAnalysis 28ms
type checking 159ms
typeclass inference 355ms
real 3.03
user 2.60
sys 0.98
LeanPool/RareDistanceFields/DyadicNorm.lean
import took 1.06s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 331ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 373ms
cumulative profiling times:
attribute application 0.232ms
compilation (IR) 0.0347ms
compilation (LCNF base) 0.591ms
compilation (LCNF impure) 0.138ms
compilation (LCNF mono) 0.183ms
congr simp thm 5.35ms
dsimp 0.886ms
elaboration 36.4ms
fix level params 0.836ms
import 1.06s
initialization 29.7ms
instantiate metavars 6.49ms
interpretation 982ms
let-to-have transformation 0.106ms
linting 15ms
module linting 0.00127ms
norm_num 21.7ms
overlappingInstancesLinter 4.15ms
parsing 11.8ms
process pre-definitions 11.9ms
ring 44.7ms
share common exprs 18ms
simp 204ms
tactic execution 412ms
tacticAnalysis 30.1ms
type checking 473ms
typeclass inference 641ms
real 3.47
user 3.87
sys 0.83
LeanPool/RareDistanceFields/DyadicSize.lean
import took 1.32s
tactic execution of Lean.Parser.Tactic.refine took 848ms
cumulative profiling times:
attribute application 0.0408ms
compilation (IR) 0.0836ms
compilation (LCNF base) 0.891ms
compilation (LCNF impure) 0.4ms
compilation (LCNF mono) 0.871ms
congr simp thm 0.988ms
dsimp 6.41ms
elaboration 14.2ms
fix level params 0.417ms
import 1.32s
initialization 30.3ms
instantiate metavars 1.12ms
interpretation 284ms
let-to-have transformation 0.0453ms
linting 11.4ms
module linting 0.00135ms
norm_num 5.71ms
overlappingInstancesLinter 3.72ms
parsing 9.76ms
process pre-definitions 3.63ms
share common exprs 1.96ms
simp 27.7ms
tactic execution 1.02s
tacticAnalysis 22ms
type checking 170ms
typeclass inference 200ms
real 3.11
user 2.84
sys 0.96
LeanPool/RareDistanceFields/IntegerDivergence.lean
import took 1.32s
cumulative profiling times:
attribute application 0.0923ms
compilation (IR) 0.0969ms
compilation (LCNF base) 0.674ms
compilation (LCNF impure) 0.35ms
compilation (LCNF mono) 0.62ms
congr simp thm 0.39ms
elaboration 32.5ms
fix level params 0.468ms
import 1.32s
initialization 30.6ms
instantiate metavars 0.53ms
interpretation 242ms
let-to-have transformation 0.0823ms
linting 13.4ms
module linting 0.00144ms
overlappingInstancesLinter 5.16ms
parsing 6.84ms
process pre-definitions 2.95ms
share common exprs 1.46ms
simp 5.72ms
tactic execution 87ms
tacticAnalysis 17.7ms
type checking 31.5ms
typeclass inference 84.6ms
real 2.28
user 1.59
sys 0.94
LeanPool/RareDistanceFields/IntegerPlane.lean
import took 1.07s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 118ms
cumulative profiling times:
attribute application 0.14ms
compilation (IR) 0.11ms
compilation (LCNF base) 1.62ms
compilation (LCNF impure) 0.53ms
compilation (LCNF mono) 0.969ms
congr simp thm 0.898ms
dsimp 29ms
elaboration 35.5ms
fix level params 1.46ms
import 1.07s
initialization 30.1ms
instantiate metavars 2.76ms
interpretation 451ms
let-to-have transformation 0.0774ms
linting 16.9ms
module linting 0.00133ms
norm_num 4.3ms
overlappingInstancesLinter 4.43ms
parsing 9.33ms
process pre-definitions 9.68ms
ring 72.6ms
share common exprs 15.7ms
simp 12.7ms
tactic execution 79.6ms
tacticAnalysis 23ms
type checking 48.3ms
typeclass inference 138ms
real 2.35
user 1.84
sys 0.86
LeanPool/RareDistanceFields/OctagonalDescent.lean
import took 1.36s
cumulative profiling times:
attribute application 0.0741ms
elaboration 26.6ms
fix level params 0.0663ms
import 1.36s
initialization 29.6ms
instantiate metavars 0.0735ms
interpretation 203ms
let-to-have transformation 0.0616ms
linting 2.84ms
module linting 0.00126ms
overlappingInstancesLinter 3.6ms
parsing 2.82ms
process pre-definitions 1.28ms
share common exprs 0.23ms
tactic execution 2.48ms
tacticAnalysis 7.94ms
type checking 3.99ms
typeclass inference 8.35ms
real 2.24
user 1.33
sys 0.97
LeanPool/RareDistanceFields/OctagonalNorm.lean
import took 1.33s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 297ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 331ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 233ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 274ms
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 108ms
type checking took 112ms
ring took 257ms
share common exprs took 123ms
type checking took 119ms
cumulative profiling times:
attribute application 0.391ms
blocked (unaccounted) 30.5ms
compilation (IR) 0.286ms
compilation (LCNF base) 4.15ms
compilation (LCNF impure) 1.57ms
compilation (LCNF mono) 2.3ms
congr simp thm 17.4ms
dsimp 132ms
elaboration 206ms
fix level params 8.37ms
import 1.33s
initialization 36.6ms
instantiate metavars 3.36ms
interpretation 2.01s
let-to-have transformation 0.352ms
linting 24ms
module linting 0.0013ms
norm_num 69.3ms
overlappingInstancesLinter 7.29ms
parsing 15.9ms
process pre-definitions 78.2ms
ring 577ms
share common exprs 224ms
simp 320ms
tactic execution 575ms
tacticAnalysis 42.2ms
type checking 929ms
typeclass inference 1.03s
real 4.89
user 7.30
sys 0.98
LeanPool/RareDistanceFields/OctagonalRational.lean
import took 1.38s
cumulative profiling times:
attribute application 0.09ms
congr simp thm 17.2ms
dsimp 1.2ms
elaboration 37.8ms
fix level params 1.07ms
import 1.38s
initialization 35.8ms
instantiate metavars 2.18ms
interpretation 280ms
let-to-have transformation 0.0988ms
linting 19ms
module linting 0.00134ms
norm_num 2.62ms
overlappingInstancesLinter 4.27ms
parsing 10.3ms
process pre-definitions 7.27ms
ring 13.3ms
share common exprs 4.9ms
simp 196ms
tactic execution 266ms
tacticAnalysis 33.2ms
type checking 70.4ms
typeclass inference 390ms
real 2.80
user 2.42
sys 1.00
LeanPool/RareDistanceFields/OrderedColors.lean
import took 1.03s
cumulative profiling times:
aesop 13.6ms
attribute application 0.0842ms
compilation (IR) 0.143ms
compilation (LCNF base) 1.48ms
compilation (LCNF impure) 0.824ms
compilation (LCNF mono) 1.87ms
congr simp thm 1ms
elaboration 34.8ms
fix level params 1.11ms
import 1.03s
initialization 29.6ms
instantiate metavars 1.34ms
interpretation 213ms
let-to-have transformation 0.0999ms
linting 17.1ms
module linting 0.00125ms
overlappingInstancesLinter 5.65ms
parsing 9.42ms
process pre-definitions 5.4ms
share common exprs 2.43ms
simp 17.9ms
tactic execution 113ms
tacticAnalysis 25.7ms
type checking 52.1ms
typeclass inference 131ms
real 2.01
user 1.52
sys 0.81
LeanPool/RareDistanceFields/PolynomialSpecialization.lean
import took 1.34s
cumulative profiling times:
attribute application 0.149ms
blocked (unaccounted) 1.27ms
congr simp thm 3.28ms
dsimp 4.73ms
elaboration 53.8ms
fix level params 1.52ms
import 1.34s
initialization 30.3ms
instantiate metavars 1.52ms
interpretation 368ms
let-to-have transformation 0.155ms
linting 18ms
module linting 0.00152ms
norm_num 2ms
overlappingInstancesLinter 6.03ms
parsing 9.96ms
process pre-definitions 7.2ms
ring 11.6ms
share common exprs 6.08ms
simp 143ms
tactic execution 126ms
tacticAnalysis 26.8ms
type checking 74.5ms
typeclass inference 721ms
real 2.73
user 2.60
sys 0.98
LeanPool/RareDistanceFields/PureTranscendental.lean
import took 1.35s
cumulative profiling times:
attribute application 0.133ms
congr simp thm 4.42ms
elaboration 82.3ms
fix level params 1.14ms
import 1.35s
initialization 29.6ms
instantiate metavars 2.7ms
interpretation 256ms
let-to-have transformation 0.173ms
linting 9.66ms
module linting 0.00161ms
overlappingInstancesLinter 4.47ms
parsing 7.81ms
process pre-definitions 8ms
share common exprs 4.37ms
simp 198ms
tactic execution 231ms
tacticAnalysis 23.8ms
type checking 95.4ms
typeclass inference 1.39s
real 3.71
user 3.40
sys 0.94
LeanPool/RareDistanceFields/RationalDivergence.lean
import took 1.35s
cumulative profiling times:
attribute application 0.131ms
congr simp thm 5.46ms
dsimp 7.61ms
elaboration 43.1ms
fix level params 1.13ms
import 1.35s
initialization 29.9ms
instantiate metavars 1.58ms
interpretation 361ms
let-to-have transformation 0.101ms
linting 25.5ms
module linting 0.00144ms
norm_num 2.05ms
overlappingInstancesLinter 5.08ms
parsing 12.5ms
process pre-definitions 7.67ms
ring 12.6ms
share common exprs 5.96ms
simp 65.5ms
tactic execution 197ms
tacticAnalysis 27.9ms
type checking 59.6ms
typeclass inference 304ms
real 2.58
user 2.18
sys 0.98
LeanPool/RareDistanceFields/RationalPlane.lean
import took 1.33s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 101ms
cumulative profiling times:
attribute application 0.179ms
compilation (IR) 0.0918ms
compilation (LCNF base) 1.79ms
compilation (LCNF impure) 0.452ms
compilation (LCNF mono) 0.733ms
congr simp thm 7.5ms
dsimp 13.1ms
elaboration 59ms
fix level params 2.34ms
import 1.33s
initialization 29.6ms
instantiate metavars 4.2ms
interpretation 627ms
let-to-have transformation 0.136ms
linting 24.7ms
module linting 0.00156ms
norm_num 9.87ms
overlappingInstancesLinter 6.8ms
parsing 14.9ms
process pre-definitions 15.2ms
ring 74.2ms
share common exprs 21.5ms
simp 126ms
tactic execution 159ms
tacticAnalysis 38.6ms
type checking 97.5ms
typeclass inference 417ms
real 2.59
user 2.75
sys 0.94
LeanPool/RareDistanceFields/SplitCounts.lean
import took 1.01s
cumulative profiling times:
attribute application 0.0759ms
blocked (unaccounted) 0.319ms
congr simp thm 2.93ms
elaboration 32.6ms
fix level params 0.707ms
import 1.01s
initialization 30.1ms
instantiate metavars 0.371ms
interpretation 189ms
let-to-have transformation 0.0881ms
linting 6.9ms
module linting 0.00134ms
overlappingInstancesLinter 4.36ms
parsing 6.18ms
process pre-definitions 2.32ms
share common exprs 1.75ms
simp 249ms
tactic execution 33.8ms
tacticAnalysis 17.1ms
type checking 17.4ms
typeclass inference 260ms
real 2.10
user 1.67
sys 0.81
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Vilin97
added
the
needs-maintainer
|
Automated review disposition: needs-maintainer This draft is a complete, internally checked quantitative theorem for configurations restricted to Q(sqrt(2)) and real purely transcendental extensions, with exact head |
|
Automation disposition: needs-maintainer. Reviewed exact current head |
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.  The PR appears safe to merge because no blocking failure remains. FindingsSummary
Reviews (8) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Egor Lyfar | ||
| -/ | ||
| import LeanPool.Erdos132N14.HopfPannwitzGeometry |
There was a problem hiding this comment.
BipartiteDiameter imports and uses internal geometry from the separate Erdos132N14 project, contrary to the repository requirement that pooled projects remain independent. Move the shared geometry into an independent common module so changes to Erdos132N14 do not unnecessarily break this project.
File Used: AGENTS.md (source)
Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
| universe u | ||
|
|
||
| open Classical in | ||
| theorem card_le_pow_of_bound (M : ℕ) : ∀ {V : Type u} [Fintype V] |
There was a problem hiding this comment.
The integer-specific DyadicSize and DyadicLevels inductions duplicate the generic BinarySize and BinaryDescent parity-splitting, halving, valuation, and cardinality proofs. Instantiating BinaryDescent.Model for integer points would leave one canonical implementation and avoid duplicate upgrade work and drift between the two live pipelines.
Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Changes requested at exact head a084d76395031d06e65141a7b1353673b4884c65.
Blocking: insignificant partial progress on an open problem. Erdős problem 132 (erdosproblems.com/132, status open) asks whether, for any n points in the plane, there are two distances occurring at most n times, and whether the number of such distances tends to infinity. This PR proves n ≤ 2^r only for configurations whose coordinates lie in ℚ(√2) or in a real purely transcendental extension ℚ(T):
theorem bounds {σ V : Type*} [Fintype V] :
(∀ x : V → ℂ, Function.Injective x → OctagonalRational.QuadraticCoordinates x →
Fintype.card V ≤ 2 ^ (OctagonalRational.rareDistances x).card) ∧
(∀ (f : PureTranscendental.Functions σ →ₐ[ℚ] ℝ) (x : ...), Function.Injective (PureTranscendental.point f x) →
Fintype.card V ≤ 2 ^ (DistancePattern.rareDistances (PureTranscendental.point f x)).card)That is a restricted-parameter case of the open problem; the card itself says the coordinate restrictions are essential, that no published result states these bounds, and that no new mathematics is claimed. Lean Pool accepts partial progress toward a named open problem only when the intermediate theorem is a recognized standalone result, and the maintainer stated on #359 (2026-09-04) that Lean Pool wants the complete formalization of this problem rather than partial cases. A restricted case with no literature standing does not meet that bar, and it is not accepted as a solution of Erdős 132.
Acceptance condition. Either (a) prove the unrestricted statement for arbitrary real coordinates, or (b) if the restricted bound is a published or otherwise recognized theorem, cite that source and present the project as a formalization of it.
Advisory, not blocking. Greptile's two unresolved threads stand: BipartiteDiameter imports LeanPool.Erdos132N14.HopfPannwitzGeometry, coupling this project to another pooled project, and DyadicSize/DyadicLevels duplicate the generic BinarySize/BinaryDescent spines. CI, the axiom audit, and the profile (135 maxHB, 45 s changed-module build) are fine and are not the blocker.
Vilin97
removed
the
needs-maintainer
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
|
Thank you for the work here, and for the careful scoping in the card. Closing this at the maintainer's decision: Lean Pool prefers completed formalizations, and for Erdős problem 132 that means the unrestricted statement rather than the Q(√2) and Q(T) cases. If you complete the full problem, please open a new PR or ask for this one to be reopened; a complete solution would be very welcome. |
2 participants
This project proves a complete quantitative rare-distance theorem for two explicitly restricted coordinate settings. For n distinct planar points, let r count the positive occurring Euclidean distances realized by at most n unordered pairs. Then n ≤ 2^r for coordinates in Q(sqrt(2)), and separately for coordinates in any real purely transcendental extension Q(T). Consequently there are two rare distances for n ≥ 3 and at least k for n ≥ 2^k.
The proof constructs binary arithmetic descent with an integer height separate from Euclidean distance. Exact rational specialization handles Q(T) while preserving the whole distance-equality pattern. Every bound counts complete unordered classes; no published classification theorem is assumed. The two coordinate regimes are not combined into arbitrary algebraic extensions.
This is a distinct completed restricted project arising from the #132 work. It does not solve unrestricted Erdős #132 or fulfill the full-problem request on #359. The E2 submission stays separate.
The source package contains this complete project and a reproduction patch against pool base
c8ddda0a64f21cb019720cdda48c94354d4091e7. Existing angular-order geometry is reused from LeanPool.Erdos132N14.HopfPannwitzGeometry; the conditional n=14 theorem is not imported. Erdős #132 is the motivating problem, and Woodall/Madore are coloring background, not sources claiming these rare-distance bounds. No mathematical novelty claim is made. Proof provenance is AI.Local validation at
902d0aa05768062df076469a95d15f8ae99732b6:lake exe runLinter LeanPool.RareDistanceFields,lake exe lint-style LeanPool.RareDistanceFields, andlake exe mk_all --checkpassed.The bounded prior-art record covers the existing pool, focused Mathlib code searches, and three semantic LeanSearch queries. Returned results did not match these bounds. This does not establish novelty or exhaust prior formalizations; LeanExplore was unavailable. Ready for review. GitHub CI passed the pool and project builds at
a084d76395031d06e65141a7b1353673b4884c65; Lean Action CI. Significance and novelty review remain pending.