Papers With

← All papers
First page of Positive quasimodular forms and the sign uncertainty principle

Positive quasimodular forms and the sign uncertainty principle

Seewoo Lee

math.NT Aug 15, 2026 · v2 math.CA
formalization number-theory mathlib
Read PDF arXiv abstract Code
TL;DR
Formalizes lemmas on Kaneko–Zagier operators and coefficient-positivity of quasimodular form families in Lean 4. Ramanujan's identities are taken as axioms, and the code was written with AI assistance.
Abstract
For every positive integer $d$ divisible by $4$, we prove the following new upper bound for the Bourgain-Clozel-Kahane sign uncertainty constant: \[ \mathrm{A}_+(d) \le \sqrt{2 \left\lfloor \frac{d}{16} \right\rfloor + 2}. \] It recovers the optimal bound $\mathrm{A}_+(12) \le \sqrt{2}$ in dimension $12$ and improves the previously best known bound $\sqrt{(d+2)/(2π)}$ for all $d \ge 52$ divisible by $4$. The proof uses Fourier eigenfunctions and associated quasimodular forms constructed by Feigenbaum, Grabner, and Hardin.
Problem

The Bourgain–Clozel–Kahane sign uncertainty constant A_+(d) has a known exact value only in dimension 12. The best general upper bound was sqrt((d+2)/(2π)).

Approach

The proof uses the Fourier eigenfunctions of Feigenbaum, Grabner and Hardin, which are built from depth-2 quasimodular forms. Their positivity is established through a positivity theory for quasimodular forms and links to Kaneko–Koike extremal forms. Routine but lengthy lemmas are formalized in Lean 4 using a q-series model and a polynomial-ring model of E2, E4 and E6. Sage code provides an independent sanity check.

Results

For every d divisible by 4, A_+(d) ≤ sqrt(2⌊d/16⌋+2). This recovers A_+(12) ≤ √2 and improves the previous bound for all d ≥ 52. The Kaneko–Zagier operator lemmas and the coefficient-positivity propositions are machine-checked in Lean.