Repository navigation
Add PentagonalNumberTheoremAnalytic: Euler's pentagonal number theorem by two independent proofs - #446
Conversation
Two independent proofs of Euler's pentagonal number theorem, sharing no lemmas: a combinatorial route via Franklin's sign-reversing involution, and a q-series route through q-Pochhammer symbols, Euler's identities and the Cauchy identity to the Jacobi triple product, both as a formal power series identity over an arbitrary commutative ring and analytically over the complex numbers. Overlap with existing work is declared in the project card rather than left to be discovered. The Franklin route and the analytic pentagonal number theorem overlap the pooled `pentagonal-number-theorem` entry, whose analytic form is stated over RCLike fields and is the more general of the two. The q-Pochhammer and Gaussian binomial definitions and Euler's two identities overlap arXiv:2607.01544, where the latter appear as qPochhammerInf_eq_tsum and qPochhammerInf_neg_eq_tsum. The distinct contribution is the complex-analytic layer: the Jacobi triple product over ℂ for ‖q‖ < 1, ‖z‖ < 1, z ≠ 0 with an extension to the punctured disc, the analytic Cauchy identity, and the summability and locally-uniform-convergence machinery these require. The arXiv:2607.01544 development is non-archimedean throughout and mentions Complex in no file; ℂ is not a NonarchimedeanRing, so those results do not specialize to it. The pooled pentagonal entry has no Jacobi triple product. provenance: AI. The Lean proofs in both routes were largely generated by Aristotle (Harmonic). The Franklin route follows a blueprint written by the authors, lemma by lemma, and carries substantially more manual intervention and review; the q-series route is machine-generated blueprint and all, with the authors restructuring the library, renaming its API and reviewing statements. Builds warning-free against the pool's Mathlib; no sorry, no axioms beyond propext / Classical.choice / Quot.sound, no unsafe or partial. Co-Authored-By: Claude Opus 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: 822 maxHeartbeats units across 21 files (4,595 added LOC). Sum of Count-heartbeats wall-clock total: 177.20 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.PentagonalNumberTheoremAnalytic.Franklin.Defs |
30.00 s |
LeanPool.PentagonalNumberTheoremAnalytic.QSeries.JTP_Core |
24.00 s |
LeanPool.PentagonalNumberTheoremAnalytic.QSeries.FPS_Algebra |
23.00 s |
LeanPool.PentagonalNumberTheoremAnalytic.QSeries.JacobiTripleProduct |
9.20 s |
LeanPool.PentagonalNumberTheoremAnalytic.Franklin.Lemmas |
9.00 s |
LeanPool.PentagonalNumberTheoremAnalytic.QSeries.FPS |
8.10 s |
LeanPool.PentagonalNumberTheoremAnalytic.QSeries.JTP_KeyIdentity |
7.60 s |
LeanPool.PentagonalNumberTheoremAnalytic.Franklin.Helpers |
7.50 s |
LeanPool.PentagonalNumberTheoremAnalytic.QSeries.Defs |
6.60 s |
LeanPool.PentagonalNumberTheoremAnalytic.QSeries.JTP_Analytic |
5.70 s |
LeanPool.PentagonalNumberTheoremAnalytic.QSeries.CauchyIdentity |
5.50 s |
LeanPool.PentagonalNumberTheoremAnalytic.Franklin.FormalPowerSeries |
5.40 s |
Per-file `lean --profile` output
LeanPool/PentagonalNumberTheoremAnalytic.lean
import took 3.59s
cumulative profiling times:
elaboration 0.085ms
import 3.59s
initialization 29.6ms
interpretation 287ms
linting 0.158ms
module linting 0.0013ms
overlappingInstancesLinter 0.138ms
parsing 0.00184ms
tacticAnalysis 0.459ms
real 4.73
user 2.49
sys 2.24
LeanPool/PentagonalNumberTheoremAnalytic/Franklin.lean
import took 3.63s
cumulative profiling times:
elaboration 0.222ms
import 3.63s
initialization 29ms
interpretation 286ms
linting 0.143ms
module linting 0.00161ms
overlappingInstancesLinter 0.141ms
parsing 0.00173ms
tacticAnalysis 0.501ms
real 4.78
user 2.56
sys 2.23
LeanPool/PentagonalNumberTheoremAnalytic/Franklin/Defs.lean
import took 3.56s
cumulative profiling times:
attribute application 0.142ms
compilation (IR) 1.14ms
compilation (LCNF base) 32.6ms
compilation (LCNF impure) 6.03ms
compilation (LCNF mono) 15.7ms
elaboration 34.2ms
fix level params 0.109ms
import 3.56s
initialization 29.1ms
instantiate metavars 0.16ms
interpretation 359ms
let-to-have transformation 0.281ms
linting 8.63ms
module linting 0.00133ms
overlappingInstancesLinter 4.69ms
parsing 7.26ms
process pre-definitions 5.59ms
share common exprs 0.602ms
tacticAnalysis 15.1ms
type checking 2.89ms
typeclass inference 28.4ms
real 4.81
user 2.74
sys 2.21
LeanPool/PentagonalNumberTheoremAnalytic/Franklin/FormalPowerSeries.lean
import took 3.55s
cumulative profiling times:
attribute application 0.174ms
congr simp thm 4.82ms
elaboration 104ms
fix level params 1.11ms
import 3.55s
initialization 29.7ms
instantiate metavars 1.85ms
interpretation 466ms
let-to-have transformation 0.302ms
linting 15.7ms
module linting 0.00148ms
norm_num 8.5ms
overlappingInstancesLinter 4.43ms
parsing 16.4ms
process pre-definitions 9.09ms
ring 39ms
share common exprs 12.5ms
simp 157ms
tactic execution 205ms
tacticAnalysis 40ms
type checking 209ms
typeclass inference 1.63s
real 5.64
user 5.04
sys 2.24
LeanPool/PentagonalNumberTheoremAnalytic/Franklin/Helpers.lean
import took 3.64s
cumulative profiling times:
attribute application 0.864ms
blocked (unaccounted) 28ms
compilation (IR) 0.083ms
compilation (LCNF base) 0.887ms
compilation (LCNF impure) 0.406ms
compilation (LCNF mono) 0.912ms
congr simp thm 5.72ms
elaboration 172ms
fix level params 1.5ms
import 3.64s
initialization 29.3ms
instantiate metavars 4.32ms
interpretation 594ms
let-to-have transformation 0.53ms
linting 83.5ms
module linting 0.00137ms
norm_num 0.453ms
overlappingInstancesLinter 8.63ms
parsing 47ms
process pre-definitions 18.5ms
ring 6.52ms
share common exprs 10.9ms
simp 342ms
tactic execution 766ms
tacticAnalysis 75.2ms
type checking 614ms
typeclass inference 689ms
real 5.92
user 5.61
sys 2.27
LeanPool/PentagonalNumberTheoremAnalytic/Franklin/Lemmas.lean
import took 3.59s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 103ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 118ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 137ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 326ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 269ms
cumulative profiling times:
attribute application 0.469ms
blocked (unaccounted) 5.89ms
congr simp thm 33.1ms
elaboration 177ms
fix level params 3.71ms
import 3.59s
initialization 37.6ms
instantiate metavars 12.3ms
interpretation 2s
let-to-have transformation 0.517ms
linting 108ms
module linting 0.00131ms
norm_num 37.3ms
overlappingInstancesLinter 9.95ms
parsing 50.1ms
process pre-definitions 37.7ms
ring 154ms
share common exprs 54.7ms
simp 639ms
tactic execution 1.83s
tacticAnalysis 89.4ms
type checking 2.14s
typeclass inference 2.95s
real 8.43
user 12.36
sys 2.31
LeanPool/PentagonalNumberTheoremAnalytic/QSeries.lean
import took 1.59s
cumulative profiling times:
elaboration 0.0765ms
import 1.59s
initialization 28.2ms
interpretation 192ms
linting 0.139ms
module linting 0.0013ms
overlappingInstancesLinter 0.12ms
parsing 0.00241ms
tacticAnalysis 0.411ms
real 2.45
user 1.39
sys 1.07
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/CauchyIdentity.lean
import took 1.57s
cumulative profiling times:
attribute application 0.339ms
blocked (unaccounted) 0.206ms
congr simp thm 3.91ms
elaboration 91.9ms
fix level params 2.05ms
import 1.57s
initialization 28.9ms
instantiate metavars 4.42ms
interpretation 685ms
let-to-have transformation 0.261ms
linting 46.7ms
module linting 0.00154ms
norm_num 8.99ms
overlappingInstancesLinter 4.93ms
parsing 25.6ms
process pre-definitions 19.5ms
ring 85.8ms
share common exprs 27.7ms
simp 243ms
tactic execution 300ms
tacticAnalysis 62.3ms
type checking 132ms
typeclass inference 642ms
real 3.14
user 3.47
sys 1.15
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/Defs.lean
import took 891ms
cumulative profiling times:
attribute application 7.32ms
compilation (IR) 0.142ms
compilation (LCNF base) 4.59ms
compilation (LCNF impure) 0.96ms
compilation (LCNF mono) 3.48ms
congr simp thm 1.71ms
elaboration 94.9ms
fix level params 2.12ms
import 891ms
initialization 30.8ms
instantiate metavars 8.41ms
interpretation 377ms
let-to-have transformation 0.197ms
linting 11.5ms
module linting 0.00149ms
norm_num 10.2ms
overlappingInstancesLinter 10.1ms
parsing 12.4ms
process pre-definitions 24.2ms
ring 76.5ms
share common exprs 19.1ms
simp 185ms
tactic execution 137ms
tacticAnalysis 30.4ms
type checking 161ms
typeclass inference 226ms
real 2.09
user 2.13
sys 0.78
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/EulerIdentities.lean
import took 1.57s
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 115ms
cumulative profiling times:
attribute application 0.428ms
congr simp thm 4.4ms
dsimp 2.45ms
elaboration 32.8ms
fix level params 0.853ms
import 1.57s
initialization 30.2ms
instantiate metavars 1.2ms
interpretation 475ms
let-to-have transformation 0.124ms
linting 14.9ms
module linting 0.00136ms
norm_num 10.4ms
overlappingInstancesLinter 9.14ms
parsing 13.5ms
process pre-definitions 7.04ms
ring 15.6ms
share common exprs 6.8ms
simp 582ms
tactic execution 183ms
tacticAnalysis 29ms
type checking 74.7ms
typeclass inference 405ms
real 3.62
user 2.99
sys 1.12
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/FPS.lean
import took 1.3s
cumulative profiling times:
attribute application 1.21ms
blocked (unaccounted) 246ms
compilation (IR) 0.495ms
compilation (LCNF base) 22.5ms
compilation (LCNF impure) 2.98ms
compilation (LCNF mono) 7.04ms
congr simp thm 2.26ms
dsimp 3.11ms
elaboration 137ms
fix level params 2.32ms
import 1.3s
initialization 28.7ms
instantiate metavars 1.88ms
interpretation 365ms
let-to-have transformation 0.306ms
linting 20.8ms
module linting 0.00208ms
norm_num 0.963ms
overlappingInstancesLinter 14.7ms
parsing 16.1ms
process pre-definitions 13.7ms
ring 20ms
share common exprs 9.65ms
simp 83.4ms
tactic execution 153ms
tacticAnalysis 43.9ms
type checking 75.5ms
typeclass inference 608ms
real 2.76
user 2.60
sys 0.97
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/FPS_Algebra.lean
import took 1.36s
simp took 519ms
simp took 117ms
elaboration took 4.41s
tactic execution of Lean.Parser.Tactic.congr took 11s
cumulative profiling times:
attribute application 2.31ms
compilation (IR) 0.165ms
compilation (LCNF base) 1.93ms
compilation (LCNF impure) 0.997ms
compilation (LCNF mono) 1.59ms
congr simp thm 9.56ms
elaboration 5.03s
fix level params 12ms
import 1.36s
initialization 30.4ms
instantiate metavars 17.8ms
interpretation 917ms
let-to-have transformation 1.23ms
linting 82.7ms
module linting 0.00131ms
norm_num 11.6ms
overlappingInstancesLinter 33.6ms
parsing 71.3ms
process pre-definitions 77.2ms
ring 259ms
share common exprs 83.6ms
simp 905ms
tactic execution 12.3s
tacticAnalysis 173ms
type checking 693ms
typeclass inference 4.2s
real 15.73
user 25.84
sys 1.07
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/FPS_Euler.lean
import took 1.32s
cumulative profiling times:
attribute application 0.047ms
congr simp thm 1.52ms
elaboration 24.8ms
fix level params 0.597ms
import 1.32s
initialization 32.3ms
instantiate metavars 0.803ms
interpretation 261ms
let-to-have transformation 0.0504ms
linting 3.62ms
module linting 0.00162ms
norm_num 0.43ms
overlappingInstancesLinter 6.54ms
parsing 2.82ms
process pre-definitions 2.12ms
share common exprs 2.65ms
simp 41.9ms
tactic execution 53.5ms
tacticAnalysis 10.6ms
type checking 19.8ms
typeclass inference 144ms
real 2.35
user 1.61
sys 0.96
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/FiniteBinomial.lean
import took 909ms
cumulative profiling times:
attribute application 0.0146ms
congr simp thm 0.914ms
elaboration 14.2ms
fix level params 0.907ms
import 909ms
initialization 30.2ms
instantiate metavars 1.91ms
interpretation 181ms
let-to-have transformation 0.0315ms
linting 3.47ms
module linting 0.00139ms
norm_num 0.846ms
overlappingInstancesLinter 2.94ms
parsing 4.84ms
process pre-definitions 2.86ms
ring 18.7ms
share common exprs 6.03ms
simp 26.4ms
tactic execution 63.8ms
tacticAnalysis 15.6ms
type checking 22.8ms
typeclass inference 64.3ms
real 1.93
user 1.19
sys 0.79
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/InfPochhammer.lean
import took 1.55s
cumulative profiling times:
attribute application 0.107ms
blocked (unaccounted) 0.808ms
congr simp thm 1.87ms
elaboration 50ms
fix level params 0.37ms
import 1.55s
initialization 29.1ms
instantiate metavars 0.54ms
interpretation 353ms
let-to-have transformation 0.103ms
linting 10.4ms
module linting 0.00154ms
norm_num 0.691ms
overlappingInstancesLinter 3.45ms
parsing 6.9ms
process pre-definitions 4.93ms
ring 12.3ms
share common exprs 2.9ms
simp 119ms
tactic execution 61.4ms
tacticAnalysis 20.1ms
type checking 32.1ms
typeclass inference 186ms
real 2.64
user 2.00
sys 1.07
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JTP_Analytic.lean
import took 1.55s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 146ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 128ms
simp took 134ms
simp took 206ms
cumulative profiling times:
aesop 52.2ms
attribute application 0.308ms
congr simp thm 12.8ms
dsimp 15.5ms
elaboration 155ms
fix level params 4.39ms
import 1.55s
initialization 37.1ms
instantiate metavars 11.7ms
interpretation 1.86s
let-to-have transformation 0.453ms
linting 94.4ms
module linting 0.0017ms
norm_num 167ms
overlappingInstancesLinter 10.7ms
parsing 42.9ms
process pre-definitions 48.2ms
ring 103ms
share common exprs 57.1ms
simp 1.44s
tactic execution 701ms
tacticAnalysis 118ms
type checking 329ms
typeclass inference 1.86s
real 4.47
user 8.11
sys 1.16
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JTP_Core.lean
import took 1.6s
tactic execution of Lean.Parser.Tactic.refine took 10.6s
tactic execution of Lean.Parser.Tactic.refine took 6.52s
simp took 100ms
simp took 109ms
cumulative profiling times:
aesop 23.2ms
attribute application 0.199ms
compilation (IR) 0.17ms
compilation (LCNF base) 2.32ms
compilation (LCNF impure) 0.966ms
compilation (LCNF mono) 1.58ms
congr simp thm 5.23ms
dsimp 1.77ms
elaboration 125ms
fix level params 1.52ms
import 1.6s
initialization 33.5ms
instantiate metavars 2.97ms
interpretation 591ms
let-to-have transformation 0.312ms
linting 29.9ms
module linting 0.00127ms
norm_num 57.7ms
overlappingInstancesLinter 4.29ms
parsing 18.5ms
process pre-definitions 79.5ms
ring 58.6ms
share common exprs 19.4ms
simp 391ms
tactic execution 17.3s
tacticAnalysis 44.2ms
type checking 157ms
typeclass inference 487ms
real 20.12
user 20.62
sys 1.11
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JTP_Helpers.lean
import took 1.55s
cumulative profiling times:
attribute application 0.0226ms
congr simp thm 0.289ms
elaboration 9.91ms
fix level params 0.0663ms
import 1.55s
initialization 36.5ms
instantiate metavars 0.17ms
interpretation 230ms
let-to-have transformation 0.0296ms
linting 2.92ms
module linting 0.00129ms
overlappingInstancesLinter 1.96ms
parsing 2.3ms
process pre-definitions 0.996ms
share common exprs 0.365ms
simp 2.75ms
tactic execution 17.3ms
tacticAnalysis 9.97ms
type checking 3.67ms
typeclass inference 23.9ms
real 2.48
user 1.41
sys 1.12
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JTP_KeyIdentity.lean
import took 1.55s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 108ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 116ms
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 138ms
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 137ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 482ms
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 106ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 181ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 126ms
share common exprs took 118ms
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 108ms
cumulative profiling times:
attribute application 0.477ms
congr simp thm 18.8ms
elaboration 136ms
fix level params 4.98ms
import 1.55s
initialization 32.7ms
instantiate metavars 29.5ms
interpretation 2.99s
let-to-have transformation 0.233ms
linting 124ms
module linting 0.00175ms
norm_num 266ms
overlappingInstancesLinter 9.59ms
parsing 31.9ms
process pre-definitions 43.4ms
ring 243ms
share common exprs 172ms
simp 409ms
tactic execution 1.07s
tacticAnalysis 77.5ms
type checking 393ms
typeclass inference 1.67s
real 5.46
user 8.76
sys 1.13
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JacobiTripleProduct.lean
import took 1.57s
simp took 210ms
simp took 118ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 128ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 4.79s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 144ms
simp took 151ms
simp took 152ms
simp took 133ms
simp took 133ms
cumulative profiling times:
aesop 128ms
attribute application 0.228ms
congr simp thm 12.1ms
dsimp 8.77ms
elaboration 141ms
fix level params 3.89ms
import 1.57s
initialization 29.8ms
instantiate metavars 7.76ms
interpretation 6.21s
let-to-have transformation 0.385ms
linting 66.5ms
module linting 0.00135ms
norm_num 139ms
overlappingInstancesLinter 5.49ms
parsing 32.6ms
process pre-definitions 40.6ms
ring 168ms
share common exprs 53.6ms
simp 2.24s
tactic execution 497ms
tacticAnalysis 80.7ms
type checking 271ms
typeclass inference 1.22s
real 9.10
user 12.39
sys 1.17
LeanPool/PentagonalNumberTheoremAnalytic/QSeries/PentagonalNumber.lean
import took 1.55s
cumulative profiling times:
attribute application 0.08ms
compilation (IR) 0.0704ms
compilation (LCNF base) 0.828ms
compilation (LCNF impure) 0.213ms
compilation (LCNF mono) 0.303ms
congr simp thm 6.31ms
elaboration 55.4ms
fix level params 1.25ms
import 1.55s
initialization 30.2ms
instantiate metavars 3.67ms
interpretation 456ms
let-to-have transformation 0.144ms
linting 21.8ms
module linting 0.00143ms
norm_num 34.7ms
overlappingInstancesLinter 3.65ms
parsing 16.2ms
process pre-definitions 10.7ms
ring 98.8ms
share common exprs 28ms
simp 201ms
tactic execution 349ms
tacticAnalysis 34.1ms
type checking 249ms
typeclass inference 574ms
real 3.15
user 3.25
sys 1.10
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
|
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; no outstanding correctness, integration, security, or repository-rule issue remains. SummaryAdds two independent formalizations of Euler’s pentagonal number theorem:
Reviews (32) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
P1 Formal JTP is monomorphic — correct. `FPS.lean` has `local notation "A" => LaurentPolynomial ℂ`, so `jacobiProd : A⟦X⟧` is fixed to (LaurentPolynomial ℂ)⟦X⟧ and the theorem takes no coefficient-ring parameter. The "arbitrary commutative ring" wording was wrong in both the main_results entry and the project summary; both now state the actual setting. The claim is narrowed rather than the development generalized, since generalizing is real work and should not ride along in a metadata fix. P1 Source revision missing — added `source.revision`, pinning the upstream commit the vendored copy was taken from. P2 Broad Mathlib imports — CODE_QUALITY.md forbids them outright, so this is treated as blocking. All four Franklin files replaced `import Mathlib` with the specific modules they use. Two corrections were needed along the way: `Mathlib.Tactic.Omega` no longer exists (omega is in Lean core), and `FormalPowerSeries.lean` additionally needs `Mathlib.Tactic.LinearCombination` and `Mathlib.Tactic.Zify`, which the blanket import had been supplying silently. No broad import remains anywhere in the project. P2 Module documentation is stale — correct on both counts. Franklin/Lemmas.lean listed five names under "Main results" that are not declared anywhere; it now names the DP*/pe_minus_po_* declarations that exist. FPS_Euler.lean claimed to prove euler_second_identity, which is proved downstream in FPS_Algebra.lean; its docstring now describes the unit and factorisation lemmas the module actually contains and says where the identity is proved. Still builds warning-free: 0 errors, 0 warnings. The three remaining P2 findings are not addressed here and are answered on the PR: the duplicated JTP assembly and the JTP_Helpers dead branch are real observations about proof structure, and the namespace question affects the upstream project's public API rather than the vendored copy. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Re-vendored from the upstream project after fixing all three remaining findings there, so the pooled copy and the source repository do not diverge. JTP_Helpers.lean is gone. Its two theorems were used zero times, the module was reachable only through the aggregate import, and neither name appeared in the blueprint or the project card. The review's further observation was also correct: the second theorem's non-annulus branch simply called the already-completed jacobiTripleProduct instead of the functional-equation propagation it advertised. Namespaces are contained. `namespace Nat` in QSeries/Defs.lean closed before `namespace QSeries` opened, so its two Pascal-rule lemmas really were landing in Mathlib's root Nat; they are now QSeries.Nat, and `#check @Nat.choose_two_succ` reports an unknown constant. `_root_.TendstoUniformlyOn.mul_of_bounded` is now the project-local `tendstoUniformlyOn_mul_of_bounded`. The Franklin API, 124 declarations previously all in the root namespace, now lives under PentagonalNumberTheorem.Franklin; its consumers were updated accordingly, including 52 blueprint annotations upstream. The broad-import fix is also upstream now rather than applied only to the vendored copy, and the card's pinned source revision is updated to match. Builds warning-free: 0 errors, 0 warnings. The one finding not addressed remains the duplicated JTP assembly in JacobiTripleProduct.lean versus JTP_Core.jacobiTripleProduct_of_hasSum. That is a refactor of a working proof rather than a defect, and we would rather do it separately than fold it into a review-response commit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The whole-pool linter rejected two declarations for containing underscores, which mathlib's convention forbids for definitions though not theorems: `p_count` is now `pCount`, and the two anonymous scoped instances on LaurentPolynomial ℂ are named explicitly. Lean was auto-generating a name for the anonymous instances and disambiguating it to `..._leanPool`; the underscore came from that suffix rather than from our source, so naming them removes it. Re-vendored from upstream so the pooled copy and the source repository stay in step, and the card's pinned revision is updated to match. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Changes requested at 165d8c73ef9add34749af08141f3e217100b2042. I compared the refresh with b7ff3fb682051b652e79d2a5c9284d9359e3cc49: only the six already-merged polynomial restricted-sum files changed; this project's source is identical. The fresh build is still running, so the earlier failure is evidence about unchanged source, not a claimed completed result for the new SHA.
- Repair the blocking module filenames. The previous-head build log reaches a warning-free Lean build and semantic lint, then fails style on
FPS_Algebra,FPS_Euler,JTP_Analytic,JTP_Core, andJTP_KeyIdentity. All five names remain at this head. Rename these modules to the repository's accepted naming form, update imports, regenerate/check the index, and pass the unchanged style and full quality gates. - Use the existing Jacobi assembly lemma.
QSeries/JacobiTripleProduct.lean:275–335rebuilds summability, Fubini, and both diagonal arguments even thoughQSeries/JTP_Core.lean:149–168exposesjacobiTripleProduct_of_hasSumfor exactly these two EulerHasSuminputs. This duplicates a substantive proof path and makes maintenance drift likely. Derive the public theorem through that core lemma, remove private helpers left unused, preserve the endpoint types, and validate the project build/trust checks and compile profile. This independently confirms the still-relevant review thread; the older import/doc findings have already been addressed. - Align the advertised formal Jacobi scope with Lean. The opening description claims an arbitrary commutative coefficient ring, but
FPS.lean:172–208fixes the Jacobi product and bilateral series to(LaurentPolynomial ℂ)⟦X⟧, andFPS_Algebra.lean:709proves equality for those definitions. Some supporting Euler lemmas are generic; this does not make the Jacobi endpoint generic. Narrow the PR's claim to the actual coefficient ring, or supply and validate a genuinely generic endpoint.
The disclosed overlap does not itself justify rejecting the whole project: the existing pooled pentagonal theorem is stronger on that endpoint, while the ordinary complex-analytic Jacobi/Cauchy and locally-uniform-convergence development adds a distinct, substantial contribution beyond the nonarchimedean source. No edit was pushed to the contributor's external fork.
Module filenames. The style gate rejects underscores and no pooled project uses them: FPS_Algebra, FPS_Euler, JTP_Analytic, JTP_Core and JTP_KeyIdentity are now FPSAlgebra, FPSEuler, JTPAnalytic, JTPCore and JTPKeyIdentity, with imports and the regenerated index updated. Jacobi assembly. QSeries/JacobiTripleProduct.lean rebuilt the summability, Fubini and diagonal arguments that JTPCore.jacobiTripleProduct_of_hasSum already performs on exactly the two Euler HasSum inputs the public theorem has in hand. It now derives through that lemma in four lines, and the four private helpers it needed are removed as dead. The endpoint type is unchanged; the file drops from 338 to 285 lines. Formal Jacobi scope. The card's claim was narrowed in the previous commit; the PR description is corrected alongside this push. FPS.lean fixes the Jacobi product and bilateral series to (LaurentPolynomial ℂ)⟦X⟧ and FPSAlgebra.lean proves equality for those definitions, so the endpoint is not generic even though some supporting Euler lemmas are. Re-vendored from upstream so the pooled copy and the source repository stay in step; the card's pinned revision is updated to match. Builds warning-free. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…/JonCYeh/lean-pool into conrad/pentagonal-number-theorem
|
All three items are addressed in 1. Module filenames. Renamed the five underscore modules to UpperCamelCase, matching the rest of the pool:
2. Jacobi assembly. You were right that the public theorem was re-deriving what theorem jacobiTripleProduct {q z : ℂ} (hq : ‖q‖ < 1) (hz : ‖z‖ < 1) (hz' : z ≠ 0) :
jacobiProd q z = jacobiBilateral q z := by
unfold jacobiProd jacobiBilateral jacobiBilateralPos jacobiBilateralNeg
exact jacobiTripleProduct_of_hasSum hq hz'
(hasSum_pow_choose_two_mul_pow_mul_qPochhammerInf hq hz)
(euler_second_identity_div' (z := z) hq)Four private helpers became dead with it ( 3. Formal Jacobi scope. Corrected — the claim of an arbitrary commutative coefficient ring was wrong. Gates re-run on the merged tree: |
State the coefficient ring as (LaurentPolynomial ℂ)⟦X⟧ directly and rewrap to the surrounding line width. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Automated substantive review; final disposition: changes requestedReviewed exact current head Independent substantive review: the complex-analytic Jacobi triple product, analytic Cauchy identity and locally uniform convergence layer form a substantial completed contribution. The general Validation at this head: warning-free focused build (2,822 jobs), project environment/style linters, all 276 public axiom queries (only propext/choice/Quot.sound), and compiled private/generated-declaration trust audit pass. The recorded pre-update profile is 89.89 s; it is not an exact-head performance measurement. No unacceptable hot spot or concrete remaining mathematical defect was found in the bounded file/dependency review. Final disposition: Changes requested after exact-head repository CI exposed stale unqualified registry declarations and a missing generated project card. The linked review gives the reproduced errors and tested correction. This supersedes the earlier operational needs-maintainer hold; that label has been removed. The proof/novelty review above remains applicable. Reconciled current head |
Vilin97
added
needs-maintainer
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Changes requested at 932556e94d25dae0354445b251fee853317e9f48. The earlier mathematical review remains favorable for the distinct complex-analytic Jacobi/Cauchy/convergence layer, and the corrected coefficient-ring description and duplicated proof chain are resolved. New exact-head CI evidence supersedes the earlier needs-maintainer disposition: repository quality fails for this project's metadata.
LeanPool/projects.ymlregisterseuler_pentagonal_number_theorem_packagedandcoeff_prod_eq_pe_sub_powithout their actualPentagonalNumberTheorem.Franklin.namespace, in bothmain_declarationsandmain_results. Importing the entry module and checking those unqualified names reproducesUnknown identifierlocally; the definitions atFranklin/FormalPowerSeries.lean:121,214are namespaced. Qualify all four registry references so the advertised entry points resolve.LeanPool/PentagonalNumberTheoremAnalytic.leanhas no generated project card. Regenerate it from the corrected registry usingpython -m lean_pool.quality --repo .. --write-project-cardsfrompython/, and commit the target card. CI reports this card as out of date.
I tested these narrowly scoped metadata corrections in an isolated worktree: the project's generated-card check and all registered-declaration checks then pass. No proof or gate changes are needed, and I have not pushed to the external fork. Acceptance requires those fixes and successful repository quality/required CI at the resulting head. Refreshing the strict base and resolving the existing review conversations are still necessary before merge. The warning-free focused proof build, project linters, and 276 public axiom closures are useful evidence but do not excuse the failing metadata gate.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Changes requested at 2545129108185fb3877123a94b653ee8234cdacf. I reviewed the full update from 932556e94d25dae0354445b251fee853317e9f48: only README statistics changed. All proof files, registry/card, toolchain and dependencies are byte-identical, so the reproduced blocking findings and tested correction remain valid.
Acceptance condition: qualify both Franklin headline names with PentagonalNumberTheorem.Franklin. in all four main_declarations/main_results references, regenerate the missing entry-module project card, and pass repository quality plus required CI at the resulting head. This is an observed metadata defect, not a mathematical objection or a speculative CI failure. The previous head's actual failure log and successful local correction establish the cause; new-head checks are not yet complete.
All seven review conversations are now resolved; that prior integration boundary is cleared. The source/novelty assessment and successful unchanged-code build/axiom/trust inspection remain applicable. No external-fork push was made.
The Franklin declarations were namespaced under PentagonalNumberTheorem.Franklin without updating LeanPool/projects.yml, so the registered names did not resolve. - Qualify both Franklin references in main_results. - Reduce main_declarations to the primary result, which the registry's own main_results ordering already identifies as such. The generated card emits main_declarations as a single unwrapped line, and five qualified names came to 269 characters against the 100-character style linter; 115 of 193 pooled projects list exactly one declaration. All five remain fully qualified in main_results, which the quality checker permits. - Drop three tags for the same line-length reason. - Commit the generated card for LeanPool/PentagonalNumberTheoremAnalytic.lean, produced by `python -m lean_pool.quality --repo .. --write-project-cards`. Build: 2822 jobs, 0 errors, 0 warnings. Card regeneration is idempotent. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Both metadata defects are fixed in 1. Unqualified registry references. Both Franklin names are now qualified in The card generator emits
So 2. Missing project card. Generated with the command you gave and committed. The generator also rewrote 18 unrelated projects' entry modules with a cosmetic blank-line change; I reverted all of those, so this commit touches only Verified at
The strict base was refreshed in Separately, the same unqualified-name defect existed in the upstream repository's own |
# Conflicts: # LeanPool/projects.yml
|
Want your agent to iterate on Greptile's feedback? Try greploops. |
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# 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.
Changes requested at 4f646c08d4 (auto-rebase merge of main; project files identical to 8195b46, which resolved the earlier metadata findings — both Franklin names are qualified and the generated card is present).
Blocking: the required Build project check fails at this head, and the cause is on the author side. main moved to Lean/Mathlib v4.34.0 (Mathlib 5ed29652, #436) after your last push, and this project no longer builds against it. I reproduced the exact-head failure locally with the pinned toolchain and Mathlib cache, and verified a fix that gives lake build LeanPool.PentagonalNumberTheoremAnalytic a clean run (2885 jobs, 0 errors, 0 warnings):
QSeries/JTPAnalytic.lean:259, 263—Finset.prod_le_prodno longer takes a nonnegativity hypothesis. In current Mathlib the two-hypothesis form for ordered semirings isFinset.prod_le_prod₀;Finset.prod_le_prodis now the ordered-monoid version with one hypothesis, henceFunction expectedand thelinarithfailure. Replace both call sites withFinset.prod_le_prod₀.- Deprecations that trip the warning gate:
QSeries/FPS.lean:7imports the deprecated moduleMathlib.Data.Complex.Basic(useMathlib.Basic.Complex.Basic), andQSeries/JacobiTripleProduct.lean:163usesmul_le_one₀, deprecated with no replacement (inline its proof:(mul_le_of_le_one_left hb₀ ha).trans hb). Used tac1 <;> tac2 where (tac1; tac2) would sufficelinter, four sites:JacobiTripleProduct.lean:155,JTPKeyIdentity.lean:193,JTPAnalytic.lean:80, 407— eachconvert … <;> …produces a single goal; write(convert … ; …).
The tested patch (10 insertions, 9 deletions across four files):
diff --git a/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/FPS.lean b/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/FPS.lean
index d3b908b1a..184be2c97 100644
--- a/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/FPS.lean
+++ b/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/FPS.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jonathan Conrad, Paula Muermann, Maryna Viazovska
-/
import Mathlib.Algebra.Polynomial.Laurent
-import Mathlib.Data.Complex.Basic
+import Mathlib.Basic.Complex.Basic
import Mathlib.RingTheory.PowerSeries.Inverse
import Mathlib.RingTheory.PowerSeries.PiTopology
diff --git a/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JTPAnalytic.lean b/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JTPAnalytic.lean
index 988280c6b..39e658962 100644
--- a/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JTPAnalytic.lean
+++ b/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JTPAnalytic.lean
@@ -77,7 +77,7 @@ theorem summable_pow_succ_mul_norm_pow_choose_two {q : ℂ} (hq : ‖q‖ < 1) (
theorem hasSum_pow_choose_two_mul_pow_mul_qPochhammerInf' {q z : ℂ} (hq : ‖q‖ < 1) :
HasSum (fun n : ℕ => q ^ n.choose 2 * z ^ n * qPochhammerInf (q * q ^ n) q)
(qPochhammerInf q q * qPochhammerInf (-z) q) := by
- convert HasSum.mul_left (qPochhammerInf q q) (euler_second_identity' hq) using 1 <;> try rfl
+ (convert HasSum.mul_left (qPochhammerInf q q) (euler_second_identity' hq) using 1; try rfl)
ext n
by_cases hn : qPochhammer q q n = 0
· exact absurd hn <| qPochhammer_ne_zero hq (by linarith) n
@@ -256,11 +256,11 @@ lemma exists_norm_qPochhammer_le {q : ℂ} (hq : ‖q‖ < 1) (R : ℝ) :
(norm_sub_le _ _).trans <| by
simpa [norm_mul] using
add_le_add_left (mul_le_mul_of_nonneg_right haR (by positivity : (0 : ℝ) ≤ ‖q‖ ^ k)) 1
- simpa [qPochhammer] using Finset.prod_le_prod (fun _ _ => norm_nonneg _) h_bound
+ simpa [qPochhammer] using Finset.prod_le_prod₀ (fun _ _ => norm_nonneg _) h_bound
have h_exp_bound : ∏ k ∈ Finset.range n, (1 + R * ‖q‖ ^ k)
≤ Real.exp (∑ k ∈ Finset.range n, R * ‖q‖ ^ k) := by
rw [Real.exp_sum]
- exact Finset.prod_le_prod (fun k _ => by linarith [hterm k])
+ exact Finset.prod_le_prod₀ (fun k _ => by linarith [hterm k])
fun k _ => by rw [add_comm]; exact Real.add_one_le_exp _
refine h_prod_le.trans <| h_exp_bound.trans <| Real.exp_le_exp.mpr ?_
rw [← Finset.mul_sum, div_eq_mul_inv]
@@ -404,7 +404,7 @@ theorem jacobiBilateral_mul_eq_div' {q z : ℂ} (hq : ‖q‖ < 1) (hq' : q ≠
simp +arith +decide [Nat.choose]]; ring_nf
simp +decide [mul_assoc, mul_comm, mul_left_comm, hq']
· have := summable_inv_pow_mul_pow_choose_two (z := q * z) hq
- convert this.mul_left (q * z) using 2 <;> first | rfl | ring_nf
+ (convert this.mul_left (q * z) using 2; first | rfl | ring_nf)
simp +decide [hq', hz', mul_assoc, mul_comm q]
rw [h_split, h_pos, h_neg,
show jacobiBilateral q z = jacobiBilateralPos q z + jacobiBilateralNeg q z from rfl]
diff --git a/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JTPKeyIdentity.lean b/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JTPKeyIdentity.lean
index 46a66cfa2..789dd7362 100644
--- a/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JTPKeyIdentity.lean
+++ b/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JTPKeyIdentity.lean
@@ -190,7 +190,7 @@ theorem keySum_sub_keySum_succ {q : ℂ} (hq : ‖q‖ < 1) (k : ℕ) :
have h : Summable fun m : ℕ =>
q ^ (m * (m + k + 1)) / (qPochhammer q q m * qPochhammer q q (m + k + 1)) := by
exact summable_keySummand hq (k + 1)
- convert h.mul_left (-q ^ (k + 1)) using 2 <;> first | rfl | ring_nf
+ (convert h.mul_left (-q ^ (k + 1)) using 2; first | rfl | ring_nf)
convert congr_arg₂ (· + ·) h_split
(show ∑' m : ℕ, -(q ^ (m * (m + k)) * q ^ (m + k + 1)) /
(qPochhammer q q m * qPochhammer q q (m + k + 1)) = -q ^ (k + 1) * keySum q (k + 1)
diff --git a/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JacobiTripleProduct.lean b/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JacobiTripleProduct.lean
index f83f271d7..b057dbfed 100644
--- a/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JacobiTripleProduct.lean
+++ b/LeanPool/PentagonalNumberTheoremAnalytic/QSeries/JacobiTripleProduct.lean
@@ -152,7 +152,7 @@ theorem jacobiBilateral_mul_eq_div {q z : ℂ} (hq : ‖q‖ < 1) (hq' : q ≠ 0
ring_nf
· have := summable_inv_pow_mul_pow_choose_two (z := z) hq
rw [← summable_nat_add_iff 1]
- convert this using 2 <;> try rfl
+ (convert this using 2; try rfl)
norm_num [Nat.choose_succ_succ, pow_succ']
ring
· refine Summable.of_norm ?_
@@ -160,8 +160,9 @@ theorem jacobiBilateral_mul_eq_div {q z : ℂ} (hq : ‖q‖ < 1) (hq' : q ≠ 0
refine Summable.of_nonneg_of_le (fun n => by positivity) (fun n => ?_)
(summable_geometric_of_lt_one (by positivity) hz)
exact le_trans (mul_le_of_le_one_right (by positivity)
- (mul_le_one₀ (pow_le_one₀ (by positivity) hq.le) (pow_nonneg (by positivity) _)
- (pow_le_one₀ (by positivity) hq.le))) (mul_le_of_le_one_left (by positivity) hz.le)
+ ((mul_le_of_le_one_left (pow_nonneg (by positivity) _)
+ (pow_le_one₀ (by positivity) hq.le)).trans (pow_le_one₀ (by positivity) hq.le)))
+ (mul_le_of_le_one_left (by positivity) hz.le)
· rw [← summable_nat_add_iff 1]
exact (summable_pow_mul_pow_choose_two hq hz).comp_injective Nat.succ_injective
· exact summable_pow_mul_pow_choose_two hq hzAcceptance condition: push the repair (or an equivalent) to conrad/pentagonal-number-theorem, and let the required Build project, separation, and documentation-preflight checks go green on the resulting head. Because the branch is on your fork, automation did not push this for you. Nothing else is outstanding: the earlier faithfulness/source/novelty assessment of the distinct complex-analytic Jacobi/Cauchy/convergence layer stands, and all review threads are resolved.
# Conflicts: # LeanPool/projects.yml
main moved to Lean/Mathlib v4.34.0 (Mathlib 5ed29652, LeanPool#436) and this project no longer built against it. Applies the repair from the maintainer review: - Finset.prod_le_prod lost its nonnegativity hypothesis; it is now the ordered-monoid form with one hypothesis. The two call sites in JTPAnalytic.lean want the ordered-semiring form, Finset.prod_le_prod₀. - Mathlib.Data.Complex.Basic is deprecated in favour of Mathlib.Basic.Complex.Basic. - mul_le_one₀ is deprecated with no replacement; its proof is inlined as (mul_le_of_le_one_left hb₀ ha).trans hb, which is the lemma's own body. - Four `convert … <;> …` sites produce a single goal, so the linter asks for `(convert …; …)`. Verified against the pinned Mathlib at 5ed29652: lake build LeanPool.PentagonalNumberTheoremAnalytic — 2885 jobs, 0 errors, 0 warnings. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Pushed as Thank you for diagnosing it and shipping a tested patch rather than just the failure — that saved a lot of guesswork. I checked each change against the Mathlib source at that revision before applying, and they hold:
One note on scope: The upstream repository still pins an older Mathlib, so this repair is vendored-copy-only for now; it will go upstream when we bump there. |
# Conflicts: # LeanPool/projects.yml
Vilin97
added
the
needs-maintainer
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Independent exact-head content review at 8b56d70d3c5c21c1cb16690193bdede50130902a: the previous requested Mathlib import, product-order lemma and scoped-convert fixes are present in the four-file +10/−9 delta. All earlier substantive overlap/card/namespace findings are resolved, with no unresolved threads. The analytic Cauchy identity and full complex Jacobi triple product (‖q‖<1, every z≠0, including q=0) have genuine convergence proofs and are independently significant. The Wang pentagonal result and AxiomMath non-archimedean q-series overlap are accurately disclosed; the latter's StrongNonarchimedeanRing hypothesis does not instantiate to ordinary ℂ. Primary source, Apache-2.0 license and AI provenance checked. Quality 4/5: useful q-series/convergence boundaries and manageable module/proof cost. The source tree is unchanged by the latest main refresh; the earlier content head passed full CI/trust, and current protected CI is still running. Approval resolves this reviewer's obsolete change requests; disposition is needs-maintainer for protected fork refresh/current CI with repository auto-merge disabled. No fork mutation or protection bypass is authorized.
|
Disposition: needs-maintainer — independently reviewed Complex-analytic Jacobi triple product and Cauchy identity are substantial, despite directly overlapping pentagonal-number proofs. The existing Wang pool entry supplies stronger RCLike pentagonal-number results, and AxiomMath RogersRamanujan overlaps q-series formal identities. Current card discloses both. AxiomMath's checked JTP source requires StrongNonarchimedeanRing; it does not specialize to ordinary ℂ. This PR proves the analytic JTP for every ‖q‖<1 and z≠0, including q=0, with genuine summability and limit arguments. Pinned primary source/Apache-2.0/AI provenance checked. Previous review's four-file API/tactic repairs are implemented (+10/−9 lines): Basic.Complex import, prod_le_prod₀ and scoped convert continuations. No unresolved threads. Content review passes, quality 4/5. Full required CI passed at 8b56d70; the subsequent main-only refresh starts fresh CI; the fork branch still requires a protected refresh against newer main, and repository auto-merge is unavailable; no fork writes authorized. Greptile notes only nonblocking stale module-documentation navigation; no new unresolved inline thread was posted. Advisory build 89.89 s; serial per-file sum 143.89 s. Largest FPS algebra module ~26 s. Current Mathlib fixes preserve statements; previous content-head full CI was green. Final-head reconciliation: the main refresh contains the already-reviewed Komlós import/Burkholder refactor and generated metadata. This PR’s own proof/tooling files are unchanged by that refresh. Fresh checks on refreshed heads remain the required gate; earlier successful runs are historical evidence, not an approval of pending CI. Repository auto-merge remains disabled. The linked disposition is the final action; no protection or workflow setting was changed. The formal approval at 8b56d70 superseded the earlier compatibility change request; this current-head review verifies that the project’s proof files remain byte-identical. 2026-09-20 reconciliation: needs-maintainer at Quality 4/5. Previous Mathlib compatibility defects are repaired, latest exact-head formal APPROVED review supersedes the old change request, and no thread is unresolved. Two main/metadata-only refreshes preserve the analytic source. Fresh required CI is pending and branch is behind; external fork pushes are unauthorized. Greptile’s old module-navigation note is advisory, not a remaining mathematical blocker. The norm-q<1 domain is the intended analytic convergence domain, and the all-z≠0 extension is present. Not acceptance of an insignificant special case; no Erdős claim. The current own-project/tooling files were compared with the reviewed content; later main-only refreshes do not change the conclusion. Current required CI and final head are recorded separately from historical green runs. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Approve for merge after the required checks pass on the refreshed base. Reviewed commit 644e0ef97e90785d3ff53d09015e133886e52fc6.
The complex-analytic Jacobi triple product and Cauchy identity are substantial completed results. I traced jacobiTripleProduct through jacobiTripleProduct_of_hasSum, the nonzero q-Pochhammer denominator bounds and the two diagonal sums; the extension jacobiTripleProduct' covers every nonzero complex z with norm q < 1 and handles q = 0 explicitly. The formal identity uses (LaurentPolynomial ℂ)⟦X⟧, exactly as the corrected card states. The Franklin endpoint counts distinct positive-part partitions and uses integer subtraction, including the n = 0 case.
There is real overlap with the pool's Pentagonal.pentagonalNumberTheorem_complex, which already works over RCLike. The analytic Jacobi/Cauchy layer and its convergence proofs provide the additional mathematical contribution; the card discloses the pentagonal overlap. A search of current Mathlib and the pool found no existing complex-analytic Jacobi triple product or this Cauchy identity. The pinned upstream README matches the two proof routes, coefficient-ring scope and stated provenance.
All earlier concrete findings are resolved: qualified Franklin registry names, generated card, renamed modules, reuse of the Jacobi assembly lemma, and the current Mathlib API repairs are present. Exact-commit Build project, separation and documentation preflight checks all pass. No further content change is needed; this supersedes the earlier requests for changes.
Integration check: the project source files and its registry card are byte-identical at current head 5b846a0bc21f188bdf142b1d60530261f877d2e1 to the reviewed commit above. The new head contains the base integration only; fresh required checks must pass before merge.
2 participants
Adds
PentagonalNumberTheoremAnalytic: two independent proofs of Euler's pentagonal number theorem, sharing no lemmas — a combinatorial route via Franklin's sign-reversing involution, and a q-series route through q-Pochhammer symbols, Euler's identities and the Cauchy identity to the Jacobi triple product, proved both as a formal power series identity in(LaurentPolynomial ℂ)⟦X⟧and analytically over ℂ.Source repository: https://github.com/viazovska/PentagonalNumberTheorem
Overlap with existing work
Flagging this up front rather than leaving it to the novelty review.
The pool already has
pentagonal-number-theorem(Weiyi Wang,wwylele/PentagonalNumberTheorem). Our Franklin route and our analytic pentagonal number theorem overlap it directly, and on the mathematics that entry is the stronger of the two: its analytic form is stated overRCLike Kwhere ours is specific to ℂ, and it proves a generic core once and instantiates it for both the formal and analytic settings. We are not proposing this as a replacement, and we have taken a distinct slug and entry module accordingly.arXiv:2607.01544 (Lau, Lee, Ono —
AxiomMath/RogersRamanujan) formalizes q-Pochhammer symbols, q-binomial coefficients, Euler's two identities and the Jacobi triple product in Lean. Our q-Pochhammer and Gaussian binomial definitions overlap theirs, as do our Euler identities, which appear there asqPochhammerInf_eq_tsumandqPochhammerInf_neg_eq_tsum.What neither covers is the complex-analytic case. The AxiomMath development is non-archimedean throughout: its Jacobi triple product is gated on
IsTopologicallyNilpotent qwith[NonarchimedeanRing R]/[StrongNonarchimedeanRing R], the series rearrangement goes throughmul_of_nonarchimedean, and the project mentionsComplexin no file. ℂ under its usual norm is not aNonarchimedeanRing, so those results do not specialize to it. The pooled pentagonal entry has no Jacobi triple product at all.So the distinct contribution is:
QSeries.jacobiTripleProduct— the Jacobi triple product over ℂ for‖q‖ < 1,‖z‖ < 1,z ≠ 0, andjacobiTripleProduct'extending it to the punctured discz ≠ 0QSeries.hasSum_qPochhammer_div_mul_pow— the Cauchy identity over ℂQSeries/JTPAnalytic.lean(474 lines) — the summability, locally-uniform-convergence and Tannery-style interchange machinery these need, which a non-archimedean proof never has to buildProvenance:
AIThe Lean proofs in both routes were largely generated by Aristotle (Harmonic). The two differ in how much human direction went in: the Franklin route follows a blueprint the authors wrote themselves, lemma by lemma, and carries substantially more manual intervention and review; the q-series route is machine-generated blueprint and all, with the authors restructuring the library, renaming its API to be mathlib-ready and reviewing statements. Claude assisted with proof development, the blueprint and CI.
If you read that split as
mixwe would not object, butAIseems the more accurate of the two.Gates
Builds warning-free against the pool's Mathlib (0 errors, 0 warnings); no
sorry; no axioms beyondpropext/Classical.choice/Quot.sound; nounsafeorpartial; Apache-2.0; file header on all 20 files; largest file 717 lines.The upstream project also carries a
leanblueprintblueprint in which every formalized declaration is tied to a prose statement and proof sketch, withleanblueprint checkdeclsenforcing in CI that every\lean{}annotation names a real declaration, and all 220 public declarations carry docstrings. Blueprint, dependency graph and doc-gen4 API documentation: https://viazovska.github.io/PentagonalNumberTheorem/🤖 Generated with Claude Code