{"id":"palomar/PALOMAR-2026-08-24-000007","url":"https://github.com/xiangyazi24/palomar-qseries-row-factorization/tree/702c524cd8bc70867c918c23039680e7adf48bf8","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-24-000007-v1.json","repo":"https://github.com/xiangyazi24/palomar-qseries-row-factorization","tags":["math.NT","msc:11F27","msc:33D15","number-theory","theta-series","lean-formalization"],"score":0,"title":"xiangyazi24/palomar-qseries-row-factorization","trust":"high","domain":"math.NT","source":"palomar","authors":["Xiang Huang"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 verification of an explicit rank-two indefinite theta completion over Q(sqrt(5)). The registered results cover the coefficientwise row-model factorization; the exact holomorphic-sign-part bridge; summability of the defining completed-theta lattice series; a specialization of Zwegers' Lemma 2.8; the weight-one T and S transformations, including the five-to-two characteristic reduction; the exact mixed boundary derivative and Bruinier--Funke image; and a kernel-checked nonharmonicity witness.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-24","reactions":{},"formalized":true,"formalizes":[{"title":"A shifted indefinite theta completion over Q(sqrt(5)): an asymmetric boundary derivative and a row-model factorization","identifier":"","relationship":"formalizes"},{"title":"Mock theta functions","identifier":"","relationship":"formalizes"}]}