Import sharp sphere-packing asymptotics - #391
Open
Vilin97 wants to merge 7 commits into
Open
Conversation
Greptile SummaryThe PR imports a sharp high-dimensional sphere-packing formalization, splits its implementation into eight dependency-ordered modules, and exposes unrestricted Cohn–Elkies asymptotics together with the sphere-packing upper-bound bridge.
|
| Filename | Overview |
|---|---|
| LeanPool/SpherePacking.lean | Adds the project entry point, source metadata, attribution, and a focused import of the conclusion module. |
| LeanPool/SpherePacking/Conclusion.lean | Defines the unrestricted admissible-function interface, proves radialization preserves the quotient, exposes the asymptotic conclusions, and bridges them to sphere-packing density. |
| LeanPool/SpherePacking/Foundations.lean | Supplies the foundational radial Cohn–Elkies definitions and analytic infrastructure used by the dependency chain. |
| LeanPool/SpherePacking/PackingBound.lean | Completes the packing-bound layer consumed by the public conclusion module. |
| LeanPool/projects.yml | Registers the source revision, provenance, license, entry module, and exact principal theorem declarations. |
| LeanPool.lean | Adds the SpherePacking entry point and implementation modules to the repository umbrella import. |
Reviews (7): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile
Contributor
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: 31,377 maxHeartbeats units across 9 files (56,368 added LOC). Sum of Count-heartbeats wall-clock total: 520.89 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.SpherePacking.PackingBound |
35.00 s |
LeanPool.SpherePacking.Foundations |
31.00 s |
LeanPool.SpherePacking.HarmonicAnalysis |
29.00 s |
LeanPool.SpherePacking.MellinAnalysis |
28.00 s |
LeanPool.SpherePacking.RadialConstruction |
26.00 s |
LeanPool.SpherePacking.GammaAnalysis |
25.00 s |
LeanPool.SpherePacking.SaddleAnalysis |
22.00 s |
LeanPool.SpherePacking.Conclusion |
11.00 s |
LeanPool.SpherePacking |
8.40 s |
Per-file `lean --profile` output
LeanPool/SpherePacking.lean
import took 1.91s
cumulative profiling times:
elaboration 0.329ms
import 1.91s
initialization 29.7ms
interpretation 231ms
linting 0.416ms
module linting 0.00128ms
overlappingInstancesLinter 0.945ms
parsing 0.074ms
tacticAnalysis 1.4ms
real 2.85
user 1.60
sys 1.25
LeanPool/SpherePacking/Conclusion.lean
import took 1.41s
typeclass inference of NonUnitalRing took 557ms
typeclass inference of ContinuousAdd took 161ms
type checking took 139ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 103ms
tactic execution of Lean.Parser.Tactic.apply took 259ms
type checking took 106ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 203ms
typeclass inference of CompleteSpace took 147ms
tactic execution of Lean.Parser.Tactic.exact took 700ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 101ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 164ms
type checking took 108ms
tactic execution of Lean.Parser.Tactic.change took 113ms
interpretation of Real._aux_Mathlib_Analysis_Real_Pi_Bounds___elabRules_Real_tacticPi_lower_bound[_,,]_1._boxed took 199ms
interpretation of Real._aux_Mathlib_Analysis_Real_Pi_Bounds___elabRules_Real_tacticPi_upper_bound[_,,]_1._boxed took 200ms
cumulative profiling times:
attribute application 8.06ms
blocked (unaccounted) 3.63s
compilation (IR) 15.3ms
compilation (LCNF base) 182ms
compilation (LCNF impure) 66.1ms
compilation (LCNF mono) 96ms
congr simp thm 19.1ms
dsimp 38.4ms
elaboration 1.55s
fix level params 14.7ms
import 1.41s
initialization 29.2ms
instantiate metavars 10.6ms
interpretation 2.91s
let-to-have transformation 74.1ms
linting 153ms
module linting 0.00128ms
norm_num 1.54s
overlappingInstancesLinter 32ms
parsing 138ms
process pre-definitions 194ms
ring 97.9ms
share common exprs 136ms
simp 462ms
tactic execution 4.87s
tacticAnalysis 267ms
type checking 2.6s
typeclass inference 13s
real 12.05
user 29.34
sys 1.16
LeanPool/SpherePacking/Foundations.lean
import took 1.33s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 130ms
typeclass inference of MeasureTheory.NullSingletonClass took 121ms
typeclass inference of MeasureTheory.NullSingletonClass took 137ms
typeclass inference of MeasureTheory.NullSingletonClass took 134ms
typeclass inference of MeasureTheory.NullSingletonClass took 136ms
typeclass inference of MeasureTheory.NullSingletonClass took 129ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 124ms
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 107ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 112ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 110ms
simp took 100ms
simp took 155ms
simp took 102ms
simp took 153ms
cumulative profiling times:
aesop 33.6ms
attribute application 7.08ms
blocked (unaccounted) 11.9s
compilation (IR) 0.0672ms
compilation (LCNF base) 0.814ms
compilation (LCNF impure) 0.3ms
compilation (LCNF mono) 0.584ms
congr simp thm 90.9ms
dsimp 227ms
elaboration 2.79s
fix level params 43.7ms
import 1.33s
initialization 32.8ms
instantiate metavars 70ms
interpretation 13.3s
let-to-have transformation 8.94ms
linting 752ms
module linting 0.00162ms
norm_num 1.87s
overlappingInstancesLinter 83ms
parsing 624ms
process pre-definitions 518ms
ring 1.25s
share common exprs 506ms
simp 3.14s
tactic execution 10.2s
tacticAnalysis 1.19s
type checking 4.48s
typeclass inference 28.7s
real 21.87
user 70.11
sys 1.59
LeanPool/SpherePacking/GammaAnalysis.lean
import took 1.41s
tactic execution of Lean.Parser.Tactic.change took 240ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 101ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 113ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 153ms
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 121ms
tactic execution of Mathlib.Tactic.linarith took 107ms
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 292ms
simp took 198ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 174ms
cumulative profiling times:
aesop 115ms
attribute application 4.19ms
blocked (unaccounted) 273ms
compilation (IR) 0.421ms
compilation (LCNF base) 4.36ms
compilation (LCNF impure) 1.82ms
compilation (LCNF mono) 3.34ms
congr simp thm 63.9ms
dsimp 370ms
elaboration 2.18s
fix level params 52.6ms
import 1.41s
initialization 38.5ms
instantiate metavars 86.1ms
interpretation 17.2s
let-to-have transformation 5.45ms
linting 788ms
module linting 0.00128ms
norm_num 4.09s
overlappingInstancesLinter 72ms
parsing 547ms
process pre-definitions 548ms
ring 2.16s
share common exprs 738ms
simp 2.4s
tactic execution 11.4s
tacticAnalysis 1.07s
type checking 3.99s
typeclass inference 21.1s
real 21.42
user 69.68
sys 1.30
LeanPool/SpherePacking/HarmonicAnalysis.lean
import took 1.4s
simp took 457ms
simp took 199ms
simp took 146ms
simp took 185ms
simp took 125ms
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 185ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 250ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 128ms
tactic execution of Mathlib.Tactic.linarith took 179ms
tactic execution of Mathlib.Tactic.linarith took 101ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 135ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 113ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 109ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 159ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.46s
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 112ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 747ms
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 105ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 393ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 114ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 103ms
tactic execution of Mathlib.Tactic.linarith took 143ms
tactic execution of Mathlib.Tactic.linarith took 218ms
tactic execution of Mathlib.Tactic.RingNF.ringNF took 117ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 177ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 988ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 2.03s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 119ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 123ms
simp took 114ms
cumulative profiling times:
aesop 58.3ms
attribute application 2.32ms
blocked (unaccounted) 17.7s
compilation (IR) 0.148ms
compilation (LCNF base) 1.45ms
compilation (LCNF impure) 0.617ms
compilation (LCNF mono) 1.13ms
congr simp thm 84.2ms
dsimp 912ms
elaboration 2.79s
fix level params 47ms
import 1.4s
initialization 39.6ms
instantiate metavars 113ms
interpretation 27.6s
let-to-have transformation 5.03ms
linting 721ms
module linting 0.00131ms
norm_num 8.3s
overlappingInstancesLinter 58.6ms
parsing 508ms
process pre-definitions 552ms
ring 2.29s
share common exprs 797ms
simp 3.05s
tactic execution 12.2s
tacticAnalysis 1.09s
type checking 3s
typeclass inference 23s
real 25.28
user 87.78
sys 1.34
LeanPool/SpherePacking/MellinAnalysis.lean
import took 1.42s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 120ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 344ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 284ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 157ms
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 129ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 802ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 377ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 240ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 127ms
tactic execution of Lean.Parser.Tactic.refine took 259ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 412ms
cumulative profiling times:
aesop 122ms
attribute application 6.45ms
blocked (unaccounted) 873ms
compilation (IR) 0.455ms
compilation (LCNF base) 4.34ms
compilation (LCNF impure) 1.82ms
compilation (LCNF mono) 3.23ms
congr simp thm 95.4ms
dsimp 321ms
elaboration 2.68s
fix level params 50.8ms
import 1.42s
initialization 29.5ms
instantiate metavars 99.2ms
interpretation 19.7s
let-to-have transformation 12.3ms
linting 915ms
module linting 0.00139ms
norm_num 4.83s
overlappingInstancesLinter 83.7ms
parsing 636ms
process pre-definitions 571ms
ring 1.99s
share common exprs 710ms
simp 2.54s
tactic execution 11.6s
tacticAnalysis 1.29s
type checking 4.27s
typeclass inference 22.2s
real 22.68
user 75.36
sys 1.39
LeanPool/SpherePacking/PackingBound.lean
import took 1.44s
typeclass inference of MeasureTheory.VAddInvariantMeasure took 182ms
typeclass inference of MeasureTheory.VAddInvariantMeasure took 115ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 278ms
elaboration took 160ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 114ms
typeclass inference of Neg took 102ms
simp took 342ms
simp took 351ms
typeclass inference of Neg took 109ms
typeclass inference of Neg took 106ms
typeclass inference of Neg took 113ms
typeclass inference of Neg took 107ms
typeclass inference of Neg took 108ms
typeclass inference of MeasureTheory.VAddInvariantMeasure took 180ms
typeclass inference of Neg took 115ms
simp took 339ms
simp took 184ms
simp took 153ms
simp took 201ms
simp took 706ms
tactic execution of Lean.Parser.Tactic.refine took 242ms
simp took 147ms
simp took 149ms
simp took 148ms
simp took 140ms
tactic execution of Lean.Parser.Tactic.obtain took 137ms
simp took 693ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 145ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 141ms
typeclass inference of CharZero took 231ms
simp took 676ms
simp took 140ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 102ms
typeclass inference of Nonempty took 125ms
simp took 737ms
typeclass inference of Nonempty took 117ms
simp took 782ms
typeclass inference of Neg took 103ms
typeclass inference of Neg took 107ms
typeclass inference of NeZero took 107ms
elaboration took 166ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 116ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 194ms
type checking took 101ms
elaboration took 141ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 114ms
typeclass inference of Nonempty took 122ms
simp took 685ms
simp took 191ms
simp took 583ms
simp took 781ms
elaboration took 136ms
simp took 1.3s
simp took 1.15s
cumulative profiling times:
attribute application 19.9ms
blocked (unaccounted) 1.32s
compilation (IR) 0.295ms
compilation (LCNF base) 2.04ms
compilation (LCNF impure) 1.18ms
compilation (LCNF mono) 2.04ms
congr simp thm 174ms
dsimp 49.3ms
elaboration 6.42s
fix level params 34.2ms
grind 64.3ms
grind cutsat 0.0667ms
grind linarith 0.396ms
grind mark subsingleton 17.9ms
grind ring 0.0706ms
grind simp 21.3ms
import 1.44s
initialization 41.2ms
instantiate metavars 95.5ms
interpretation 7.96s
let-to-have transformation 240ms
linting 689ms
module linting 0.00144ms
norm_num 415ms
overlappingInstancesLinter 126ms
parsing 496ms
process pre-definitions 477ms
ring 169ms
share common exprs 299ms
simp 17s
sym canon 81ms
sym typeclass inference 289ms
tactic execution 15.3s
tacticAnalysis 1.28s
type checking 5.51s
typeclass inference 38.8s
real 31.32
user 96.76
sys 1.51
LeanPool/SpherePacking/RadialConstruction.lean
import took 1.36s
tactic execution of Mathlib.Tactic.normNum took 139ms
tactic execution of Lean.Parser.Tactic.exact took 121ms
interpretation of Mathlib.Meta.Positivity.evalFinsetSum._lam_3._boxed took 110ms
interpretation of Mathlib.Meta.Positivity.evalAdd._lam_0._boxed took 150ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 134ms
tactic execution of Mathlib.Tactic.nlinarith took 501ms
simp took 137ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 252ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 105ms
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 109ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 359ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 429ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 107ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 2s
tactic execution of Mathlib.Tactic.nlinarith took 186ms
tactic execution of Mathlib.Tactic.linarith took 118ms
tactic execution of Mathlib.Tactic.linarith took 117ms
tactic execution of Mathlib.Tactic.linarith took 138ms
tactic execution of Mathlib.Tactic.FieldSimp.fieldSimp took 111ms
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 139ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 247ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 232ms
cumulative profiling times:
aesop 38ms
attribute application 3.64ms
blocked (unaccounted) 28.1s
compilation (IR) 0.0688ms
compilation (LCNF base) 0.668ms
compilation (LCNF impure) 0.32ms
compilation (LCNF mono) 0.501ms
congr simp thm 87.9ms
dsimp 606ms
elaboration 2.58s
fix level params 42ms
import 1.36s
initialization 29.7ms
instantiate metavars 95.1ms
interpretation 19.4s
let-to-have transformation 7.27ms
linting 733ms
module linting 0.00143ms
norm_num 4.6s
overlappingInstancesLinter 73.4ms
parsing 524ms
process pre-definitions 506ms
ring 1.77s
share common exprs 619ms
simp 2.65s
tactic execution 14.5s
tacticAnalysis 1.12s
type checking 3.24s
typeclass inference 18.2s
real 21.79
user 71.88
sys 1.36
LeanPool/SpherePacking/SaddleAnalysis.lean
import took 1.37s
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 158ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 184ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 121ms
simp took 228ms
simp took 137ms
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 100ms
simp took 106ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 100ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 311ms
tactic execution of Mathlib.Tactic.FieldSimp.fieldSimp took 203ms
simp took 131ms
cumulative profiling times:
attribute application 12.2ms
blocked (unaccounted) 1.61s
congr simp thm 65.4ms
dsimp 309ms
elaboration 2.51s
fix level params 42.8ms
import 1.37s
initialization 35.9ms
instantiate metavars 74.3ms
interpretation 13.7s
let-to-have transformation 7.66ms
linting 743ms
module linting 0.00118ms
norm_num 2.19s
overlappingInstancesLinter 65.7ms
parsing 499ms
process pre-definitions 463ms
ring 1.57s
share common exprs 578ms
simp 2.85s
tactic execution 9.07s
tacticAnalysis 1.03s
type checking 3.16s
typeclass inference 17.2s
real 17.54
user 56.74
sys 1.27
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Contributor
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | 🤔 discuss |
The visible headline statements match the card, but this review is based on a partial diff and the elided Foundations and MellinAnalysis bodies prevent a complete assumption audit. |
| Novelty | ✅ pass |
Based on the partial diff, none of the four headline results is already formalized in Mathlib or the pool. |
| Significance | ✅ pass |
Based on the partial diff, this is a research-level theory-building project centered on named sharp Cohn–Elkies sphere-packing asymptotics. |
| Sources | ✅ pass |
Based on the partial diff, the canonical revision and prior formalization contributions are credited consistently, but the cited repository’s contents are not present to verify its mathematical claims. |
| Code quality (advisory) | 🤔 discuss |
Based on a partial diff, the visible Lean has enough maintainability debt—duplicate admissibility encodings and plus/minus proof families, a fake parameter dependency, and residual imports and scaffolding—to require human review before merge. |
| Aspect | Value |
|---|---|
| Proves the claim | ➖ unverifiable |
| Assumed, not proved | The visible headline theorems take no hypotheses, but bundled or postulated content in the elided bodies of LeanPool/SpherePacking/Foundations.lean and LeanPool/SpherePacking/MellinAnalysis.lean cannot be ruled out from this partial diff. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | discrete geometry and harmonic analysis |
| Mode | theory_building |
| Code quality | 2 / 5 |
Statement check: The visible endpoints state both unrestricted-program limits, an upper bound on SpherePackingConstant d in every positive dimension with a vanishing error, and an unconditional witness of the packaged sharp conclusions.
The contribution proves sharp root and logarithmic asymptotics for the unrestricted Cohn–Elkies linear program, relates it to the radial program by symmetrization, and derives an asymptotic upper bound for sphere-packing density.
Code quality findings (5)
- import-residue — PR-wide
The module headers directly depend on off-domain algebraic-topology, ring-theory, coalgebra, and sheaf libraries. In the fully visiblePackingBound.lean, the coalgebra import is disconnected from the packing, lattice, measure, and Fourier declarations; the retained headers of the two elided modules show the same pattern. Run module-local import minimization and remove direct imports not required by elaboration.
Evidence: LeanPool/SpherePacking/Foundations.lean importsimport Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected,import Mathlib.RingTheory.WittVector.IsPoly, andimport Std.Tactic.BVDecide.Normalize.Prop. LeanPool/SpherePacking/MellinAnalysis.lean importsimport Mathlib.RingTheory.Etale.Weakly,import Mathlib.RingTheory.PiTensorProduct,import Mathlib.RingTheory.TotallySplit, andimport Mathlib.Topology.Sheaves.Presheaf. LeanPool/SpherePacking/PackingBound.lean importsimport Mathlib.RingTheory.Coalgebra.CoassocSimps. - duplicate-definition —
LeanPool/SpherePacking/Conclusion.lean:214
FullAdmissibleandSpherePacking.Alternative.IsUnrestrictedAdmissibleencode the same unrestricted admissibility conditions in bundled and predicate forms, followed by a field-for-field adapter. This creates two representations that must remain synchronized. State the radialization development against one shared predicate or directly againstFullAdmissible.
Evidence: The public representation starts withstructure FullAdmissible (d : ℕ) where function : CohnElkies.TestFunction d real : ∀ x : CohnElkies.Euclidean d, (function x).im = 0 fourier_real : ∀ x : CohnElkies.Euclidean d, ((𝓕 function) x).im = 0. The second representation isprivate structure IsUnrestrictedAdmissible {d : ℕ} (f : Schwartz d) : Prop where real_valued : IsRealValued f fourier_real_valued : IsRealValued (𝓕 f : Schwartz d) fourier_zero_pos : 0 < fourierReal f 0 fourier_nonneg : ∀ x, 0 ≤ fourierReal f x eventually_nonpos : ∀ x : Ambient d, 1 ≤ ‖x‖ → (f x).re ≤ 0. The duplication is exposed byprivate theorem FullAdmissible.toAlternative {d : ℕ} (f : FullAdmissible d) : SpherePacking.Alternative.IsUnrestrictedAdmissible f.function where real_valued := f.real fourier_real_valued := f.fourier_real fourier_zero_pos := f.fourier_zero_pos fourier_nonneg := f.fourier_nonneg eventually_nonpos := f.outside_nonpos. - unused-parameter —
LeanPool/SpherePacking/SaddleAnalysis.lean:154
saddleSmallRadiusStarOrdinateis independent ofε; the dummy local only manufactures a false dependency. Remove theεparameter and update its private consumers.
Evidence: private noncomputable def saddleSmallRadiusStarOrdinate (ε : ℝ) (d : ℕ) : ℝ :=
let _sourceParameter : ℝ := ε
show ℝ from
-1 + Real.log ((d : ℝ) / 2) /
(4 * ((d : ℝ) / 2)) - duplicate-proof — PR-wide
The implementation repeatedly proves plus/minus variants by copying the same proof and changing only the profile or polynomial. This occurs inplusSaddleFunction_contDiff_nat/minusSaddleFunction_contDiff_nat, the outer-difference and Schwartz constructions inSaddleAnalysis.lean, and the weighted, difference, and central-window polynomial lemmas inHarmonicAnalysis.lean. Introduce a private parameter package for the polynomial/profile/residue data and instantiate one generic proof for the two signs.
Evidence: Both copied smoothness proofs begin identically apart from the function name:
private theorem plusSaddleFunction_contDiff_nat {ε : ℝ} (hε : 0 < ε) {d : ℕ} (hd : 0 < d) (horder : (ε ^ 3) ≤ (10 * Real.log (1 / ε))) (n : ℕ) : ContDiff ℝ n (plusSaddleFunction ε d) := by have hdimension : 0 < (d : ℝ) / 2 := div_pos (by exact_mod_cast hd) (by norm_num) apply contDiff_iff_contDiffAt.mpr intro x by_cases hx : x = 0
and
private theorem minusSaddleFunction_contDiff_nat {ε : ℝ} (hε : 0 < ε) {d : ℕ} (hd : 0 < d) (horder : (ε ^ 3) ≤ (10 * Real.log (1 / ε))) (n : ℕ) : ContDiff ℝ n (minusSaddleFunction ε d) := by have hdimension : 0 < (d : ℝ) / 2 := div_pos (by exact_mod_cast hd) (by norm_num) apply contDiff_iff_contDiffAt.mpr intro x by_cases hx : x = 0. - agent-slop — PR-wide
Several empty sections and namespaces remain from the source split. They provide no scoping or declarations and obscure the already deep section structure. Remove all empty scaffolding together.
Evidence: LeanPool/SpherePacking/PackingBound.lean contains `section Disjoint_Covering_of_Centers
end Disjoint_Covering_of_Centersandsection Complex_Function_Helpers
end Complex_Function_Helpers. LeanPool/SpherePacking/Conclusion.lean contains namespace SpherePacking.Alternative
end SpherePacking.Alternative`.
Tokens: 2,826,688 in / 15,743 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $14.4877
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.
Owner
Author
|
/review |
Contributor
|
LLM review skipped: Lean Action CI conclusion was |
Vilin97
added
the
needs-maintainer
Owner
Author
|
Automation disposition: needs-maintainer Reviewed exact head 11bc329 after a verified repair pass that removed the brittle ten-field repackaging, duplicate averaging/continuity definitions, and unused assumptions; both affected modules build. The project is still only partially reviewable at this size, including elided foundational and Mellin modules, so a maintainer must decide whether the remaining 56k-line import meets the 4/5 bar. |
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
privateProvenance
The canonical source is
openai/ten-proofs@94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6. The migration also incorporates Dean Cureton's independent optimization work from revision30c21d72a2ee3308d66c945387729d736e0cb305of histen-proofsfork. Those revisions are recorded separately in the project card/provenance note. Substantial foundations adapted in the source remain attributed to Sidharth Hariharan and Gareth Ma, so the registered proof provenance ismix.Optimization metrics
The module split necessarily adds headers/import declarations and reformats long source lines to repository style, so raw physical line count is not presented as a reduction.
Reuse surface
A compile-through compatibility check against the downstream MetricCodes source confirms that
LeanPool.SpherePackingitself is a sufficient import. Its exact SpherePacking dependency surface is:CohnElkies.numeralTwoAtLeastCohnElkies.euclideanFiniteDimensionalCohnElkies.euclideanBorelSpace_root_.SpherePackingand its four field projectionsSpherePacking.distinct_centers_separation_boundSpherePacking.rescaleConfigurationThe two asymptotic helper lemmas used later by MetricCodes are defined locally in MetricCodes and are not SpherePacking dependencies. The focused compatibility shim recreating MetricCodes' packing conversion compiles cleanly against the project entry point.
Validation
lake build LeanPool.SpherePacking(3,768 jobs; warning-free)lake exe runLinter LeanPool.SpherePacking(2,332 declarations plus 1,563 generated; all 14 linters pass)lake exe lint-style LeanPool.SpherePackinglake exe mk_all --checksorry/admit/unsafe/partial/opaque/ broad-import scansThe full umbrella collision build and whole-repository deterministic quality audit were also started from a clean project-artifact state; CI remains authoritative for the complete pool-wide run.