feat: prove LSeries_totient_eq (IK L1029 sorry closure, corrected hypothesis Re(s) > 2)#1437
Open
d0d1 wants to merge 2 commits into
Open
feat: prove LSeries_totient_eq (IK L1029 sorry closure, corrected hypothesis Re(s) > 2)#1437d0d1 wants to merge 2 commits into
d0d1 wants to merge 2 commits into
Conversation
…othesis)
Close the sorry at IwaniecKowalskiCh1.lean L1029. The original hypothesis
`1 < s.re` is incorrect; the totient L-series converges absolutely only for
Re(s) > 2 (using φ(n) ≤ n to bound terms; average order ∑_{n≤x} φ(n) ~ 3x²/π²
establishes the abscissa of absolute convergence is 2). Lean's tsum returns 0
for non-summable series, so the original statement is false for Re(s) ∈ (1, 2].
Changes:
- Strengthen hypothesis to `2 < s.re`
- Add private helpers: totientAF, totientAF_apply, totientAF_mul_zeta_eq_powR1,
lseriesSummable_totientAF (all private, no public API change)
- Replace sorry with a proof via: summability + convolution identity
(totientAF * ζ = powR 1 via ∑_{d|n} φ(d) = n) + LSeries_powR_eq
Reviewed and approved by GPT 5.5 xhigh adversarial review.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
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
2 participants
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
Closes the
sorryatIwaniecKowalskiCh1.leanL1029 forLSeries_totient_eq.Bug fix: incorrect hypothesis
The original statement has hypothesis$\varphi(n) \le n$ , so bounding the terms by $n / n^{\mathrm{Re}(s)}$ requires $\mathrm{Re}(s) - 1 > 1$ . (The original hypothesis
(hs : 1 < s.re), which is mathematically incorrect. The Euler totient L-series:629069L(\varphi, s) = \sum_{n=1}^{\infty} \frac{\varphi(n)}{n^s}629069
converges absolutely only for
Re(s) > 2, not forRe(s) > 1. This is because1 < s.reis the convergence range for the Riemann zeta function, not for the totient L-series.)In Lean,
LSeries (↗totient) s = 0when the series is not absolutely summable (sincetsumof non-summable terms is 0), so the statement with1 < s.reis false forRe(s) \in (1, 2].Proof strategy
totientAF : ArithmeticFunction ℂwrappingNat.totienttotientAF * ζ = powR 1via the identityNat.sum_totient)LSeriesSummable (↗totientAF) sforRe(s) > 2usingLSeriesSummable_of_le_const_mul_rpowwith boundNat.totient_leLSeries_mul',LSeries_powR_eq,LSeries_zeta_eq_riemannZetato concludeAll helpers are
private. No public API surface changed beyond the hypothesis strengthening.