{"id":"palomar/PALOMAR-2026-08-22-000003","url":"https://github.com/xiangyazi24/palomar-hahn-hecke-appell/tree/b9d84fd9f905605b3956f974f50ed41ee59d54e2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-22-000003-v1.json","repo":"https://github.com/xiangyazi24/palomar-hahn-hecke-appell","tags":["math.NT","msc:11F27","msc:33D15","q-series","hecke-appell","lean-formalization","partial-fractions"],"score":0,"title":"xiangyazi24/palomar-hahn-hecke-appell","trust":"high","domain":"math.NT","source":"palomar","authors":["Xiang Huang"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 verification of the coefficientwise Kronecker partial-fraction identity and the general boundary-cleared Hickerson--Mortenson Hecke--Appell identity for f_{n,n+p,n}, for all positive integers n and p.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-22","reactions":{},"formalized":true,"formalizes":[{"title":"A Hahn-Series Coefficientwise Proof of the Hickerson--Mortenson Hecke--Appell Identities","identifier":"","relationship":"formalizes"}]}