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) = ∏δ∣Nη(δz)rδf(z) \;=\; \prod_{\delta \mid N} \eta(\delta z)^{r_\delta}f(z)=δ∣N∏η(δz)rδ 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:… See the full description on the dataset page: https://huggingface.co/datasets/callensxavier/socrateai-eta-quotients.
Refresh numbers and add the Fricke-self-dual citation
Refresh numbers and add the Fricke-self-dual citation
Refresh numbers and add the Fricke-self-dual citation
Refresh dag/theorems.jsonl (104 nodes, 95 proved)
Refresh FinalCheck.lean (1122 guards)
Refresh library-wide numbers (1122 guards, 1120 distinct, 104/95 DAG) and link the new self-dual eta-quotient artifact
v9: AI-disclosure note on method (Tao arXiv:2608.16753; Leiden Declaration); refreshed library-wide numbers
v9: AI-disclosure note on method (Tao arXiv:2608.16753; Leiden Declaration); refreshed library-wide numbers
v9: AI-disclosure note on method (Tao arXiv:2608.16753; Leiden Declaration); refreshed library-wide numbers
v9: AI-disclosure note on method (Tao arXiv:2608.16753; Leiden Declaration); refreshed library-wide numbers
v9: AI-disclosure note on method (Tao arXiv:2608.16753; Leiden Declaration); refreshed library-wide numbers
v9: AI-disclosure note on method (Tao arXiv:2608.16753; Leiden Declaration); refreshed library-wide numbers
v9: AI-disclosure note on method (Tao arXiv:2608.16753; Leiden Declaration); refreshed library-wide numbers
v9: AI-disclosure note on method (Tao arXiv:2608.16753; Leiden Declaration); refreshed library-wide numbers
v9: AI-disclosure note on method (Tao arXiv:2608.16753; Leiden Declaration); refreshed library-wide numbers
v8: substantive correction — Phi/FLT claim retracted, ETA-01 narrowed to one node, N=17 refutation
v7: prior-art correction — FLT artifact already has Dedekind sums, reciprocity, Phi, and the eta multiplier
v6: gate-verified before publication; axiom count corrected to six; TACTICS.md added
v5: internal review — corrected Phi/Psi conflation, abelianization rank, footprint split 385/1/3, scoped axiom claim
v4: review revisions — code snippets, AFP citations, corrected limitation (d)
Artifact is now third-party buildable; portable lakefile
Stamp concept DOI 10.5281/zenodo.22648098
Eta-quotients in Lean 4: cusp orders, Ligozat at small level, named obstruction
initial commit