callensxavier/socrateai-eta-quotients

Eta-Quotients in Lean 4

Machine-checked Lean 4 formalization of the arithmetic and analytic layers of Ligozat's criterion for eta-quotients

$$f(z) \;=\; \prod{\delta \mid N} \eta(\delta z)^{r\delta}$$

together with a precisely named obstruction to the general case.

⚠️ PREPRINT — not peer reviewed. The Lean development compiles and is axiom-audited; those claims are machine-checked. The paper's exposition has had no external referee.

DOI: 10.5281/zenodo.22648098 (all versions) · Author: Xavier Callens · Code: SocrateAI-Lean-Lib · Paper: SocrateAI-Scientific-Communication

Read the scope before citing

Three results at three different strengths. The difference matters:

The DAG node ETA-01 (the general criterion) remains `open` with `lean_name: null`. This artifact does not claim it.

The obstruction, stated exactly

The multiplier is $w(\gamma) = \exp\!\big(\tfrac{\pi i}{12}\,\mathrm{per}(\gamma)\big)$, where $\mathrm{per}$ is the period cocycle of the weight-two quasi-modular combination $\sum\delta r\delta\,\delta\,E_2(\delta z)$ — exactly the integration constant that both the logDeriv route and the 24th-power route erase. For a single $\eta$ that period function is Rademacher's $\Phi$, whose non-coboundary content is the Dedekind sum $s(d,|c|)$.

Mathlib contains no Dedekind sums. Evaluating $w$ on one hyperbolic element of $\Gamma_0(11)$ is equivalent to evaluating a Dedekind sum. Every disguise tried — Atkin–Lehner conjugation, theta/Poisson, Wohlfahrt level-24 — reduces back to it.

MATHLIB_PR.md names the minimal Mathlib addition that would remove it, and argues that Rademacher's $\Phi$ is best built as the period of $E2$ on the `E2slash_action` machinery Mathlib already has.

Verification

lake build SocrateAI → 3769 jobs, 0 errors, 0 `sorry`. Lean 4.32.2, Mathlib 905b9581. 519 declarations in 8117 lines. 1122 build-failing `#guard_msgs in #print axioms` guards (library-wide, now shared with a follow-up T-duality module and a follow-up self-dual eta-quotient module — see 10.5281/zenodo.22542571 v4 and the Fricke-self-dual artifact) over 1120 distinct theorems; 1080 report exactly [propext, Classical.choice, Quot.sound]. A negative control asserting a deliberately wrong footprint is verified to fail, which is what makes the guards load-bearing rather than vacuous.

Of the 453 theorems in the new modules, 14 (3%) have a one-line `rfl`/`decide` proof and 45% quantify over a structure. This ratio is reported because an earlier module in this project was 174 numeral identities of which 158 were one-line and carried no evidential weight.

A correction we made to our own specification

The cusp-order node was originally specified with the Θ-exponent written as Ligozat's $\mathrm{ord}(N,r,d)$. That statement is false. Ligozat's order is taken in the local uniformiser $q_h$ at a cusp of width $h = N/\gcd(d^2,N)$, so a decay statement in $\mathrm{Im}\,z$ carries exponent $\mathrm{ord}/h$. The corrected statement is what was proved, and the discrepancy is stated in the paper rather than quietly matched. Ligozat's positivity condition is unaffected ($h > 0$).

A note on method

The paper's closing section, "A note on method: AI assistance and human responsibility," follows the disclosure norm argued for by Terence Tao (Mathematics in the age of AI, arXiv:2608.16753) and the Leiden Declaration on Artificial Intelligence and Mathematics: the Lean formalization, literature search, and drafting were produced with LLM assistance under human direction, the Lean kernel — not the model — admits or rejects every mathematical claim, and the author is responsible for every claim in the paper, including the specification correction recorded above.

Prior art

Mathlib has $\eta$ (DedekindEta.lean, and the $S$-transformation in Discriminant.lean) but no eta-quotients: EtaQuotient, Ligozat, DedekindSum, etaMultiplier all return zero. anthropics/fermats-last-theorem contains eta material, but it is about modular units on modular function fields; its three Ligozat occurrences are namespace labels (LigozatUnitEngine, LigozatUnitAL), not the criterion. GitHub-wide language:lean returns 0 for Ligozat. Not checked: Lean Zulip, open mathlib4 PRs.

Reproducing this

git clone https://github.com/xaviercallens/SocrateAI-Lean-Lib
cd SocrateAI-Lean-Lib
lake exe cache get      # ~5 GB of prebuilt Mathlib oleans
lake build SocrateAI    # 3769 jobs, 0 errors

The build configuration is portable: lakefile.lean requires Mathlib from git at the pinned revision 905b95818eb3…, lean-toolchain matches, and no tracked file contains a machine-specific path. See BUILDING.md.

Earlier versions of this card said the artifact was not third-party buildable. That was true, and understated — the published `lakefile.lean` declared no Mathlib dependency at all and its `lean-toolchain` named a different compiler version. Both are fixed.

Citation

@misc{callens2026etaquotients,
  author = {Callens, Xavier},
  title  = {Eta-Quotients in Lean 4: Cusp Orders at Every Cusp, Ligozat's Criterion
            at Small Level, and a Named Obstruction at General Level},
  year   = {2026},
  doi    = {10.5281/zenodo.22648098},
  note   = {Preprint, not peer reviewed. Ligozat proved only for N in {1,2,3,4,5,7,13}},
  url    = {https://doi.org/10.5281/zenodo.22648098}
}