Trace — 2607.20408v1
**Planning workspace inspection and commentary update**
I’ll first extract the exact central theorem, dependency chain, and any explicitly imported deep inputs from the paper. Then I’ll map that claim against mathlib, formalize the strongest faithful statement achievable, and repeatedly compile the development and its documentation before issuing the required JSON verdict.
$ /bin/bash -lc "pwd && rg --files -g 'AGENTS.md' -g '"'!repro/.lake/**'"' -g '"'!repro/.git/**'"' | sed -n '1,80p' && rg --files | sed -n '1,100p'" codex-events.jsonl paper.pdf codex.err paper.json paper.txt PROMPT.txt repro/Counterexamples.lean repro/README.md repro/docs.lean repro/lake-manifest.json repro/DownstreamTest/README.md repro/DownstreamTest/lakefile.toml repro/DownstreamTest/DownstreamTest.lean repro/lean-toolchain repro/CODE_OF_CONDUCT.md repro/Archive.lean repro/Cache/Infra.lean repro/Cache/Marker.lean repro/Cache/README.md repro/Cache/Cli.lean repro/Cache/Main.lean repro/Cache/Requests.lean repro/Cache/Lean.lean repro/Cache/Warning.lean repro/Cache/Hashing.lean repro/Cache/Query.lean repro/Cache/IO.lean repro/Cache/SECURITY.md repro/Cache/Test.lean repro/MathlibTest/AModuleWithAVeryLongModuleNameToTestTheLineLengthLinterXXXXXXXXXXXXXXXXXXXXXXXX.lean repro/MathlibTest/irreducibleDef.lean repro/MathlibTest/byContra.lean repro/MathlibTest/Continuity.lean repro/MathlibTest/BinaryRec.lean repro/MathlibTest/symbolFrequency.lean repro/MathlibTest/Complex.lean repro/MathlibTest/InstanceDiamonds/Normed.lean repro/MathlibTest/InstanceDiamonds/Data/Complex/Module.lean repro/MathlibTest/InstanceDiamonds/Analysis/Normed/Field/WithAbs.lean repro/MathlibTest/InstanceDiamonds/Algebra/Algebra/Rat.lean repro/MathlibTest/IsBoundedDefault.lean repro/MathlibTest/MkIffOfInductive.lean repro/MathlibTest/delaborators.lean repro/MathlibTest/symm.lean repro/MathlibTest/ValuedCSP.lean repro/MathlibTest/TacticCheckInstancesReassoc.lean repro/MathlibTest/TacticAnalysis.lean repro/MathlibTest/borelize.lean repro/MathlibTest/renameBvar.lean repro/MathlibTest/DeriveCountable.lean repro/MathlibTest/TermReduce.lean repro/MathlibTest/JacobiSymbol.lean repro/MathlibTest/trace.lean repro/MathlibTest/GalNotation.lean repro/MathlibTest/InstanceDiamonds/FieldTheory/SplittingField/Construction.lean repro/MathlibTest/InstanceDiamonds/FieldTheory/IsAlgClosed/AlgebraicClosure.lean repro/MathlibTest/TacticCheckInstancesSimps.lean repro/MathlibTest/FinsetBuilder.lean repro/MathlibTest/Clean.lean repro/MathlibTest/FunPropMinimal.lean repro/Ma
**Inspecting project README and status**
$ /bin/bash -lc "git status --short && sed -n '1,240p' README.md && sed -n '1,260p' Counterexamples.lean && rg -n \""'^(Theorem|THEOREM|Theorem [0-9]|Abstract|ABSTRACT|1'"\\.? |Introduction|Main theorem|Corollary|Proposition)\" ../paper.txt | sed -n '1,240p'" # mathlib4  [](https://mathlib-bors-ca18eefec4cb.herokuapp.com/repositories/16) [](https://leanprover.zulipchat.com) [](https://gitpod.io/#https://github.com/leanprover-community/mathlib4) [Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean theorem prover](https://leanprover.github.io). It contains both programming infrastructure and mathematics, as well as tactics that use the former and allow to develop the latter. ## Installation You can find detailed instructions to install Lean, mathlib, and supporting tools on [our website](https://leanprover-community.github.io/get_started.html). Alternatively, click on one of the buttons below to open a GitHub Codespace or a Gitpod workspace containing the project. [](https://codespaces.new/leanprover-community/mathlib4) [](https://gitpod.io/#https://github.com/leanprover-community/mathlib4) ## Using `mathlib4` as a dependency Please refer to [https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency](https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency) ## Experimenting Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/install/project.html)? For more pointers, see [Learning Lean](https://leanprover-community.github.io/learn.html). ## Documentation Besides the installation guides above and [Lean's general documentation](https://docs.lea
$ /bin/bash -lc "sed -n '1,190p' paper.txt && sed -n '190,430p' paper.txt && sed -n '430,760p' paper.txt" EXTREME VALUES OF QUADRATIC DIRICHLET L-FUNCTIONS ZIKANG DONG, WEIJIA WANG, HAO ZHANG, AND SHENGBO ZHAO arXiv:2607.20408v1 [math.NT] 22 Jul 2026 Abstract. In this article, we investigate extreme values of quadratic Dirichlet Lfunctions at the central point. We provide new extreme values of L( 12 , χd ) as d is large, which improves the recent result of Darbar and Maiti. 1. Introduction Throughout this paper, we write logj for the j-th iterated logarithm, such as log2 x = log log x, and log3 x = log log log x. In recent years, research on extreme values has advanced significantly, due to the resonance method introduced by Hilberdink [8] and developed by Soundararajan [10]. In [10], Soundararajan showed extreme values for the Riemann zeta function, the quadratic Dirichlet L-functions, and the L-functions for the cusp forms. For the Riemann zeta function, he showed for large T s log T 1 . max ζ( 2 + it)| ≥ exp 1 + o(1) T <|t|≤2T log2 T This was improved in 2017 by Bondarenko and Seip [2] s log T log3 T 1 1 max ζ( 2 + it)| ≥ exp √2 + o(1) . 0<|t|≤T log2 T This breakthrough was based on the connection between the Riemann zeta function and GCD sums, which was first observed by Aistleitner [1]. Bondarenko and Seip [3] also improved the constant √12 to 1 in 2018. After then, in 2019 La Bretèche and √ Tenenbaum [4] improved this to 2 and this is the best known result till now. (Zikang Dong) School of Mathematical Sciences, Soochow University, Suzhou 215006, P. R. China (Weijia Wang) School of Mathematics, Shandong University, Jinan 250100, P. R. China (Hao Zhang) School of Mathematics, Hunan University, Changsha 410082, P. R. China (Shengbo Zhao) School of Mathematical Sciences, Key Laboratory of Intelligent Computing and Applications (Tongji University), Ministry of Education, Tongji University, Shanghai 200092, China E-mail addresses: zikangdong@gmail.com, weijiawang@amss.ac.cn, zhanghaomath@hnu.edu.cn, shengbozhao@hotmail.com. 2020 Mathematics Subject Clas
**Planning formal theorem under GRH assumption** **Refining minimal theorem hypotheses and searching mathlib**
The paper’s central claim is Theorem 1.1: under GRH, the largest central value among fundamental discriminants \(X<|d|\le 2X\) is at least
\(\exp((1+o(1))\sqrt{\log X\,\log_3X/\log_2X})\).
Its proof is not self-contained: it imports an approximate functional equation, a GRH-dependent quadratic-character mean estimate, and a sharp GCD-sum construction. I’m now checking exactly which of these theories mathlib already exposes and whether the paper’s asymptotic conclusion can be derived faithfully from minimally named hypotheses.$ /bin/bash -lc "rg -n \"structure DirichletCharacter|def LFunction|Dirichlet.*L|LSeries|fundamental discriminant|FundamentalDiscriminant|quadratic.*character|kronecker|Kronecker|jacobiSym|Asymptotics.*IsLittleO|isLittleO.*exp|Filter.*atTop\" Mathlib | sed -n '1,260p'"
Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean:8:public import Mathlib.NumberTheory.LSeries.Dirichlet
Mathlib/NumberTheory/DirichletCharacter/Basic.lean:116: ∃ (h : d ∣ n) (χ₀ : DirichletCharacter R d), χ = changeLevel h χ₀
Mathlib/NumberTheory/DirichletCharacter/Basic.lean:138: ∃! χ' : DirichletCharacter R d, χ = changeLevel h.dvd χ' := by
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:9:public import Mathlib.NumberTheory.LSeries.Dirichlet
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:12:# The Euler Product for the Riemann Zeta Function and Dirichlet L-Series
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:22:The second result is `dirichletLSeries_eulerProduct` (with variants
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:23:`dirichletLSeries_eulerProduct_hasProd` and `dirichletLSeries_eulerProduct_tprod`),
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:24:which is the analogous statement for Dirichlet L-series.
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:79:open scoped LSeries.notation in
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:82: simp only [dirichletSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, LSeries,
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:83: LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs), div_eq_mul_inv]
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:108:open scoped LSeries.notation
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:110:/-- The Euler product for Dirichlet L-series, valid for `s.re > 1`.
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:112:theorem DirichletCharacter.LSeries_eulerProduct_hasProd {N : ℕ} (χ : DirichletCharacter ℂ N)
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:118:/-- The Euler product for Dirichlet L-series, valid for `s.re > 1`.
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean:120:theorem DirichletCharacter.LSeries_eulerProduct_tprod {N : ℕ} (χ : DirichletCharacter ℂ N)
M**Inspecting LSeries Dirichlet**
$ /bin/bash -lc "sed -n '1,260p' Mathlib/NumberTheory/LSeries/Dirichlet.lean && sed -n '1,220p' Mathlib/NumberTheory/DirichletCharacter/Basic.lean && rg -n \"def.*(kronecker|Kronecker)|fundamental.*discriminant|IsFundamental|Int.*discriminant|jacobi.*char|of.*jacobi|changeLevel\" Mathlib/NumberTheory | sed -n '1,300p'" /- Copyright (c) 2024 Michael Stoll. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Stoll -/ module public import Mathlib.NumberTheory.DirichletCharacter.Bounds public import Mathlib.NumberTheory.LSeries.Convolution public import Mathlib.NumberTheory.LSeries.Deriv public import Mathlib.NumberTheory.LSeries.Positivity public import Mathlib.NumberTheory.LSeries.RiemannZeta public import Mathlib.NumberTheory.SumPrimeReciprocals public import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt /-! # L-series of Dirichlet characters and arithmetic functions We collect some results on L-series of specific (arithmetic) functions, for example, the Möbius function `μ` or the von Mangoldt function `Λ`. In particular, we show that `L ↗Λ` is the negative of the logarithmic derivative of the Riemann zeta function on `re s > 1`; see `LSeries_vonMangoldt_eq_deriv_riemannZeta_div`. We also prove some general results on L-series associated to Dirichlet characters (i.e., Dirichlet L-series). For example, we show that the abscissa of absolute convergence equals `1` (see `DirichletCharacter.absicssaOfAbsConv_eq_one`) and that the L-series does not vanish on the open half-plane `re s > 1` (see `DirichletCharacter.LSeries_ne_zero_of_one_lt_re`). We deduce results on the Riemann zeta function (which is `L 1` or `L ↗ζ` on `re s > 1`) as special cases. ## Tags Dirichlet L-series, Möbius function, von Mangoldt function, Riemann zeta function -/ public section open scoped LSeries.notation /-- `δ` is the function underlying the arithmetic function `1`. -/ lemma ArithmeticFunction.one_eq_delta : ↗(1 : ArithmeticFunction ℂ) = δ := by ext simp [one_apply, LSeries.delta] section Moebius /-! ### The L-series of the Möbius function We show that `L μ s` converges absolutely if and only if `re s > 1`. -/ namespace ArithmeticFunction -- access notation `μ` open scoped Moebius open LSeries Nat Complex set_option backward.is
**Planning Kronecker symbol implementation** **Examining nonnegativity of quadratic central values** **Verifying theorem absolute value notation**
**Inspecting L-function analytic continuation**
$ /bin/bash -lc "sed -n '1,260p' Mathlib/NumberTheory/LSeries/DirichletContinuation.lean && rg -n \"DirichletContinuation|LFunction\" Mathlib/NumberTheory/LSeries | sed -n '1,260p' && rg -n \"Kronecker|kronecker|FundamentalDiscriminant|fundamental discriminant\" . -g '*.lean' | sed -n '1,160p'" /- Copyright (c) 2024 David Loeffler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: David Loeffler, Michael Stoll -/ module public import Mathlib.NumberTheory.LSeries.ZMod public import Mathlib.NumberTheory.DirichletCharacter.Basic public import Mathlib.NumberTheory.EulerProduct.DirichletLSeries /-! # Analytic continuation of Dirichlet L-functions We show that if `χ` is a Dirichlet character `ZMod N → ℂ`, for a positive integer `N`, then the L-series of `χ` has analytic continuation (away from a pole at `s = 1` if `χ` is trivial), and similarly for completed L-functions. All definitions and theorems are in the `DirichletCharacter` namespace. ## Main definitions * `LFunction χ s`: the L-function, defined as a linear combination of Hurwitz zeta functions. * `completedLFunction χ s`: the completed L-function, which for *almost* all `s` is equal to `LFunction χ s * gammaFactor χ s` where `gammaFactor χ s` is the archimedean Gamma-factor. * `rootNumber`: the global root number of the L-series of `χ` (for `χ` primitive; junk otherwise). ## Main theorems * `LFunction_eq_LSeries`: if `1 < re s` then the `LFunction` coincides with the naive `LSeries`. * `differentiable_LFunction`: if `χ` is nontrivial then `LFunction χ s` is differentiable everywhere. * `LFunction_eq_completed_div_gammaFactor`: we have `LFunction χ s = completedLFunction χ s / gammaFactor χ s`, unless `s = 0` and `χ` is the trivial character modulo 1. * `differentiable_completedLFunction`: if `χ` is nontrivial then `completedLFunction χ s` is differentiable everywhere. * `IsPrimitive.completedLFunction_one_sub`: the **functional equation** for Dirichlet L-functions, showing that if `χ` is primitive modulo `N`, then `completedLFunction χ s = N ^ (s - 1 / 2) * rootNumber χ * completedLFunction χ⁻¹ s`. -/ @[expose] public section open HurwitzZeta Complex Finset ZMod Filter open scoped Real Topology namespace DirichletCharacter variab
**Planning Dirichlet character construction** **Formulating Jacobi symbol character**
$ /bin/bash -lc "rg -n \"def .*jacobi|jacobi.*(Hom|Char|MulChar)|χ₄|χ₈|DirichletCharacter\" Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean | sed -n '1,300p' && sed -n '340,430p' Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean && sed -n '1,230p' Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean"
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:30:We define the primitive quadratic characters `χ₄` on `ZMod 4`
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:31:and `χ₈`, `χ₈'` on `ZMod 8`.
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:39:/-- Define the nontrivial quadratic character on `ZMod 4`, `χ₄`.
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:42:def χ₄ : MulChar (ZMod 4) ℤ where
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:52:/-- `χ₄` takes values in `{0, 1, -1}` -/
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:53:theorem isQuadratic_χ₄ : χ₄.IsQuadratic := by
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:57:/-- The value of `χ₄ n`, for `n : ℕ`, depends only on `n % 4`. -/
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:58:theorem χ₄_nat_mod_four (n : ℕ) : χ₄ n = χ₄ (n % 4 : ℕ) := by grind
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:60:/-- The value of `χ₄ n`, for `n : ℤ`, depends only on `n % 4`. -/
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:61:theorem χ₄_int_mod_four (n : ℤ) : χ₄ n = χ₄ (n % 4 : ℤ) := by
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:64:/-- An explicit description of `χ₄` on integers / naturals -/
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:65:theorem χ₄_int_eq_if_mod_four (n : ℤ) :
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:66: χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 := by
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:67: have help : ∀ m : ℤ, 0 ≤ m → m < 4 → χ₄ m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1 := by
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:72:theorem χ₄_nat_eq_if_mod_four (n : ℕ) :
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:73: χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 :=
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:74: mod_cast χ₄_int_eq_if_mod_four n
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:76:/-- Alternative description of `χ₄ n` for odd `n : ℕ` in terms of powers of `-1` -/
Mathlib/**Clarifying construction of MulChar from Jacobi symbol** **Analyzing factorization of quadratic characters for even discriminants**
**Planning quadratic character formalization** **Identifying potential errors in paper formulas**
**Verifying Rankin-type inequality for sum bounds** **Analyzing asymptotic bounds and constant factors**
**Analyzing S1 and S2 term bounds** **Planning resonance transfer theorem formalization**
**Defining ResonanceBounds concept and hypotheses** **Verifying GCD sum constants and bounds**
**Analyzing zeta constant improvements** **Clarifying square-free set constant bounds**
**Planning resonance algebra formalization** **Evaluating abstract lemma formulation** **Drafting partial formalization with hypotheses**
**Structuring hypotheses with consequences** **Planning PNT-based hypothesis formalization** **Reevaluating error term calculation**
**Verifying error bounds in weighted sums** **Identifying gamma factor discrepancy for negative discriminants**
**Analyzing formula validity for negative discriminants** **Planning numeric counterexample for Lemma 2.1**
**Analyzing Mellin transform discrepancy** **Identifying sign-restriction errors in lemma**
A concrete issue has surfaced in the paper’s own setup: Lemma 2.1 uses the even-character gamma factor \(\Gamma(1/4+s/2)\) and \(\sqrt d\), but Theorem 1.1 ranges over both signs of \(d\). For \(d<0\), \(\chi_d\) is odd and the correct factor is \(\Gamma(3/4+s/2)\) with \(\sqrt{|d|}\). I’m checking the PDF and testing \(d=-4\) numerically; in parallel I’m assessing whether the main argument can be repaired by splitting the two parities, since this may be a fixable lemma error rather than a false central theorem.$ /bin/bash -lc "command -v pdftoppm || true
pdfinfo paper.pdf | sed -n '1,40p'
pdftotext -layout -f 2 -l 3 paper.pdf - | sed -n '1,220p'
python3 - <<'PY'
try:
import mpmath as mp
print('mpmath', mp.__version__)
except Exception as e:
print('no mpmath',e)
PY"
no mpmath No module named 'mpmath'**Identifying and correcting algebra error in g2 definition** **Considering numerical alternatives to mpmath**
$ /bin/bash -lc "python3 - <<'PY'
mods=['scipy','sympy','numpy']
for m in mods:
try:
x=__import__(m); print(m, getattr(x,'__version__','ok'))
except Exception as e: print(m,'no')
PY
rg -n \"sum_primes|prime.*reciprocal|sum.*Prime|log.*log\" Mathlib/NumberTheory/SumPrimeReciprocals.lean | sed -n '1,240p'
sed -n '1,260p' Mathlib/NumberTheory/SumPrimeReciprocals.lean"
scipy no
sympy no
numpy no
18:expresses the sum as a sub-sum of the harmonic series, and `Nat.Primes.not_summable_one_div`,
19:which writes it as a sum over `Nat.Primes`. We also show that the sum of `p^r` for `r : ℝ`
44:@[to_additive /-- Reindex a sum over `Nat.Primes` as a sum over `ℕ`, extending `f` by `0`. -/]
75:lemma one_half_le_sum_primes_ge_one_div (k : ℕ) :
107: refine ((one_half_le_sum_primes_ge_one_div k).trans_lt <| LE.le.trans_lt ?_ hk).false
119:theorem Nat.Primes.not_summable_one_div : ¬ Summable (fun p : Nat.Primes ↦ (1 / p : ℝ)) := by
/-
Copyright (c) 2023 Michael Stoll. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Michael Stoll
-/
module
public import Mathlib.Algebra.Order.Group.Indicator
public import Mathlib.Analysis.PSeries
public import Mathlib.NumberTheory.SmoothNumbers
/-!
# The sum of the reciprocals of the primes diverges
We show that the sum of `1/p`, where `p` runs through the prime numbers, diverges.
We follow the elementary proof by Erdős that is reproduced in "Proofs from THE BOOK".
There are two versions of the main result: `not_summable_one_div_on_primes`, which
expresses the sum as a sub-sum of the harmonic series, and `Nat.Primes.not_summable_one_div`,
which writes it as a sum over `Nat.Primes`. We also show that the sum of `p^r` for `r : ℝ`
converges if and only if `r < -1`; see `Nat.Primes.summable_rpow`.
## References
See the sixth proof for the infinity of primes in Chapter 1 of [aigner1999proofs].
The proof is due to Erdős.
-/
public section
open Set Nat
open scoped Topology
section PrimeSums
variable {M : Type*} [CommMonoid M] [TopologicalSpace M] (f : ℕ → M)
omit [TopologicalSpace M] in
@[to_additive]
private lemma ite_prime_eq_mulIndicator :
(fun n : ℕ ↦ if n.Prime then f n else 1) = {n | n.Prime}.mulIndicator f := by
ext; simp [Set.mulIndicator_apply]
/-- Reindex a product over `Nat.Primes` as a product over `ℕ`, extending `f` by `1`. -/
@[to_additive /**Formalizing elementary prime product bound** **Planning QuadraticDatum structure design** **Simplifying theorem character dependency**
**Defining primitive quadratic character structure** **Designing algorithmic Kronecker definition** **Restricting discriminant to simplify character**
**Assessing character estimates for positive discriminants** **Formalizing asymptotic theorem for positive squarefree discriminants** **Defining jacobiChar on ZMod q with necessary lemmas**
$ /bin/bash -lc "sed -n '70,220p' Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean && sed -n '450,510p' Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean && rg -n \"IsPrimitive.*(χ₄|χ₈|jacobi)|isPrimitive|conductor.*quadratic|Quadratic.*primitive\" Mathlib/NumberTheory | sed -n '1,220p'"
We define the Jacobi symbol $\Bigl(\frac{a}{b}\Bigr)$ for integers `a` and natural numbers `b`
as the product of the Legendre symbols $\Bigl(\frac{a}{p}\Bigr)$, where `p` runs through the
prime divisors (with multiplicity) of `b`, as provided by `b.factors`. This agrees with the
Jacobi symbol when `b` is odd and gives less meaningful values when it is not (e.g., the symbol
is `1` when `b = 0`). This is called `jacobiSym a b`.
We define localized notation (scope `NumberTheorySymbols`) `J(a | b)` for the Jacobi
symbol `jacobiSym a b`.
-/
open Nat ZMod
-- Since we need the fact that the factors are prime, we use `List.pmap`.
/-- The Jacobi symbol of `a` and `b` -/
def jacobiSym (a : ℤ) (b : ℕ) : ℤ :=
(b.primeFactorsList.pmap (fun p pp => @legendreSym p ⟨pp⟩ a) fun _ pf =>
prime_of_mem_primeFactorsList pf).prod
-- Notation for the Jacobi symbol.
@[inherit_doc]
scoped[NumberTheorySymbols] notation "J(" a " | " b ")" => jacobiSym a b
open NumberTheorySymbols
/-!
### Properties of the Jacobi symbol
-/
namespace jacobiSym
/-- The symbol `J(a | 0)` has the value `1`. -/
@[simp]
theorem zero_right (a : ℤ) : J(a | 0) = 1 := by
simp only [jacobiSym, primeFactorsList_zero, List.prod_nil, List.pmap]
/-- The symbol `J(a | 1)` has the value `1`. -/
@[simp]
theorem one_right (a : ℤ) : J(a | 1) = 1 := by
simp only [jacobiSym, primeFactorsList_one, List.prod_nil, List.pmap]
/-- The Legendre symbol `legendreSym p a` with an integer `a` and a prime number `p`
is the same as the Jacobi symbol `J(a | p)`. -/
theorem legendreSym.to_jacobiSym (p : ℕ) [fp : Fact p.Prime] (a : ℤ) :
legendreSym p a = J(a | p) := by
simp only [jacobiSym, primeFactorsList_prime fp.1, List.prod_cons, List.prod_nil, mul_one,
List.pmap]
/-- The Jacobi symbol is multiplicative in its second argument. -/
theorem mul_right' (a : ℤ) {b₁ b₂ : ℕ} (hb₁ : b₁ ≠ 0) (hb₂ : b₂ ≠ 0) :
J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂) := by
rw [jacobiSym, ((perm_primeFactorsList_mul hb₁ hb₂).pmap _).p**Planning Jacobi character implementation** **Developing Lean counterexample for g2 product equality**
**Planning mpmath installation in /tmp**
$ /bin/bash -lc 'python3 -m pip install --target /tmp/extreme-values-mpmath mpmath' /usr/bin/python3: No module named pip
**Planning numerical incomplete gamma implementation** **Evaluating beta function via zeta relation**
$ /bin/bash -lc "python3 - <<'PY'
import math
ITMAX=10000; EPS=3e-15; FPMIN=1e-300
def gammaincc(a,x):
if x < 0 or a <=0: raise ValueError
if x == 0: return 1.0
gln=math.lgamma(a)
if x < a+1:
ap=a; s=1.0/a; d=s
for _ in range(ITMAX):
ap += 1; d *= x/ap; s += d
if abs(d) < abs(s)*EPS: break
P=s*math.exp(-x+a*math.log(x)-gln)
return 1-P
b=x+1-a; c=1/FPMIN; d=1/b; h=d
for i in range(1,ITMAX+1):
an=-i*(i-a); b +=2; d=an*d+b
if abs(d)<FPMIN:d=FPMIN
c=b+an/c
if abs(c)<FPMIN:c=FPMIN
d=1/d; delta=d*c; h*=delta
if abs(delta-1)<EPS: break
return math.exp(-x+a*math.log(x)-gln)*h
def chi4(n):
if n%2==0:return 0
return 1 if n%4==1 else -1
def rhs(a, terms=100):
return 2*sum(chi4(n)/math.sqrt(n)*gammaincc(a,math.pi*(n/2)**2) for n in range(1,terms+1))
for a in (.25,.75):
print(a, format(rhs(a),'.17g'))
print('difference', rhs(.25)-rhs(.75))
# Validate gamma Q implementation at known Q(1,x)=e"'^-x and Q(1/2,x)=erfc(sqrt x)
for x in [0.1,1,4,10]: print(x,gammaincc(1,x)-math.exp(-x),gammaincc(.5,x)-math.erfc(math.sqrt(x)))
PY'
0.25 0.18901770464767276
0.75 0.66769145718960932
difference -0.47867375254193656
0.1 0.0 0.0
1 -1.1102230246251565e-16 1.942890293094024e-16
4 3.469446951953614e-18 -7.806255641895632e-18
10 6.776263578034403e-21 6.776263578034403e-21**Planning theorem repair and formalization** **Designing abstract resonance moment hypothesis** **Preparing partial results with counterexamples**
**Defining IsFundamentalDiscriminant property** **Defining ExtremeValueClaim and character structures**
**Defining extreme values theorem** **Refining resonance moment hypotheses** **Applying weighted average lemma conditions**
**Defining ResonanceWitness structure** **Planning formal gamma factor construction**
$ /bin/bash -lc "rg -n \"def comp|lemma.*comp.*IsQuadratic|IsQuadratic.*comp|χ₄.*Odd|odd_χ|χ₄.*primitive\" Mathlib/NumberTheory/MulChar/Basic.lean Mathlib/NumberTheory/LegendreSymbol -g '*.lean' | sed -n '1,260p'
rg -n \"def Odd|namespace Odd|Odd.*gamma|odd_iff\" Mathlib/NumberTheory/DirichletCharacter Mathlib/NumberTheory/MulChar | sed -n '1,220p'
rg -n \"mobius.*(two|prime)|moebius_apply_prime|Nat.mobius\" Mathlib/NumberTheory | sed -n '1,160p'"
Mathlib/NumberTheory/MulChar/Basic.lean:513:theorem IsQuadratic.comp {χ : MulChar R R'} (hχ : χ.IsQuadratic) (f : R' →+* R'') :
Mathlib/NumberTheory/DirichletCharacter/Basic.lean:533:def Odd : Prop := ψ (-1) = -1
Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean:109:theorem moebius_apply_prime {p : ℕ} (hp : p.Prime) : μ p = -1 := by
Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean:112:theorem moebius_apply_prime_pow {p k : ℕ} (hp : p.Prime) (hk : k ≠ 0) :
Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean:115: · rw [h, pow_one, moebius_apply_prime hp]
Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean:123: rw [moebius_apply_prime_pow hp hk.ne', if_neg]
Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean:149: rw [pmul_apply, intCoe_apply, ArithmeticFunction.moebius_apply_prime
Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean:165: simp [moebius_apply_prime_pow, hp.ne_one, hn.ne', hp, hn]
Mathlib/NumberTheory/LSeries/Dirichlet.lean:67: · simp [hn, hn.ne_zero, moebius_apply_prime hn, push_cast, neg_div]$ /bin/bash -lc "sed -n '480,550p' Mathlib/NumberTheory/MulChar/Basic.lean && sed -n '510,565p' Mathlib/NumberTheory/DirichletCharacter/Basic.lean && rg -n \"def comp\" Mathlib/NumberTheory/MulChar -g '*.lean' Mathlib/Algebra | head -50"
@[simps]
def ringHomCompHom (f : R' →+* R'') : MulChar R R' →* MulChar R R'' where
toFun χ := χ.ringHomComp f
map_one' := ringHomComp_one f
map_mul' _ _ := ringHomComp_mul _ _ f
lemma ringHomComp_zpow (χ : MulChar R R') (f : R' →+* R'') (n : ℤ) :
χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f :=
((ringHomCompHom f).map_zpow χ n).symm
/-- If `a` is a unit and `n : ℤ`, then `(χ ^ n) a = χ (a ^ n)`. -/
theorem zpow_apply_coe {R : Type*} [CommGroupWithZero R] {R' : Type*} [CommRing R']
(χ : MulChar R R') (n : ℤ) (a : Rˣ) : (χ ^ n) a = χ (a ^ n : Rˣ) := by
obtain ⟨m, rfl | rfl⟩ := Int.eq_nat_or_neg n
· simp [pow_apply_coe]
· simp [pow_apply_coe, inv_apply', ← inv_pow]
lemma injective_ringHomComp {f : R' →+* R''} (hf : Function.Injective f) :
Function.Injective (ringHomComp (R := R) · f) := by
simpa
only [Function.Injective, MulChar.ext_iff, ringHomComp, coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
using fun χ χ' h a ↦ hf (h a)
lemma ringHomComp_eq_one_iff {f : R' →+* R''} (hf : Function.Injective f) {χ : MulChar R R'} :
χ.ringHomComp f = 1 ↔ χ = 1 := by
conv_lhs => rw [← (show (1 : MulChar R R').ringHomComp f = 1 by simp)]
exact (injective_ringHomComp hf).eq_iff
lemma ringHomComp_ne_one_iff {f : R' →+* R''} (hf : Function.Injective f) {χ : MulChar R R'} :
χ.ringHomComp f ≠ 1 ↔ χ ≠ 1 :=
(ringHomComp_eq_one_iff hf).not
/-- Composition with a ring homomorphism preserves the property of being a quadratic character. -/
theorem IsQuadratic.comp {χ : MulChar R R'} (hχ : χ.IsQuadratic) (f : R' →+* R'') :
(χ.ringHomComp f).IsQuadratic := by
intro a
rcases hχ a with (ha | ha | ha) <;> simp [ha]
/-- The inverse of a quadratic character is itself. → -/
theorem IsQuadratic.inv {χ : MulChar R R'} (hχ : χ.IsQuadratic) : χ⁻¹ = χ := by
ext x
rw [inv_apply_eq_inv]
rcases hχ x with (h₀ | h₁ | h₂)
· rw [h₀, Ring.inverse_zero]
· rw [h₁, Ring.inverse_one]
· -- Porting note (#11573): was `by norm_cast`
have : (-1 : R') =**Testing chiMinusFour oddness lemma**
The PDF confirms both defects are literal, not extraction artifacts. There is also an elementary sign error immediately after Lemma 2.2: the paper defines \(g_2(n)=\sum_{q\mid n}\mu(q)^2/q^{1/2+\varepsilon}\), whose Euler product has \(1+\cdots\), but prints \(1-\cdots\). At \(n=2,\varepsilon=1/2\), the two sides are \(3/2\) and \(1/2\). Both errors look repairable asymptotically, so I’m not treating them as a counterexample to Theorem 1.1; I’m formalizing the exact failures and the rigorous resonance-to-maximum core while continuing to test a parity-split repair.**Planning compilation step**
$ /bin/bash -lc 'lake env lean ExtremeValues.lean' ExtremeValues.lean:29:2: error: unsolved goals case inr hm : True ⊢ False ExtremeValues.lean:123:32: error: Application type mismatch: The argument d has type ℤ of sort `Type` but is expected to have type ∃ i ∈ R.support, R.weight i * value i < R.weight i * target of sort `Prop` in the application Finset.sum_lt_sum hle d ExtremeValues.lean:125:2: error: linarith failed to find a contradiction value : ℤ → ℝ X : ℕ target : ℝ R : ResonanceWitness value X target h : ∀ (d : ℤ), IsFundamentalDiscriminant d → X < d.natAbs → d.natAbs ≤ 2 * X → value d < target hle : ∀ d ∈ R.support, R.weight d * value d ≤ R.weight d * target hsum : ∑ d ∈ R.support, R.weight d * value d ≤ target * ∑ d ∈ R.support, R.weight d heq : ∑ d ∈ R.support, R.weight d * value d = ∑ i ∈ R.support, target * R.weight i d : ℤ hd : d ∈ R.support hwd : 0 < R.weight d hstrict : R.weight d * value d < R.weight d * target this : ∑ d ∈ R.support, R.weight d * value d < ∑ d ∈ R.support, R.weight d * target ⊢ False failed ExtremeValues.lean:159:15: warning: `Set.mem_setOf_eq` has been deprecated: Use `Set.mem_ofPred_eq` instead ExtremeValues.lean:161:20: error: omega could not prove the goal: a possible counterexample may satisfy the constraints f ≥ 0 e ≥ 0 b + e ≤ -1 a ≥ 0 a - f ≤ -1 2*a - e ≥ 0 2*a - f ≥ 0 where a := ↑X b := Int.ofNat (2 * X) e := z f := d ExtremeValues.lean:161:20: error: omega could not prove the goal: a possible counterexample may satisfy the constraints f ≥ 0 b ≥ 0 b - e ≥ 1 a ≥ 0 a - f ≤ -1 2*a - b ≥ 0 2*a - f ≥ 0 where a := ↑X b := z e := Int.ofNat (2 * X) f := d ExtremeValues.lean:159:15: warning: This simp argument is unused: Set.mem_setOf_eq Hint: Omit it from the simp argument list. [apply] simp only [Set.mem_Icc] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
$ /bin/bash -lc 'lake env lean PaperErrors.lean'
PaperErrors.lean:28:32: error: unsolved goals
⊢ ∑ q ∈ Finset.Ico 1 3 with q ∣ 2, ↑(μ q) ^ 2 / ↑q = 3 / 2
PaperErrors.lean:37:43: error: unsolved goals
⊢ ¬∑ q ∈ Finset.Ico 1 3 with q ∣ 2, ↑(μ q) ^ 2 / ↑q = 1 / 2
PaperErrors.lean:46:43: error: unsolved goals
⊢ ↑(match -1 with
| 0 => 0
| 2 => 0
| 1 => 1
| 3 => -1) =
-1**Fixing zero-case contradiction and refining sum equality** **Simplifying sum equality and searching bounds lemma**
$ /bin/bash -lc "# inspect signatures and relevant lemmas
rg -n \"theorem sum_lt_sum|lemma sum_lt_sum\" Mathlib/Algebra/Order/BigOperators/Group/Finset.lean Mathlib | head -30
rg -n \"natAbs.*(le|lt).*iff|neg.*natAbs|ofNat.*natAbs|natAbs_ofNat\" Mathlib/Data/Int Mathlib/Algebra/Order | sed -n '1,220p'
# query check via temporary file
sed -n '1,120p' Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean"
Mathlib/Data/ENNReal/BigOperators.lean:128:theorem sum_lt_sum_of_nonempty {s : Finset α} (hs : s.Nonempty) {f g : α → ℝ≥0∞}
Mathlib/Data/ENat/BigOperators.lean:80:theorem sum_lt_sum_of_nonempty {s : Finset α} (hs : s.Nonempty) {f g : α → ℕ∞}
Mathlib/Data/Int/Lemmas.lean:43:theorem natAbs_lt_iff_sq_lt {a b : ℤ} : a.natAbs < b.natAbs ↔ a ^ 2 < b ^ 2 := by
Mathlib/Data/Int/Lemmas.lean:45: exact natAbs_lt_iff_mul_self_lt
Mathlib/Data/Int/Lemmas.lean:47:theorem natAbs_le_iff_sq_le {a b : ℤ} : a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2 := by
Mathlib/Data/Int/Lemmas.lean:49: exact natAbs_le_iff_mul_self_le
Mathlib/Data/Int/Lemmas.lean:61: simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg ha (neg_nonneg_of_nonpos hb)
Mathlib/Data/Int/Lemmas.lean:65: simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) hb
Mathlib/Data/Int/Lemmas.lean:92: natAbs_lt_natAbs_of_nonneg_of_lt (Right.nonneg_neg_iff.mpr hb) (neg_lt_neg_iff.mpr hab)
Mathlib/Data/Int/Order/Lemmas.lean:30:theorem natAbs_lt_iff_mul_self_lt {a b : ℤ} : a.natAbs < b.natAbs ↔ a * a < b * b := by
Mathlib/Data/Int/Order/Lemmas.lean:34:theorem natAbs_le_iff_mul_self_le {a b : ℤ} : a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b := by
Mathlib/Data/Int/GCD.lean:163: | ofNat m, n => m.gcdA n.natAbs
Mathlib/Data/Int/GCD.lean:168: | m, ofNat n => m.natAbs.gcdB n
Mathlib/Data/Int/Fib/Lemmas.lean:35: natAbs_neg, natAbs_natCast, ← fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq]
/-
Copyright (c) 2020 Aaron Anderson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aaron Anderson
-/
module
public import Mathlib.Algebra.Order.Ring.Abs
public import Mathlib.NumberTheory.ArithmeticFunction.Misc
/-!
# The Möbius function and Möbius inversion
## Main Definitions
* `μ` is the Möbius function (spelled `moebius` in code; the notation `μ` is available by opening
the namespace `ArithmeticFunction.Moebius`).
## Main Results
* Several **Exploring finite set proof via natAbs**
$ /bin/bash -lc "rg -n \"finite.*natAbs|natAbs.*finite|natAbs.*Icc|natAbs_le\" Mathlib | sed -n '1,220p'
rg -n \"sum_lt_sum \\{\" Mathlib/Algebra Mathlib/Data/Finset | head -50"
Mathlib/Data/Int/Lemmas.lean:47:theorem natAbs_le_iff_sq_le {a b : ℤ} : a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2 := by
Mathlib/Data/Int/Lemmas.lean:49: exact natAbs_le_iff_mul_self_le
Mathlib/Data/Int/Order/Lemmas.lean:34:theorem natAbs_le_iff_mul_self_le {a b : ℤ} : a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b := by
Mathlib/Data/Int/Basic.lean:86:lemma natAbs_le_of_dvd_ne_zero (hmn : m ∣ n) (hn : n ≠ 0) : natAbs m ≤ natAbs n :=
Mathlib/NumberTheory/FLT/Four.lean:246: apply lt_of_le_of_lt (Int.natAbs_le_self_sq i)
Mathlib/Algebra/Order/Group/Unbundled/Int.lean:54:lemma natAbs_le_self_sq (a : ℤ) : (Int.natAbs a : ℤ) ≤ a ^ 2 := by
Mathlib/Algebra/Order/Group/Unbundled/Int.lean:59:alias natAbs_le_self_pow_two := natAbs_le_self_sq
Mathlib/Algebra/Order/Group/Unbundled/Int.lean:61:lemma le_self_sq (b : ℤ) : b ≤ b ^ 2 := le_trans le_natAbs (natAbs_le_self_sq _)
Mathlib/Algebra/Order/Group/Unbundled/Int.lean:85: have := Int.natAbs_le_of_dvd_ne_zero h1 h
Mathlib/RingTheory/Multiplicity.lean:758:theorem Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs {a b : ℤ} :
Mathlib/RingTheory/Multiplicity.lean:762:theorem Int.finiteMultiplicity_iff {a b : ℤ} : FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0 := by
Mathlib/RingTheory/Multiplicity.lean:763: rw [finiteMultiplicity_iff_finiteMultiplicity_natAbs, Nat.finiteMultiplicity_iff,**Exploring lemmas for bounding with Int.le_natAbs**
$ /bin/bash -lc "rg -n \"le_natAbs|natAbs.*le|neg_natAbs\" Mathlib/Data/Int Mathlib/Algebra/Order/Group/Unbundled/Int.lean | sed -n '1,160p'
rg -n \"sum_lt_sum.*∀|sum_lt_sum.*exists|sum_lt_sum\" Mathlib/Algebra/Order/BigOperators Mathlib/Algebra/Order | head -100"
Mathlib/Algebra/Order/Group/Unbundled/Int.lean:54:lemma natAbs_le_self_sq (a : ℤ) : (Int.natAbs a : ℤ) ≤ a ^ 2 := by
Mathlib/Algebra/Order/Group/Unbundled/Int.lean:59:alias natAbs_le_self_pow_two := natAbs_le_self_sq
Mathlib/Algebra/Order/Group/Unbundled/Int.lean:61:lemma le_self_sq (b : ℤ) : b ≤ b ^ 2 := le_trans le_natAbs (natAbs_le_self_sq _)
Mathlib/Algebra/Order/Group/Unbundled/Int.lean:85: have := Int.natAbs_le_of_dvd_ne_zero h1 h
Mathlib/Data/Int/Lemmas.lean:47:theorem natAbs_le_iff_sq_le {a b : ℤ} : a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2 := by
Mathlib/Data/Int/Lemmas.lean:49: exact natAbs_le_iff_mul_self_le
Mathlib/Data/Int/Lemmas.lean:69:theorem natAbs_coe_sub_coe_le_of_le {a b n : ℕ} (a_le_n : a ≤ n) (b_le_n : b ≤ n) :
Mathlib/Data/Int/Order/Lemmas.lean:34:theorem natAbs_le_iff_mul_self_le {a b : ℤ} : a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b := by
Mathlib/Data/Int/NatAbs.lean:20:* `Int.natAbsHom`: `Int.natAbs` bundled as a `MonoidWithZeroHom`.
Mathlib/Data/Int/NatAbs.lean:27:/-- `Int.natAbs` as a bundled `MonoidWithZeroHom`. -/
Mathlib/Data/Int/NatAbs.lean:38:lemma natAbs_natCast_sub_natCast_of_le {a b : ℕ} (h : a ≤ b) : Int.natAbs (↑a - ↑b) = b - a := by
Mathlib/Data/Int/Basic.lean:86:lemma natAbs_le_of_dvd_ne_zero (hmn : m ∣ n) (hn : n ≠ 0) : natAbs m ≤ natAbs n :=
Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean:121:@[to_additive sum_lt_sum]
Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean:128:@[to_additive sum_lt_sum_of_nonempty]
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean:481:@[to_additive sum_lt_sum]
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean:489:@[to_additive (attr := gcongr) sum_lt_sum_of_nonempty]
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean:498:add_decl_doc sum_lt_sum_of_nonempty
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean:500:@[to_additive sum_lt_sum_of_subset]
Mathlib/Algebra/Order/BigOperators/Group/List.lean:68:@[to_additive sum_lt_sum]
Mathlib/Algebra/Order/BigOperators/Expect.lean:117: smul_lt_smul$ /bin/bash -lc "sed -n '470,495p' Mathlib/Algebra/Order/BigOperators/Group/Finset.lean && # lean check common names
true"
lemma one_lt_prod_iff {ι M : Type*} [CommMonoid M] [PartialOrder M] [CanonicallyOrderedMul M]
{f : ι → M} {s : Finset ι} : 1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x :=
have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
Finset.one_lt_prod_iff_of_one_le <| fun _ _ => one_le
end CanonicallyOrderedMul
section OrderedCancelCommMonoid
variable [CommMonoid M] [Preorder M] [IsOrderedCancelMonoid M] {f g : ι → M} {s t : Finset ι}
@[to_additive sum_lt_sum]
theorem prod_lt_prod' [MulLeftStrictMono M] (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
∏ i ∈ s, f i < ∏ i ∈ s, g i :=
Multiset.prod_lt_prod' hle hlt
/-- In an ordered commutative monoid, if each factor `f i` of one nontrivial finite product is
strictly less than the corresponding factor `g i` of another nontrivial finite product, then
`s.prod f < s.prod g`. -/
@[to_additive (attr := gcongr) sum_lt_sum_of_nonempty]
theorem prod_lt_prod_of_nonempty' [MulLeftStrictMono M] (hs : s.Nonempty)
(hlt : ∀ i ∈ s, f i < g i) :
∏ i ∈ s, f i < ∏ i ∈ s, g i :=
Multiset.prod_lt_prod_of_nonempty' (by aesop) hlt
/-- In an ordered additive commutative monoid, if each summand `f i` of one nontrivial finite sum is**Planning finite shell construction** **Defining shellFinset and shellMax with bounds**
$ /bin/bash -lc 'lake env lean Check.lean'
Int.le_natAbs {a : ℤ} : a ≤ ↑a.natAbs
Check.lean:3:7: error(lean.unknownIdentifier): Unknown constant `Int.neg_natAbs_le`
Check.lean:4:7: error(lean.unknownIdentifier): Unknown constant `Int.natAbs_ofNat`
Int.natAbs_natCast (n : ℕ) : (↑n).natAbs = n
Finset.le_max'.{u_2} {α : Type u_2} [LinearOrder α] (s : Finset α) (x : α) (H2 : x ∈ s) : x ≤ s.max' ⋯
Finset.max'_mem.{u_2} {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : s.max' H ∈ s
Finset.sum_lt_sum.{u_1, u_4} {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Preorder M] [IsOrderedCancelAddMonoid M]
{f g : ι → M} {s : Finset ι} [AddLeftStrictMono M] (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
∑ i ∈ s, f i < ∑ i ∈ s, g i
Set.Finite.bddAbove.{u} {α : Type u} [Preorder α] [IsDirectedOrder α] [Nonempty α] {s : Set α} (hs : s.Finite) :
BddAbove s
Check.lean:10:7: error(lean.unknownIdentifier): Unknown constant `Int.natAbs_le`**Deriving bounds using Int.le_natAbs and omega** **Fixing divisor set and ZMod coercion in tests**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean ExtremeValues.lean' ExtremeValues.lean:165:54: error: mod_cast has type z.natAbs ≤ 2 * X but is expected to have type (-z).natAbs ≤ 2 * X ExtremeValues.lean:166:20: error: omega could not prove the goal: a possible counterexample may satisfy the constraints f ≥ 0 b ≥ 0 b + e ≤ -1 a ≥ 0 a - f ≤ -1 2*a - b ≥ 0 2*a - f ≥ 0 2*a + b ≥ 0 where a := ↑X b := z e := Int.ofNat (2 * X) f := d
$ /bin/bash -lc 'lake env lean PaperErrors.lean' PaperErrors.lean:29:14: error: unexpected identifier after decimal point; consider parenthesizing the number PaperErrors.lean:29:7: error: Missing cases: PaperErrors.lean:28:32: error: unsolved goals hdiv : sorry ⊢ g2AtHalf 2 = 3 / 2 PaperErrors.lean:41:20: error: unexpected identifier after decimal point; consider parenthesizing the number PaperErrors.lean:41:13: error: Missing cases: PaperErrors.lean:40:6: error: unsolved goals hdiv : sorry ⊢ g2AtHalf 2 = 3 / 2 PaperErrors.lean:39:43: error: unsolved goals ⊢ 3 / 2 ≠ printedProductAtHalf 2
**Refining inequality negation steps** **Completing proof with endpoint simplifications**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean ExtremeValues.lean' ExtremeValues.lean:166:44: error: mod_cast has type z.natAbs ≤ 2 * X but is expected to have type (-z).natAbs ≤ 2 * X
$ /bin/bash -lc 'lake env lean PaperErrors.lean'
PaperErrors.lean:28:32: error: unsolved goals
hdiv : Nat.divisors 2 = {1, 2}
⊢ 1 + ↑(μ 2) ^ 2 / 2 = 3 / 2
PaperErrors.lean:40:6: error: unsolved goals
hdiv : Nat.divisors 2 = {1, 2}
⊢ 1 + ↑(μ 2) ^ 2 / 2 = 3 / 2**Refactoring cast and rewriting moebius function**
$ /bin/bash -lc 'lake env lean ExtremeValues.lean'
$ /bin/bash -lc 'lake env lean PaperErrors.lean'
PaperErrors.lean:31:6: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
μ 2
in the target expression
∑ q ∈ {1, 2}, ↑(μ q) ^ 2 / ↑q = 3 / 2
hdiv : Nat.divisors 2 = {1, 2}
⊢ ∑ q ∈ {1, 2}, ↑(μ q) ^ 2 / ↑q = 3 / 2
PaperErrors.lean:44:12: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
μ 2
in the target expression
∑ q ∈ {1, 2}, ↑(μ q) ^ 2 / ↑q = 3 / 2
hdiv : Nat.divisors 2 = {1, 2}
⊢ ∑ q ∈ {1, 2}, ↑(μ q) ^ 2 / ↑q = 3 / 2**Preparing finset sum simplification**
$ /bin/bash -lc 'lake env lean PaperErrors.lean' PaperErrors.lean:31:54: error(lean.unknownIdentifier): Unknown identifier `one_ne_ofNat` PaperErrors.lean:31:2: error: `simp` made no progress PaperErrors.lean:46:60: error(lean.unknownIdentifier): Unknown identifier `one_ne_ofNat` PaperErrors.lean:46:8: error: `simp` made no progress
**Clarifying nested sum expression structure** **Confirming single sum notation and patch**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean PaperErrors.lean'
PaperErrors.lean:32:46: error: unsolved goals
hdiv : Nat.divisors 2 = {1, 2}
⊢ Nat.Prime 2
PaperErrors.lean:46:52: error: unsolved goals
hdiv : Nat.divisors 2 = {1, 2}
⊢ Nat.Prime 2**Fixing prime number patch for Nat.Prime**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean PaperErrors.lean'
**Planning Jacobi character formalization**
$ /bin/bash -lc "rg -n \"def .*: MulChar \\(ZMod [a-zA-Z0-9_]+\\)\" Mathlib/NumberTheory | sed -n '1,160p'
rg -n \"val_mul|natCast_zmod_val|intCast_zmod|val_one|val_eq\" Mathlib/Data/ZMod | sed -n '1,240p'
rg -n \"def lift.*ZMod|ZMod.lift\" Mathlib/Data/ZMod | sed -n '1,160p'"
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:42:def χ₄ : MulChar (ZMod 4) ℤ where
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:118:def χ₈ : MulChar (ZMod 8) ℤ where
Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean:157:def χ₈' : MulChar (ZMod 8) ℤ where
Mathlib/Data/ZMod/IntUnitsPower.lean:47: rw [← pow_mul, ZMod.val_mul, ← Int.units_pow_eq_pow_mod_two, mul_comm]
Mathlib/Data/ZMod/ValMinAbs.lean:40: · rw [Int.cast_natCast, natCast_zmod_val]
Mathlib/Data/ZMod/ValMinAbs.lean:41: · rw [Int.cast_sub, Int.cast_natCast, natCast_zmod_val, Int.cast_natCast, natCast_self,
Mathlib/Data/ZMod/ValMinAbs.lean:84: · rw [← intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]
Mathlib/Data/ZMod/ValMinAbs.lean:119: · rw [Int.natAbs_natCast, natCast_zmod_val]
Mathlib/Data/ZMod/ValMinAbs.lean:121: Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
Mathlib/Data/ZMod/ValMinAbs.lean:152:lemma val_eq_ite_valMinAbs [NeZero n] (a : ZMod n) :
Mathlib/Data/ZMod/Coprime.lean:32: intCast_zmod_eq_zero_iff_dvd]
Mathlib/Data/ZMod/Defs.lean:70: Fin.eq_of_val_eq <|
Mathlib/Data/ZMod/Defs.lean:86: Fin.eq_of_val_eq <|
Mathlib/Data/ZMod/Units.lean:112: rw [← natCast_zmod_val a, ← natCast_zmod_val u.1, ha₀, ← Nat.cast_mul,
Mathlib/Data/ZMod/Units.lean:123: rw [← natCast_zmod_val x]
Mathlib/Data/ZMod/Units.lean:133: rw [natCast_zmod_val, coe_int_mul_inv_eq_one h]
Mathlib/Data/ZMod/Basic.lean:77:theorem val_one' : (1 : ZMod 0).val = 1 :=
Mathlib/Data/ZMod/Basic.lean:85:theorem val_mul' {m n : ZMod 0} : (m * n).val = m.val * n.val :=
Mathlib/Data/ZMod/Basic.lean:205:theorem natCast_zmod_val {n : ℕ} [NeZero n] (a : ZMod n) : (a.val : ZMod n) = a := by
Mathlib/Data/ZMod/Basic.lean:208: · apply Fin.cast_val_eq_self
Mathlib/Data/ZMod/Basic.lean:211: natCast_zmod_val
Mathlib/Data/ZMod/Basic.lean:220:theorem intCast_zmod_cast (a : ZMod n) : ((cast a : ℤ) : ZMod n) = a := by
Mathlib/Data/ZMod/Basic.lean:224: rw [Int.cast_natC**Defining toFun with val and proving properties**
$ /bin/bash -lc "sed -n '660,710p' Mathlib/Data/ZMod/Basic.lean && rg -n \"isUnit_iff_coprime\" Mathlib/Data/ZMod | sed -n '1,120p'
rg -n \"gcd.*natCast|natCast.*gcd\" Mathlib/Data/Int/GCD.lean | sed -n '1,140p'"
Nat.mod_eq_of_lt (val_lt _)]
rwa [Nat.mod_eq_of_lt (val_lt _), Nat.mod_eq_of_lt (val_lt _)]
theorem val_add_of_le {n : ℕ} [NeZero n] {a b : ZMod n} (h : n ≤ a.val + b.val) :
(a + b).val = a.val + b.val - n := by
rw [val_add_val_of_le h]
exact eq_tsub_of_add_eq rfl
theorem val_add_le {n : ℕ} (a b : ZMod n) : (a + b).val ≤ a.val + b.val := by
cases n
· simpa [ZMod.val] using! Int.natAbs_add_le _ _
· simpa [ZMod.val_add] using! Nat.mod_le _ _
theorem val_mul {n : ℕ} (a b : ZMod n) : (a * b).val = a.val * b.val % n := by
cases n
· rw [Nat.mod_zero]
apply Int.natAbs_mul
· apply Fin.val_mul
theorem val_mul_le {n : ℕ} (a b : ZMod n) : (a * b).val ≤ a.val * b.val := by
rw [val_mul]
apply Nat.mod_le
theorem val_mul_of_lt {n : ℕ} {a b : ZMod n} (h : a.val * b.val < n) :
(a * b).val = a.val * b.val := by
rw [val_mul]
apply Nat.mod_eq_of_lt h
theorem val_mul_iff_lt {n : ℕ} [NeZero n] (a b : ZMod n) :
(a * b).val = a.val * b.val ↔ a.val * b.val < n := by
constructor <;> intro h
· rw [← h]; apply ZMod.val_lt
· apply ZMod.val_mul_of_lt h
instance nontrivial (n : ℕ) [Fact (1 < n)] : Nontrivial (ZMod n) :=
⟨⟨0, 1, fun h =>
zero_ne_one <|
calc
0 = (0 : ZMod n).val := by rw [val_zero]
_ = (1 : ZMod n).val := congr_arg ZMod.val h
_ = 1 := val_one n
⟩⟩
instance nontrivial' : Nontrivial (ZMod 0) := by
delta ZMod; infer_instance
lemma one_eq_zero_iff {n : ℕ} : (1 : ZMod n) = 0 ↔ n = 1 := by
rw [← Nat.cast_one, natCast_eq_zero_iff, Nat.dvd_one]
/-- The inversion on `ZMod n`.
It is setup in such a way that `a * a⁻¹` is equal to `gcd a.val n`.
Mathlib/Data/ZMod/Units.lean:77: rw [isUnit_iff_coprime]
Mathlib/Data/ZMod/Units.lean:103: refine (isUnit_iff_coprime _ _).mpr (Nat.isCoprime_iff_coprime.mp ?_)
Mathlib/Data/ZMod/Basic.lean:809:lemma isUnit_iff_coprime (m n : ℕ) : IsUnit (m : ZMod n) ↔ m.Coprime n := by
Mathlib/Data/ZMod/Basic.lean:822: rw [isUnit_iff_coprime, Nat.**Refining gcd and coprimality proof**
$ /bin/bash -lc 'lake env lean Check.lean'
Check.lean:2:7: error(lean.unknownIdentifier): Unknown constant `Int.gcd_ofNat`
Check.lean:3:7: error(lean.unknownIdentifier): Unknown constant `Int.gcd_natCast_left`
Check.lean:4:7: error(lean.unknownIdentifier): Unknown constant `Int.gcd_natCast_right`
Nat.coprime_iff_gcd_eq_one {m n : ℕ} : m.Coprime n ↔ m.gcd n = 1
ZMod.isUnit_iff_coprime (m n : ℕ) : IsUnit ↑m ↔ m.Coprime n
Int.natCast_emod (m n : ℕ) : ↑(m % n) = ↑m % ↑n
Int.natCast_mod (m n : ℕ) : ↑(m % n) = ↑m % ↑n**Defining gcd and proving gcd theorem**
$ /bin/bash -lc "rg -n \"theorem gcd.*nat|lemma gcd.*nat|gcd_eq_natAbs|natAbs.*gcd|gcd.*ofNat\" Mathlib/Data/Int/GCD.lean | sed -n '1,220p'" 134: refine ⟨(n.gcdA k % k).toNat, ?_, (Int.ofNat_inj.1 ?_).trans key.symm⟩ 159:theorem gcd_def (i j : ℤ) : gcd i j = Nat.gcd i.natAbs j.natAbs := rfl 168: | m, ofNat n => m.natAbs.gcdB n 169: | m, -[n+1] => -m.natAbs.gcdB n.succ
**Testing integer character compilation**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean QuadraticCharacters.lean' QuadraticCharacters.lean:20:23: error: Application type mismatch: The argument LT.lt.ne hq has type 1 ≠ q but is expected to have type q ≠ 1 in the application ZMod.val_one'' (LT.lt.ne hq) QuadraticCharacters.lean:29:8: error(lean.synthInstanceFailed): failed to synthesize instance of type class NeZero q Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. QuadraticCharacters.lean:32:10: error(lean.synthInstanceFailed): failed to synthesize instance of type class NeZero q Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. QuadraticCharacters.lean:28:23: error: unsolved goals q : ℕ hq : 1 < q a : ZMod q ha : ¬IsUnit a hgcd : (↑a.val).gcd ↑q = 1 ⊢ IsUnit a q : ℕ hq : 1 < q a : ZMod q ha : ¬IsUnit a ⊢ NeZero q QuadraticCharacters.lean:44:6: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern J(↑n % ↑q | q) in the target expression J(↑(↑n).val | q) = J(↑n | q) q n : ℕ hq : 1 < q ⊢ J(↑(↑n).val | q) = J(↑n | q) QuadraticCharacters.lean:56:2: error: Type mismatch ?m.16 ∘ ⇑(Int.castRingHom ℂ) has type ℤ → ?m.14 but is expected to have type MulChar.IsQuadratic (jacobiCharacter q hq) QuadraticCharacters.lean:56:32: error(lean.invalidField): Invalid field notation: Type of a is not known; cannot resolve field `val` Hint: Consider replacing the field projection with a call to one of the following: • `AddUnits.val` • `Char.val` • `Fin.val` • `Finset.val` • `IntermediateField.val` • `IterateAddAct.val` • `IterateMulAct.val` • `NonScalar.val` • `PNat.val` • `PreQuasiregular.val` • `Subalgebra.val` • `SubalgebraClass.val` • `Subtype.val` • `Units.val` • `ZMod.val` • `Array.Mem.val` • `Lean.ExprStructEq.val` • `NumberField.RingOfIntegers.val` • `OrderHom.Subtype.val` • `ST.Out.val` • `Valuation.IsUniformizer.val` • `Valuation.Uniformizer.val` • `
**Fixing NeZero dependency and refining mod proof**
$ /bin/bash -lc "rg -n \"val_natCast|natCast.*val|val.*natCast\" Mathlib/Data/ZMod/Basic.lean | sed -n '1,160p'
sed -n '420,470p' Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean"
89:theorem val_natCast (n a : ℕ) : (a : ZMod n).val = a % n := by
93: · apply Fin.val_natCast
95:lemma val_natCast_of_lt {n a : ℕ} (h : a < n) : (a : ZMod n).val = a := by
96: rwa [val_natCast, Nat.mod_eq_of_lt]
98:lemma val_ofNat (n a : ℕ) [a.AtLeastTwo] : (ofNat(a) : ZMod n).val = ofNat(a) % n := val_natCast ..
101: val_natCast_of_lt han
109: rw [← Nat.mod_zero n, ← val_natCast, val_unit'.mp h]
204:see `ZMod.natCast_val`. -/
205:theorem natCast_zmod_val {n : ℕ} [NeZero n] (a : ZMod n) : (a.val : ZMod n) = a := by
210:theorem natCast_rightInverse [NeZero n] : Function.RightInverse val ((↑) : ℕ → ZMod n) :=
211: natCast_zmod_val
224: rw [Int.cast_natCast, natCast_zmod_val]
237: | _ + 1, i => natCast_zmod_val i
247:theorem natCast_comp_val [NeZero n] : ((↑) : ℕ → R) ∘ (val : ZMod n → ℕ) = cast := by
264:theorem natCast_val [NeZero n] (i : ZMod n) : (i.val : R) = cast i :=
265: congr_fun (natCast_comp_val R) i
278: simp only [Fin.val_add_eq_ite, Int.natCast_succ]
502: have hle : (0 : ℤ) ≤ ↑(a : ZMod n).val := Int.natCast_nonneg _
505: rw [← ZMod.intCast_eq_intCast_iff', Int.cast_natCast, ZMod.natCast_val, ZMod.cast_id]
554: · rw [← natCast_val, val_neg_one, Nat.cast_succ, add_sub_cancel_right]
575: rw [val_natCast, Nat.mod_add_div]
577: rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
587: rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
607: simp only [cast, val, natCast_eq_natCast_iff',
631: rw [← Nat.cast_one, val_natCast]
634: rw [← Nat.cast_two, val_natCast]
737: rw [natCast_zmod_val]
777: rw [mul_inv_eq_gcd, val_natCast, h, Nat.cast_one]
783: rw [ZMod.natCast_zmod_val, ZMod.coe_mul_inv_eq_one _ hmn]
806: rw [← natCast_zmod_val ((u * u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1))]
807: rw [Units.val_mul, val_mul, natCast_mod]
812: rw [IsUnit.unit_spec, val_natCast, Nat.coprime_iff_gcd_eq_one] at H'
875: left_inv := fun ⟨_, _, _, _⟩ => Units.ext (natCast_zmod_val _)
912:**Applying modulo reduction in Jacobi symbol proof** **Patching gcd equivalence between Int and Nat**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean QuadraticCharacters.lean' QuadraticCharacters.lean:35:4: error: Type mismatch: After simplification, term hgcd has type a.cast.natAbs.gcd q = 1 but is expected to have type a.val.gcd q = 1
**Inspecting jacobi symbol cast usage**
$ /bin/bash -lc "nl -ba QuadraticCharacters.lean | sed -n '20,42p'"
20 rw [ZMod.val_one'' hq.ne']
21 exact jacobiSym.one_left q
22 map_mul' a b := by
23 rw [ZMod.val_mul]
24 rw [show (((a.val * b.val) % q : ℕ) : ℤ) =
25 ((a.val * b.val : ℕ) : ℤ) % (q : ℤ) by exact Int.natCast_emod _ _]
26 rw [← jacobiSym.mod_left ((a.val * b.val : ℕ) : ℤ) q]
27 exact jacobiSym.mul_left a.val b.val q
28 map_nonunit' a ha := by
29 letI : NeZero q := ⟨by omega⟩
30 rw [jacobiSym.eq_zero_iff_not_coprime]
31 intro hgcd
32 apply ha
33 rw [← ZMod.natCast_zmod_val a, ZMod.isUnit_iff_coprime,
34 Nat.coprime_iff_gcd_eq_one]
35 simpa [Int.gcd_def] using hgcd
36
37 /-- The complex-valued character used to define its Dirichlet L-function. -/
38 def jacobiCharacter (q : ℕ) (hq : 1 < q) : DirichletCharacter ℂ q :=
39 (jacobiCharacterInt q hq).ringHomComp (Int.castRingHom ℂ)
40
41 @[simp]
42 theorem jacobiCharacterInt_apply_nat (q n : ℕ) (hq : 1 < q) :**Investigating ZMod cast versus val behavior**
$ /bin/bash -lc "rg -n \"cast_eq_val|val_eq_cast|natAbs.*cast|cast.*natAbs\" Mathlib/Data/ZMod | sed -n '1,160p'"
Mathlib/Data/ZMod/ValMinAbs.lean:120: · rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
Mathlib/Data/ZMod/Basic.lean:106: rw [Int.isUnit_iff, Int.natAbs_eq_iff, Nat.cast_one]
Mathlib/Data/ZMod/Basic.lean:182:theorem cast_eq_val [NeZero n] (a : ZMod n) : (cast a : R) = a.val := by
Mathlib/Data/ZMod/Basic.lean:1046:theorem val_cast_eq_val_of_lt {m n : ℕ} [nzm : NeZero m] {a : ZMod m}
Mathlib/Data/ZMod/Basic.lean:1055: rw [cast_eq_val, val_cast_eq_val_of_lt (a.val_lt.trans_le h), natCast_zmod_val]
Mathlib/Data/ZMod/QuotientRing.lean:60: Int.castRingHom (ZMod n.natAbs) := rfl
Mathlib/Data/ZMod/QuotientRing.lean:64: ((Int.quotientSpanEquivZMod n).symm : _ →+* _).comp (Int.castRingHom (ZMod n.natAbs)) =**Patching ZMod.cast_eq_val usage**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean QuadraticCharacters.lean' QuadraticCharacters.lean:33:8: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern ZMod.cast ?a in the target expression (↑a.val).gcd ↑q = 1 q : ℕ hq : 1 < q a : ZMod q ha : ¬IsUnit a this : NeZero q := ⋯ hgcd : (↑a.val).gcd ↑q = 1 ⊢ IsUnit a
**Refining gcd proof with exact_mod_cast**
$ /bin/bash -lc 'lake env lean QuadraticCharacters.lean'
**Defining positive odd quadratic central value function** **Planning conditional theorem on resonance and GRH** **Inspecting mathlib theorem axioms for verification**
**Planning parity verification script and README update** **Developing numeric parity check script**
The first formal layer now compiles: it defines fundamental discriminants and the paper’s \(o(1)\) claim precisely, proves the finite weighted-average/resonance implication, bundles \(n\mapsto J(n\mid q)\) as a genuine mathlib `DirichletCharacter`, proves its pointwise Jacobi-symbol specification and quadraticity, and machine-checks both printed paper defects. The remaining obstruction is the analytic moment estimate itself—the paper’s novel content—not the maximum step or the character semantics. I’m making one last pass to see whether its cited inputs can be exposed narrowly enough to count as legitimate deep hypotheses rather than assuming the conclusion.
**Formulating analytic number theory hypotheses** **Planning moment proof with weighted sums**
**Implementing NeZero instance for LFunction** **Refining shellSup with zero-padding for non-fundamental d**
**Verifying quadratic character properties** **Planning extended Kronecker symbol definition**
**Formalizing moment hypothesis theorem**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean CentralClaim.lean' CentralClaim.lean:1:0: error: unknown module prefix 'ExtremeValues' No directory 'ExtremeValues' or file 'ExtremeValues.olean' in the search path entries: /work/repro/.lake/packages/Cli/.lake/build/lib/lean /work/repro/.lake/packages/batteries/.lake/build/lib/lean /work/repro/.lake/packages/Qq/.lake/build/lib/lean /work/repro/.lake/packages/aesop/.lake/build/lib/lean /work/repro/.lake/packages/proofwidgets/.lake/build/lib/lean /work/repro/.lake/packages/importGraph/.lake/build/lib/lean /work/repro/.lake/packages/LeanSearchClient/.lake/build/lib/lean /work/repro/.lake/packages/plausible/.lake/build/lib/lean /work/repro/.lake/build/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean
**Analyzing Lean compilation and .olean generation**
$ /bin/bash -lc "ls -l *.olean 2>/dev/null || true
sed -n '1,100p' lakefile.lean"
import Lake
open Lake DSL
/-!
## Mathlib dependencies on upstream projects
-/
require "leanprover-community" / "batteries" @ git "main"
require "leanprover-community" / "Qq" @ git "master"
require "leanprover-community" / "aesop" @ git "master"
require "leanprover-community" / "proofwidgets" @ git "main"
with NameMap.empty.insert `errorOnBuild
"ProofWidgets failed to reuse pre-built JS code. \
Please report this issue on the Lean Zulip."
require "leanprover-community" / "importGraph" @ git "main"
require "leanprover-community" / "LeanSearchClient" @ git "main"
require "leanprover-community" / "plausible" @ git "main"
/-!
## Options for building mathlib
-/
/-- These options are used as `leanOptions`, prefixed by `` `weak``, so that
`lake build` uses them, as well as `Archive` and `Counterexamples`. -/
abbrev mathlibOnlyLinters : Array LeanOption := #[
⟨`linter.mathlibStandardSet, true⟩,
-- Explicitly enable the header linter, since the standard set is defined in `Mathlib.Init`
-- but we want to run this linter in files imported by `Mathlib.Init`.
⟨`linter.style.header, true⟩,
⟨`linter.checkInitImports, true⟩,
⟨`linter.allScriptsDocumented, true⟩,
⟨`linter.pythonStyle, true⟩,
⟨`linter.style.longFile, .ofNat 1500⟩,
-- ⟨`linter.nightlyRegressionSet, true⟩,
-- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
]
/-- These options are passed as `leanOptions` to building mathlib, as well as the
`Archive` and `Counterexamples`. (`tests` omits the first two options.) -/
abbrev mathlibLeanOptions := #[
⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
⟨`autoImplicit, false⟩,
⟨`maxSynthPendingDepth, .ofNat 3⟩,
] ++ -- options that are used in `lake build`
mathlibOnlyLinters.map fun s ↦ { s with name := `weak ++ s.name }
package mathlib where
testDriver := "MathlibTest"
lintDriver := "batteries/runLinter"
lintDriverArgs := #["Mathlib"]
-- A version of Mathlib only su**Planning adding Repro lean_lib to lakefile** **Planning reorganizing files under Repro namespace**
**Refining patch application strategy**
**Building reproducible environment**
$ /bin/bash -lc 'lake build Repro' ✔ [3566/3570] Built Repro.ExtremeValues (3.4s) ✔ [3567/3570] Built Repro.QuadraticCharacters (3.4s) ✔ [3568/3570] Built Repro.PaperErrors (3.8s) ✖ [3569/3570] Building Repro.CentralClaim (2.6s) trace: .> LEAN_PATH=/work/repro/.lake/packages/Cli/.lake/build/lib/lean:/work/repro/.lake/packages/batteries/.lake/build/lib/lean:/work/repro/.lake/packages/Qq/.lake/build/lib/lean:/work/repro/.lake/packages/aesop/.lake/build/lib/lean:/work/repro/.lake/packages/proofwidgets/.lake/build/lib/lean:/work/repro/.lake/packages/importGraph/.lake/build/lib/lean:/work/repro/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/work/repro/.lake/packages/plausible/.lake/build/lib/lean:/work/repro/.lake/build/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/lean /work/repro/Repro/CentralClaim.lean -o /work/repro/.lake/build/lib/lean/Repro/CentralClaim.olean -i /work/repro/.lake/build/lib/lean/Repro/CentralClaim.ilean -c /work/repro/.lake/build/ir/Repro/CentralClaim.c --setup /work/repro/.lake/build/ir/Repro/CentralClaim.setup.json --json error: Repro/CentralClaim.lean:24:30: omega could not prove the goal: a possible counterexample may satisfy the constraints a ≤ -1 where a := d error: Repro/CentralClaim.lean:26:8: Tactic `rewrite` failed: Did not find an occurrence of the pattern ↑d.natAbs in the target expression d.natAbs = d.toNat d : ℤ hd : IsPositiveOddFundamental d hdnonneg : 0 ≤ d ⊢ d.natAbs = d.toNat error: Repro/CentralClaim.lean:29:4: mod_cast has type d.toNat % 4 = 1 but is expected to have type d % 4 = 1 error: Repro/CentralClaim.lean:38:2: failed to synthesize instance of type class Decidable (IsPositiveOddFundamental d) Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. error: Repro/CentralClaim.lean:39:32: omega could not prove the goal: a possible counterexample may satisfy the constraints a ≤ 0 where a := d error: Repro/CentralClaim.lean:46:7: failed to synthesize
**Resolving Squarefree decidability issues** **Refining noncomputable def with classical tactic**
$ /bin/bash -lc 'lake env lean Check.lean'
Int.natAbs_of_nonneg {a : ℤ} (H : 0 ≤ a) : ↑a.natAbs = a
Int.toNat_of_nonneg {a : ℤ} (h : 0 ≤ a) : ↑a.toNat = a
Int.ofNat_toNat (a : ℤ) : ↑a.toNat = max a 0
Check.lean:5:7: error(lean.unknownIdentifier): Unknown constant `Int.toNat_ofNat`
Check.lean:6:7: error(lean.unknownIdentifier): Unknown constant `Int.natAbs_ofNat`
Check.lean:7:7: error(lean.unknownIdentifier): Unknown constant `Int.emod_ofNat_eq_coe`**Applying exact_mod_cast for equality** **Defining quadraticLFunction helper with instance**
$ /bin/bash -lc 'lake build Repro' ✔ [3568/3570] Built Repro.QuadraticCharacters (3.3s) ✖ [3569/3570] Building Repro.CentralClaim (3.0s) trace: .> LEAN_PATH=/work/repro/.lake/packages/Cli/.lake/build/lib/lean:/work/repro/.lake/packages/batteries/.lake/build/lib/lean:/work/repro/.lake/packages/Qq/.lake/build/lib/lean:/work/repro/.lake/packages/aesop/.lake/build/lib/lean:/work/repro/.lake/packages/proofwidgets/.lake/build/lib/lean:/work/repro/.lake/packages/importGraph/.lake/build/lib/lean:/work/repro/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/work/repro/.lake/packages/plausible/.lake/build/lib/lean:/work/repro/.lake/build/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/lean /work/repro/Repro/CentralClaim.lean -o /work/repro/.lake/build/lib/lean/Repro/CentralClaim.olean -i /work/repro/.lake/build/lib/lean/Repro/CentralClaim.ilean -c /work/repro/.lake/build/ir/Repro/CentralClaim.c --setup /work/repro/.lake/build/ir/Repro/CentralClaim.setup.json --json error: Repro/CentralClaim.lean:44:34: omega could not prove the goal: a possible counterexample may satisfy the constraints a ≤ -1 where a := d error: Repro/CentralClaim.lean:54:36: omega could not prove the goal: a possible counterexample may satisfy the constraints a ≤ -1 where a := d warning: Repro/CentralClaim.lean:58:6: declaration uses `sorry` warning: Repro/CentralClaim.lean:63:6: declaration uses `sorry` warning: Repro/CentralClaim.lean:61:8: declaration uses `sorry` error: Lean exited with code 1 Some required targets logged failures: - Repro.CentralClaim error: build failed
$ /bin/bash -lc "nl -ba Repro/CentralClaim.lean | sed -n '35,72p'"
35 /--
36 The central norm for the repaired positive odd subfamily, extended by zero away
37 from that subfamily. This is an actual mathlib analytic continuation of the
38 bundled Jacobi-symbol Dirichlet character.
39 -/
40 noncomputable def positiveOddCentralNorm (d : ℤ) : ℝ :=
41 by
42 classical
43 exact if hd : IsPositiveOddFundamental d then
44 have hdnonneg : 0 ≤ d := by omega
45 have hdcast : (d.toNat : ℤ) = d := Int.toNat_of_nonneg hdnonneg
46 have hq : 1 < d.toNat := by
47 exact_mod_cast (show (1 : ℤ) < (d.toNat : ℤ) by simpa [hdcast] using hd.1)
48 ‖jacobiLFunction d.toNat hq (1 / 2)‖
49 else 0
50
51 theorem positiveOddCentralNorm_of_mem {d : ℤ} (hd : IsPositiveOddFundamental d) :
52 positiveOddCentralNorm d =
53 ‖jacobiLFunction d.toNat (by
54 have hdnonneg : 0 ≤ d := by omega
55 have hdcast : (d.toNat : ℤ) = d := Int.toNat_of_nonneg hdnonneg
56 exact_mod_cast (show (1 : ℤ) < (d.toNat : ℤ) by simpa [hdcast] using hd.1) :
57 1 < d.toNat) (1 / 2)‖ := by
58 rw [positiveOddCentralNorm]
59 simp only [dif_pos hd]
60
61 theorem positiveOddCentralNorm_of_not_mem {d : ℤ} (hd : ¬IsPositiveOddFundamental d) :
62 positiveOddCentralNorm d = 0 := by
63 rw [positiveOddCentralNorm]
64 simp only [dif_neg hd]
65
66 /--
67 GRH for exactly the primitive quadratic family used in the repaired statement.
68 The definition is explicit: every nontrivial zero has real part `1/2`.
69 -/
70 def GRHForPositiveOddQuadratic : Prop :=
71 ∀ (q : ℕ) (hq : 1 < q), Squarefree q → q % 4 = 1 →
72 ∀ s : ℂ, jacobiLFunction q hq s = 0 →**Fixing field projection with rcases**
**Initiating build process**
$ /bin/bash -lc 'lake build Repro' ✔ [3569/3570] Built Repro.CentralClaim (2.8s) Build completed successfully (3570 jobs).
**Creating Audit.lean with axioms and theorems**
**Planning Python linter integration**
$ /bin/bash -lc "rg -n \"\\bsorry\\b|\\baxiom\\b|admit|unsafe\" Repro -g '*.lean' || true" Repro/Audit.lean:10:axiom. Repro/CentralClaim.lean:79:finite-moment output of equations (3.2)--(3.8), not an axiom and not the Repro/ExtremeValues.lean:12:not hidden behind an axiom or a `sorry`.
$ /bin/bash -lc 'python3 Repro/parity_check.py' paper-even-weight RHS: 0.18901770464767276 correct odd-weight RHS: 0.66769145718960932 difference: -0.47867375254193656
$ /bin/bash -lc 'lake env lean Repro/Audit.lean' 'ExtremeValues.extreme_values_of_quadratic_dirichlet_L' depends on axioms: [propext, Classical.choice, Quot.sound] 'ExtremeValues.extreme_lower_bound_of_resonance' depends on axioms: [propext, Classical.choice, Quot.sound] 'ExtremeValues.jacobiCharacter_apply_nat' depends on axioms: [propext, Classical.choice, Quot.sound] 'ExtremeValues.jacobiCharacter_isQuadratic' depends on axioms: [propext, Classical.choice, Quot.sound] 'PaperErrors.g2_product_sign_counterexample' depends on axioms: [propext, Classical.choice, Quot.sound, PaperErrors.g2_product_sign_counterexample._native.native_decide.ax_1_1] 'PaperErrors.chiNegFour_gammaFactor' depends on axioms: [propext, Classical.choice, Quot.sound]
**Replacing native_decide with decide in hdiv proof** **Confirming #print axioms necessity and changing native_decide**
**Compiling audit report**
$ /bin/bash -lc "lake env lean Repro/PaperErrors.lean && lake build Repro >/tmp/repro-build.log && lake env lean Repro/Audit.lean && rg -n \"declaration uses|sorryAx|native_decide.ax\" /tmp/repro-build.log Repro -g '*.lean' || true" 'ExtremeValues.extreme_values_of_quadratic_dirichlet_L' depends on axioms: [propext, Classical.choice, Quot.sound] 'ExtremeValues.extreme_lower_bound_of_resonance' depends on axioms: [propext, Classical.choice, Quot.sound] 'ExtremeValues.jacobiCharacter_apply_nat' depends on axioms: [propext, Classical.choice, Quot.sound] 'ExtremeValues.jacobiCharacter_isQuadratic' depends on axioms: [propext, Classical.choice, Quot.sound] 'PaperErrors.g2_product_sign_counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] 'PaperErrors.chiNegFour_gammaFactor' depends on axioms: [propext, Classical.choice, Quot.sound]
**Planning wait using functions.wait**
**Planning repository inspection starting with git status**
$ /bin/bash -lc "git status --short && git diff --stat && git diff -- lakefile.lean | sed -n '1,100p' && find Repro -maxdepth 2 -type f -print | sort" M lakefile.lean ?? Repro/ lakefile.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lakefile.lean b/lakefile.lean index bcdf13405f..e749339b88 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -86,6 +86,10 @@ lean_lib Archive where lean_lib Counterexamples where leanOptions := mathlibLeanOptions +/-- Formal development for the quadratic Dirichlet L-function reproduction attempt. -/ +lean_lib Repro where + globs := #[`Repro.+] + /-- Additional documentation in the form of modules that only contain module docstrings. -/ lean_lib docs where roots := #[`docs] Repro/Audit.lean Repro/CentralClaim.lean Repro/ExtremeValues.lean Repro/PaperErrors.lean Repro/QuadraticCharacters.lean Repro/parity_check.py
**Clarifying theorem assumptions and partial proof status** **Listing errors and repair strategies** **Considering GitHub search for formalizations**
**Planning GitHub library searches**
The parity split gives a semantically clean repaired family, but it does not close the proof: one still needs the GRH-dependent character mean estimate in that restricted progression, the approximate-functional-equation error analysis, and the sharp squarefree GCD-sum construction to produce the formal moment witness. Before documenting a partial verdict, I’m doing the permitted tooling-only search for an existing generic Lean library covering GRH/Dirichlet approximate functional equations or sharp GCD sums; I will not query the paper, its authors, or any paper-specific formalization.
**Using GitHub connector for search**
**Planning parallel tool invocation**
**Implementing nested parallel repository searches**
**Testing global code search with exact strings**
**Inspecting GRH repo file definitions**
**Searching repo for approximateFunctional**
**Evaluating partial GitHub file fetching**
**Fetching KroneckerCharacter source**
**Planning README writing and patching strategy**
The permitted library search found useful generic analytic-number-theory experiments, including a Kronecker-character bridge, but none supplies the three required results: the quadratic-character mean estimate under GRH, the central approximate functional equation with the needed uniform error control, or the sharp squarefree GCD-sum asymptotic. The Kronecker bridge itself leaves the crucial periodicity theorem as a hypothesis, so importing it would not close this proof. I’ve exhausted the credible library route and am now recording the exact boundary and verification results in the README.
**Verifying completion status and updating plan** **Planning full build and audit runs**
$ /bin/bash -lc 'python3 Repro/parity_check.py' paper-even-weight RHS: 0.18901770464767276 correct odd-weight RHS: 0.66769145718960932 difference: -0.47867375254193656
$ /bin/bash -lc "rg -n \"\\bsorry\\b|sorryAx|\\badmit\\b|"'^axiom'"\\b|native_decide\\.ax\" Repro -g '*.lean' || true"
$ /bin/bash -lc 'git status --short' M README.md M lakefile.lean ?? Repro/
$ /bin/bash -lc 'lake build Repro' ℹ [3570/3571] Replayed Repro.Audit info: Repro/Audit.lean:13:0: 'ExtremeValues.extreme_values_of_quadratic_dirichlet_L' depends on axioms: [propext, Classical.choice, Quot.sound] info: Repro/Audit.lean:14:0: 'ExtremeValues.extreme_lower_bound_of_resonance' depends on axioms: [propext, Classical.choice, Quot.sound] info: Repro/Audit.lean:15:0: 'ExtremeValues.jacobiCharacter_apply_nat' depends on axioms: [propext, Classical.choice, Quot.sound] info: Repro/Audit.lean:16:0: 'ExtremeValues.jacobiCharacter_isQuadratic' depends on axioms: [propext, Classical.choice, Quot.sound] info: Repro/Audit.lean:17:0: 'PaperErrors.g2_product_sign_counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Repro/Audit.lean:18:0: 'PaperErrors.chiNegFour_gammaFactor' depends on axioms: [propext, Classical.choice, Quot.sound] Build completed successfully (3571 jobs).
$ /bin/bash -lc 'lake env lean Repro/ExtremeValues.lean'
$ /bin/bash -lc 'lake env lean Repro/QuadraticCharacters.lean'
$ /bin/bash -lc 'lake env lean Repro/Audit.lean' 'ExtremeValues.extreme_values_of_quadratic_dirichlet_L' depends on axioms: [propext, Classical.choice, Quot.sound] 'ExtremeValues.extreme_lower_bound_of_resonance' depends on axioms: [propext, Classical.choice, Quot.sound] 'ExtremeValues.jacobiCharacter_apply_nat' depends on axioms: [propext, Classical.choice, Quot.sound] 'ExtremeValues.jacobiCharacter_isQuadratic' depends on axioms: [propext, Classical.choice, Quot.sound] 'PaperErrors.g2_product_sign_counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] 'PaperErrors.chiNegFour_gammaFactor' depends on axioms: [propext, Classical.choice, Quot.sound]
$ /bin/bash -lc 'lake env lean Repro/CentralClaim.lean'
$ /bin/bash -lc 'lake env lean Repro/PaperErrors.lean'
**Confirming plan completion**
**Preparing final JSON output format** **Summarizing partial proof claims**
{"status":"partial","claim":"Lean proves the epsilon-form extreme-value bound for the positive odd fundamental-discriminant subfamily, assuming both `GRHForPositiveOddQuadratic` and `GRHImpliesPaperResonanceMoments`. It also proves the Jacobi-character semantics and the resonance-moment-to-maximum argument; the second hypothesis is the paper’s still-unformalized analytic core, not an accepted external theorem.","note":"All files in `repro/Repro/` compile with zero proof placeholders and no project axioms. The missing work comprises the parity-correct approximate functional equation and error bounds, the GRH quadratic-character mean estimate, and the sharp squarefree GCD-sum construction. Two printed errors were verified: Lemma 2.1 uses the even gamma factor for negative discriminants (with d=-4 a concrete failing case), and the Euler product for g2 has a minus where a plus is required. Full details and attempted approaches are in `repro/README.md`.","significance":"The paper claims under GRH that the maximum of $|L(1/2,\\chi_d)|$ for $X<|d|\\le 2X$ is at least $\\exp((1+o(1))\\sqrt{\\log X\\,\\log_3X/\\log_2X})$. This would improve the leading constant in the known lower bound to $1$, sharpening our understanding of extreme central values in a fundamental family of $L$-functions."}