Project: Six distances from the E2 diameter-heptagon pattern - #359
Project: Six distances from the E2 diameter-heptagon pattern#359lyfar wants to merge 43 commits into
Conversation
Source DOI: 10.11650/tjm.18.2014.4030 Certificates: https://github.com/lyfar/erdos132-wei-certificates Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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: 334 maxHeartbeats units across 14 files (3,325 added LOC). Sum of Count-heartbeats wall-clock total: 105.92 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.Erdos132WeiE2.Algebra.BezoutGenerated |
19.00 s |
LeanPool.Erdos132WeiE2.Geometry.Parametrization |
15.00 s |
LeanPool.Erdos132WeiE2.Algebra.Exclusions |
10.00 s |
LeanPool.Erdos132WeiE2.Geometry.Star |
9.70 s |
LeanPool.Erdos132WeiE2.Counting.Endgame |
8.80 s |
Challenge.WeiLiCongGao |
6.70 s |
LeanPool.Erdos132WeiE2.Algebra.Ranges |
6.50 s |
LeanPool.Erdos132WeiE2.Geometry.Basic |
6.20 s |
LeanPool.Erdos132WeiE2.Algebra.G10 |
5.80 s |
LeanPool.Erdos132WeiE2.Algebra.TrigSigns |
4.70 s |
LeanPool.Erdos132WeiE2.Algebra.TanExpressions |
3.60 s |
LeanPool.Erdos132WeiE2.Counting.Assembly |
3.10 s |
Per-file `lean --profile` output
Challenge/WeiLiCongGao.lean
import took 1.43s
Challenge/WeiLiCongGao.lean:42:8: warning: declaration uses `sorry`
cumulative profiling times:
attribute application 0.0113ms
elaboration 12.9ms
fix level params 0.0521ms
import 1.43s
initialization 29.3ms
instantiate metavars 0.0412ms
interpretation 188ms
let-to-have transformation 0.0603ms
linting 1.27ms
module linting 0.00133ms
overlappingInstancesLinter 0.99ms
parsing 1.69ms
process pre-definitions 0.294ms
share common exprs 0.357ms
tacticAnalysis 3.88ms
type checking 1.39ms
typeclass inference 8.23ms
real 2.30
user 1.30
sys 1.03
LeanPool/Erdos132WeiE2.lean
import took 1.72s
cumulative profiling times:
elaboration 0.319ms
import 1.72s
initialization 28.1ms
interpretation 191ms
linting 0.33ms
module linting 0.00125ms
overlappingInstancesLinter 0.181ms
parsing 0.0281ms
tacticAnalysis 0.799ms
real 2.60
user 1.45
sys 1.17
LeanPool/Erdos132WeiE2/Algebra/BezoutGenerated.lean
import took 849ms
elaboration took 101ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 895ms
ring took 233ms
share common exprs took 114ms
type checking took 443ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 878ms
ring took 106ms
type checking took 238ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 748ms
ring took 124ms
type checking took 224ms
cumulative profiling times:
attribute application 0.106ms
congr simp thm 1.64ms
elaboration 651ms
fix level params 17.1ms
import 849ms
initialization 29.7ms
instantiate metavars 2.45ms
interpretation 3.06s
let-to-have transformation 0.448ms
linting 17.5ms
module linting 0.00147ms
norm_num 2.75s
overlappingInstancesLinter 3.75ms
parsing 18.9ms
process pre-definitions 155ms
ring 464ms
share common exprs 234ms
tactic execution 1.27ms
tacticAnalysis 58.4ms
type checking 941ms
typeclass inference 5.74s
real 9.68
user 14.86
sys 0.76
LeanPool/Erdos132WeiE2/Algebra/Exclusions.lean
import took 1.27s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 304ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 607ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 546ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.42s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.37s
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 181ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.5s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.47s
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 123ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.47s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.47s
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 117ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.24s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.07s
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 111ms
cumulative profiling times:
attribute application 0.144ms
compilation (IR) 0.383ms
compilation (LCNF base) 14ms
compilation (LCNF impure) 1.53ms
compilation (LCNF mono) 5.47ms
congr simp thm 4.81ms
dsimp 3.69ms
elaboration 246ms
fix level params 5.1ms
import 1.27s
initialization 29.3ms
instantiate metavars 16.9ms
interpretation 13.7s
let-to-have transformation 0.394ms
linting 135ms
module linting 0.00118ms
norm_num 368ms
overlappingInstancesLinter 4.37ms
parsing 17.8ms
process pre-definitions 44ms
ring 296ms
share common exprs 134ms
simp 56.9ms
tactic execution 390ms
tacticAnalysis 58.9ms
type checking 312ms
typeclass inference 2.75s
real 7.40
user 19.53
sys 0.98
LeanPool/Erdos132WeiE2/Algebra/G10.lean
import took 1.27s
cumulative profiling times:
attribute application 0.0236ms
congr simp thm 2.13ms
elaboration 51.4ms
fix level params 1.07ms
import 1.27s
initialization 29.3ms
instantiate metavars 1.74ms
interpretation 847ms
let-to-have transformation 0.0756ms
linting 18ms
module linting 0.00158ms
norm_num 312ms
overlappingInstancesLinter 1.47ms
parsing 6.27ms
process pre-definitions 12.3ms
ring 93.4ms
share common exprs 23.7ms
simp 16.5ms
tactic execution 131ms
tacticAnalysis 13.7ms
type checking 48.9ms
typeclass inference 451ms
real 3.85
user 3.03
sys 0.93
LeanPool/Erdos132WeiE2/Algebra/Ranges.lean
import took 1.25s
cumulative profiling times:
attribute application 0.0583ms
congr simp thm 0.267ms
elaboration 38.2ms
fix level params 0.417ms
import 1.25s
initialization 40.5ms
instantiate metavars 0.459ms
interpretation 280ms
let-to-have transformation 0.122ms
linting 10.2ms
module linting 0.0013ms
norm_num 25.3ms
overlappingInstancesLinter 1.7ms
parsing 3.2ms
process pre-definitions 3.01ms
ring 21.3ms
share common exprs 4.82ms
simp 1.04ms
tactic execution 8.58ms
tacticAnalysis 12.8ms
type checking 16.6ms
typeclass inference 69.1ms
real 2.31
user 1.47
sys 0.95
LeanPool/Erdos132WeiE2/Algebra/TanExpressions.lean
import took 1.25s
cumulative profiling times:
attribute application 0.0748ms
congr simp thm 0.531ms
elaboration 30.7ms
fix level params 0.63ms
import 1.25s
initialization 28.8ms
instantiate metavars 0.477ms
interpretation 350ms
let-to-have transformation 0.107ms
linting 6.71ms
module linting 0.00133ms
norm_num 43.5ms
overlappingInstancesLinter 1.9ms
parsing 3.93ms
process pre-definitions 4.25ms
ring 41.6ms
share common exprs 6.66ms
simp 1.98ms
tactic execution 33ms
tacticAnalysis 13.8ms
type checking 44.5ms
typeclass inference 148ms
real 2.31
user 1.68
sys 0.94
LeanPool/Erdos132WeiE2/Algebra/TrigSigns.lean
import took 1.25s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 147ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 126ms
cumulative profiling times:
attribute application 0.19ms
congr simp thm 0.897ms
elaboration 118ms
fix level params 1.93ms
import 1.25s
initialization 36.7ms
instantiate metavars 1.96ms
interpretation 772ms
let-to-have transformation 0.358ms
linting 22ms
module linting 0.00153ms
norm_num 122ms
overlappingInstancesLinter 3.72ms
parsing 10.5ms
process pre-definitions 13.4ms
ring 109ms
share common exprs 25.4ms
simp 5.17ms
tactic execution 83.3ms
tacticAnalysis 38.6ms
type checking 112ms
typeclass inference 559ms
real 2.60
user 2.98
sys 0.91
LeanPool/Erdos132WeiE2/Counting/Assembly.lean
import took 1.69s
cumulative profiling times:
attribute application 0.0119ms
congr simp thm 1.63ms
elaboration 32.4ms
fix level params 0.357ms
import 1.69s
initialization 28.6ms
instantiate metavars 0.821ms
interpretation 560ms
let-to-have transformation 0.0871ms
linting 24.5ms
module linting 0.00124ms
norm_num 83.2ms
overlappingInstancesLinter 2.09ms
parsing 11.5ms
process pre-definitions 3.92ms
ring 15.4ms
share common exprs 4.41ms
simp 16.6ms
tactic execution 134ms
tacticAnalysis 24.7ms
type checking 15.2ms
typeclass inference 187ms
real 3.46
user 2.33
sys 1.16
LeanPool/Erdos132WeiE2/Counting/Endgame.lean
import took 1.65s
cumulative profiling times:
attribute application 0.0122ms
congr simp thm 5.21ms
elaboration 11.4ms
fix level params 0.307ms
import 1.65s
initialization 29.5ms
instantiate metavars 1.37ms
interpretation 428ms
let-to-have transformation 0.0247ms
linting 12.9ms
module linting 0.00141ms
norm_num 2.02ms
overlappingInstancesLinter 0.821ms
parsing 3.89ms
process pre-definitions 2.91ms
ring 32.9ms
share common exprs 6.52ms
simp 102ms
tactic execution 57.5ms
tacticAnalysis 11.3ms
type checking 21.5ms
typeclass inference 82ms
real 3.10
user 1.98
sys 1.15
LeanPool/Erdos132WeiE2/Geometry/Basic.lean
import took 1.45s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 226ms
cumulative profiling times:
attribute application 0.15ms
blocked (unaccounted) 0.965ms
compilation (IR) 0.0324ms
compilation (LCNF base) 0.566ms
compilation (LCNF impure) 0.152ms
compilation (LCNF mono) 0.22ms
congr simp thm 0.866ms
elaboration 67ms
fix level params 1.21ms
import 1.45s
initialization 36.9ms
instantiate metavars 11.6ms
interpretation 786ms
let-to-have transformation 0.327ms
linting 16.9ms
module linting 0.00128ms
norm_num 1.88ms
overlappingInstancesLinter 3.46ms
parsing 11.1ms
process pre-definitions 21.3ms
ring 20.8ms
share common exprs 10.3ms
simp 78.6ms
tactic execution 219ms
tacticAnalysis 28.4ms
type checking 203ms
typeclass inference 497ms
real 3.20
user 3.03
sys 1.05
LeanPool/Erdos132WeiE2/Geometry/Parametrization.lean
import took 1.45s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 502ms
simp took 697ms
simp took 334ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 118ms
simp took 106ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 209ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.38s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.34s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 718ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.82s
cumulative profiling times:
attribute application 1.2ms
blocked (unaccounted) 1.63s
compilation (IR) 0.0503ms
compilation (LCNF base) 0.799ms
compilation (LCNF impure) 0.271ms
compilation (LCNF mono) 0.536ms
congr simp thm 12.7ms
elaboration 595ms
fix level params 8.12ms
import 1.45s
initialization 29.7ms
instantiate metavars 16.7ms
interpretation 8.31s
let-to-have transformation 1.25ms
linting 169ms
module linting 0.00135ms
norm_num 599ms
overlappingInstancesLinter 16.6ms
parsing 97ms
process pre-definitions 80.2ms
ring 469ms
share common exprs 135ms
simp 2.06s
tactic execution 2.01s
tacticAnalysis 246ms
type checking 1.08s
typeclass inference 4.83s
real 9.82
user 21.37
sys 1.13
LeanPool/Erdos132WeiE2/Geometry/Star.lean
import took 1.45s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 670ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 614ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 846ms
simp took 413ms
simp took 354ms
simp took 362ms
simp took 353ms
cumulative profiling times:
attribute application 0.282ms
congr simp thm 52.3ms
elaboration 195ms
fix level params 6.34ms
import 1.45s
initialization 29.1ms
instantiate metavars 47.7ms
interpretation 3.73s
let-to-have transformation 0.528ms
linting 101ms
module linting 0.00169ms
norm_num 8.18ms
overlappingInstancesLinter 8.08ms
parsing 55.8ms
process pre-definitions 107ms
ring 159ms
share common exprs 78.6ms
simp 5.17s
tactic execution 1.44s
tacticAnalysis 127ms
type checking 443ms
typeclass inference 3.14s
real 7.27
user 15.84
sys 1.12
Solution/WeiLiCongGao.lean
import took 1.71s
cumulative profiling times:
attribute application 0.0141ms
elaboration 13.7ms
fix level params 0.0545ms
import 1.71s
initialization 33.8ms
instantiate metavars 0.081ms
interpretation 213ms
let-to-have transformation 0.0562ms
linting 1.92ms
module linting 0.00139ms
overlappingInstancesLinter 0.713ms
parsing 3.05ms
process pre-definitions 0.565ms
share common exprs 0.436ms
tactic execution 15ms
tacticAnalysis 6.48ms
type checking 2.82ms
typeclass inference 11.7ms
real 2.64
user 1.49
sys 1.18
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reviewed exact draft head 05e2268d8e26a07acfb8149422f04d8e0317a561.
The comparator check is green and the proof profile is reasonable for a 3,325-LOC development (334 maxHB; 55.19 s changed-module wall time), but this head cannot be accepted in its current shape:
- It adds
Challenge/WeiLiCongGao.leanand the matchingSolution/in one PR. Under the solution rules, a solution must not touch the challenge statement it claims to solve. The maintainer has also directed that this already-solved result be submitted as a project rather than an open challenge. - Exact-head Lean Action CI fails because the project emits repository-blocking warnings: misplaced module docstrings in
Ranges.lean,TrigSigns.lean,TanExpressions.lean, andEndgame.lean, plus the broadimport Mathlib.TacticinEndgame.lean. - The pooled project currently leaves the final theorem with the original geometric hypotheses only in
Solution/WeiLiCongGao.lean; its registered headline is the conditionalsix_distances_of_parametrization. A project-only revision should expose and register the final E2 theorem in the pooled project itself.
Please convert this to a ready-for-review pooled-project PR, remove the challenge/solution lifecycle changes, fix all warning-producing imports/docstrings, expose the final E2 theorem as a project result, and obtain green required CI. Keep the card explicit that this is the independently significant repaired E2 step; it does not completely solve Erdős problem 132.
|
Supplement to the current-head changes request: the DOI metadata and paper itself list the authors of 10.11650/tjm.18.2014.4030 as Xianglin Wei, Guogang Li, Yue Cong, and Feixing Gao. This PR records Zhengyu Li, Meiqin Cong, and Yan Gao after the first author. Please correct the source attribution in the registry/project card when converting this result to a pooled project. Authoritative DOI metadata: https://api.crossref.org/works/10.11650/tjm.18.2014.4030 |
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
lyfar
changed the title
|
Converted per your review — now a pooled-project-only PR at merged head 69d002e: lifecycle changes reverted, final geometric theorem exposed and registered as the headline, docstring/import warnings fixed, author attribution corrected per Crossref. Details in the updated PR body. |
Greptile SummaryThe PR adds a pooled Lean formalization proving that the specified E2 diameter-heptagon pattern realizes at least six distinct pairwise distances.
|
| Filename | Overview |
|---|---|
| LeanPool/Erdos132WeiE2/Algebra/BezoutGenerated.lean | Adds the generated Bézout cofactors and kernel-checked polynomial identities, with the previously requested pinned provenance. |
| LeanPool/Erdos132WeiE2/Final.lean | Exposes the geometric E2 six-distance result as the project’s final theorem. |
| LeanPool/Erdos132WeiE2/Counting/Assembly.lean | Connects geometric distance values, algebraic collision exclusions, and the finite counting argument. |
| LeanPool/projects.yml | Registers the project, source metadata, attribution, provenance, and headline declaration. |
Reviews (13): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All three registered results match their informal statements, and their geometric and parametric assumptions are disclosed. |
| Novelty | ✅ pass |
The Mathlib searches and pool inventory contain no declaration proving any of the three headline results. |
| Significance | ✅ pass |
This is a research-level discrete-geometry project with a substantive headline theorem in the Erdős 132 program and a complete geometric-to-algebraic development. |
| Sources | ✅ pass |
The citation is internally consistent and the repaired E2 variant is clearly labelled, but the paper’s exact case analysis is not independently verifiable from the diff. |
| Code quality (advisory) | ✅ pass |
The proof is well-factored across geometry, algebra, and counting, with localized debt in one expanded finite enumeration and three duplicate order wrappers. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | The headline assumes hdiam, hshort, the four boundary-class equalities, and the strict class ordering hBA and hAC; the card discloses these as the step-three diameter graph and ordered boundary edge classes. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | discrete geometry |
| Mode | mixed |
| Code quality | 4 / 5 |
Statement check: The headline proves that any seven planar points with exactly the stated step-three unit-diameter pattern and boundary classes B < A < C have at least six distinct distances; the two supporting declarations provide exactly the claimed parametrization and conditional counting result.
The project proves that seven planar points with the unit step-three diameter-cycle pattern and ordered boundary-edge classes realize at least six distinct pairwise distances.
Code quality findings (2)
-
agent-slop —
LeanPool/Erdos132WeiE2/Geometry/Star.lean:306
fin_four_partition_casesexpands the finite enumeration into sixteen hand-written branches and repeats the same complement calculation in every non-diagonal branch. Replace it with exhaustive case splitting followed bysimpordecide, or factor the repeated complement proof into a helper.
Evidence: private theorem fin_four_partition_cases
(i j k l : Fin 4) (hji : j ≠ i)
(hcomp : ({k, l} : Set (Fin 4)) = ({i, j} : Set (Fin 4))ᶜ) :fin_cases i
· fin_cases j
· exact (hji rfl).elim
· exact Or.inl (Or.inl ⟨rfl, hcomp.trans (by
ext m
fin_cases m <;> decide)⟩)
· exact Or.inr (Or.inl (Or.inl ⟨rfl, hcomp.trans (by
ext m
fin_cases m <;> decide)⟩))
· exact Or.inr (Or.inr (Or.inl ⟨by simp, hcomp.trans (by
ext m
fin_cases m <;> decide)⟩)) -
duplicate-definition —
LeanPool/Erdos132WeiE2/Algebra/TrigSigns.lean:134
ra_gt_ea,rb_gt_eb, andra_gt_rbare alpha-renamed copies of the same square-order conversion, already expressed bylt_of_sq_lt_sq_of_nonneg. Use that generic lemma directly at the three call sites to avoid redundant API names.
Evidence: lemma ra_gt_ea {RA eA : ℝ} (hsq : eA ^ 2 < RA ^ 2)
(hRA : 0 ≤ RA) (heA : 0 ≤ eA) : eA < RA :=
lt_of_sq_lt_sq_of_nonneg hsq heA hRA
lemma rb_gt_eb {RB eB : ℝ} (hsq : eB ^ 2 < RB ^ 2)
(hRB : 0 ≤ RB) (heB : 0 ≤ eB) : eB < RB :=
lt_of_sq_lt_sq_of_nonneg hsq heB hRB
lemma ra_gt_rb {RA RB : ℝ} (hsq : RB ^ 2 < RA ^ 2)
(hRA : 0 ≤ RA) (hRB : 0 ≤ RB) : RB < RA :=
lt_of_sq_lt_sq_of_nonneg hsq hRB hRA
Tokens: 305,917 in / 22,710 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $1.1054
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.
…module bezout_cofactors.py (cofactor derivation + verification), cofactors.json (exact cofactors, schema e2-bezout-cofactors-v1), generate_bezout_lean.py (Lean renderer, provenance string parametrized via --source). Answers the reproducibility finding on Vilin97/lean-pool#359. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Generation inputs and both generators are now published at theorem4-2014/bezout-lean/ in lyfar/erdos132-wei-certificates @ 34bc87ff0; docstrings cite that pin instead of a private workspace path. Answers the Greptile reproducibility finding. Generated file, byte-reproducible via generate_bezout_lean.py (see the directory README). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
All three review findings addressed in ab22212:
Gates re-run green on the new head: warning-free build, |
Maintainer decision requiredReviewed exact head This is a partial-result PR. It does not completely solve Erdős problem 132, and the card/docstring now say so. The intermediate theorem is independently significant: it supplies a kernel-checked repair of the published E2 diameter-heptagon case, from the original geometric hypotheses, in a 3.2k-line discrete-geometry development. The remaining boundary is a genuine maintenance/provenance judgment. The exact-head quality review rates the project 3/5 and identifies duplicated public interfaces ( Quality evidence: #359 (comment) |
Vilin97
added
the
needs-maintainer
# Conflicts: # LeanPool/projects.yml
|
Round-two findings addressed in f7f3b8b, plus the companion-repo items:
Gates green on the new head; the six-distance headline statement is byte-identical (receipt in the project record) and its axioms remain |
# Conflicts: # LeanPool/projects.yml
|
May I ask that you fully formalize this Erdos problem and then submit the PR? I want Lean Pool to contain finished formalizations rather than partial. |
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
2 participants
Project: Six distances from the E2 diameter-heptagon pattern
Reworked from the challenge+solution pair (#358) into a single pooled project.
What this is
The repaired E2 step of Wei–Li–Cong–Gao 2014 (doi:10.11650/tjm.18.2014.4030, Thm 4, Part III,
Case 2), formalized: seven planar points whose unit-distance diameter graph is the step-three
7-cycle, with boundary edge classes ordered B < A < C, realize at least six distinct pairwise
distances. It is independently significant but does not completely solve Erdős problem 132.
Exact-arithmetic companion: github.com/lyfar/erdos132-wei-certificates.
Headline:
LeanPool.Erdos132WeiE2.e2_pattern_six_distances(original geometric hypotheses).Addressing the review
Challenge/WeiLiCongGao.lean,Solution/,Challenge/challenges.yml, and theChallenge.lean/Solution.leanindex lines areback to
main. Diff vsmainis now project-only (LeanPool/Erdos132WeiE2/**,LeanPool.lean,LeanPool/projects.yml).LeanPool/Erdos132WeiE2/Final.leanand registered it asmain_declarations;six_distances_of_parametrizationis now a supporting result only.Ranges.lean,TrigSigns.lean,TanExpressions.lean,Endgame.lean;import Mathlib.TacticinEndgame.leanreplaced with thespecific tactic imports it uses. Clean rebuild of the cone is warning-free.
runLinter,lint-style, and the quality gate pass; project issorry/admit/unsafe/partial-free;
#print axiomsof the headline is[propext, Classical.choice, Quot.sound].mainsync-merges are kept and mergedthrough (never rebased); whole-pool
lake build LeanPoolpasses with the newly merged projects.projects.ymlnow lists the Crossref-authoritative authors fordoi:10.11650/tjm.18.2014.4030 — Xianglin Wei, Guogang Li, Yue Cong, Feixing Gao.
Source verification
Wei–Li–Cong–Gao 2014, Distance sets with diameter graph being cycle, Taiwanese J. Math. 18(6),
publisher open-access PDF:
https://projecteuclid.org/journals/taiwanese-journal-of-mathematics/volume-18/issue-6/DISTANCE-SETS-WITH-DIAMETER-GRAPH-BEING-CYCLE/10.11650/tjm.18.2014.4030.pdf.
The repaired case lives in the proof of Theorem 4, Part III, Case 2 (pp. 1983–1984): the text
excludes
d(6,7) = d₃for the one still-free boundary edge and handles the two remaining valuesby a "the proof is similar" appeal; E2 is the
d(6,7) = d₄branch of that appeal. Withd(6,7) = d₄the seven boundary edges read, in the paper's vertex order,(d₃, d₅, d₅, d₃, d₄, d₄, d₄)— after the 1-based → 0-based index shift exactly this project'spattern
(C, B, B, C, A, A, A)withC = d₃,A = d₄,B = d₅, andB < A < Cis the paper'sstanding
d₃ > d₄ > d₅.Honest scope
The pooled result is the repaired E2 case, not a full solution of Erdős 132.