Eta-Quotients in Lean 4: Cusp Orders at Every Cusp, Ligozat's Criterion at Small Level, and a Named Obstruction at General Level
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. Machine-checked Lean 4 formalization of the arithmetic and analytic layers of Ligozat's criterion for eta-quotients f(z) = ∏δ|N η(δz)rδ, reporting three results at three different strengths. (i) General N. For every level N, every integer exponent vector r with Σ rδ = 2k, and every γ ∈ SL(2,ℤ) — with no congruence condition and no Γ0(N)-membership hypothesis — a two-sided Θ-asymptotic for |(f|kγ)(z)| along Im z → ∞, with exponent Ligozat's cusp-order expression. At the cusp ∞ the order is additionally identified in Mathlib's own meromorphicOrderAt / cuspFunction language. (ii) Bounded. Ligozat's full transformation law f(γz) = w(γ)(cz+d)kf(z) on all of Γ0(N), with the character identified, for N ∈ {1,2,3,4,5,7,13} only — N ≤ 4 by a Euclidean descent, and the genus-zero primes 5, 7, 13 by a Schreier transversal criterion. (iii) Obstructed. Ligozat's criterion for general N is not proved, and the obstruction is named exactly: the multiplier is w(γ) = exp((πi/12)·per(γ)) where per is the period cocycle of the weight-two quasi-modular combination Σ rδδE2(δz) — the integration constant that both the logDeriv route and the 24th-power route erase. For a single η that period function is Rademacher's Φ, whose non-coboundary content is the Dedekind sum s(d,|c|). Mathlib contains no Dedekind sums. The deposit names the minimal Mathlib addition that would remove the obstruction, and argues Φ is best built as the period of E2 on the E2_slash_action machinery Mathlib already has. The DAG node ETA-01 (the general criterion) remains open with lean_name: null. This artifact does not claim it. Verification: lake build SocrateAI → 3768 jobs, 0 errors, 0 sorry. 519 declarations in 8117 lines. 822 build-failing #guard_msgs in #print axioms guards (library-wide, now shared with a follow-up T-duality module — see 10.5281/zenodo.22542571 v4) over 820 distinct theorems; 793 report exactly [propext, Classical.choice, Quot.sound]. A negative control asserting a deliberately wrong footprint is verified to fail. Of 453 theorems, 14 (3%) have a one-line rfl/decide proof. v9 update: adds a note on method, grounded in Tao's Mathematics in the age of AI (arXiv:2608.16753) and the Leiden Declaration on Artificial Intelligence and Mathematics, disclosing the neuro-symbolic, AI-assisted methodology and stating the author's responsibility for every claim in the paper. Correction to our own specification: the cusp-order node was scoped with the Θ-exponent written as Ligozat's ord(N,r,d). That statement is false — Ligozat's order is taken in the local uniformiser at a cusp of width h = N/gcd(d²,N), so a decay statement in Im z carries exponent ord/h. The corrected statement is what was proved. Reproduction caveat: the build configuration is not distributed (lakefile.lean hard-codes absolute paths to a local Mathlib pool), so this artifact is not yet buildable by a third party. Mirror: HuggingFace. Builds on the Fricke involution formalization, 10.5281/zenodo.22542571.