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.