{"id":"palomar/PALOMAR-2026-08-25-000001","url":"https://github.com/balancedscorpion/shifted-square-root-fourier-classification/tree/8aa99c16d2733debd1fac67353b0206802ee52bb","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-25-000001-v1.json","repo":"https://github.com/balancedscorpion/shifted-square-root-fourier-classification","tags":["math.CA","math.NT","msc:42A38","msc:11F37","msc:52C23","fourier-analysis","modular-forms","measure-theory"],"score":0,"title":"balancedscorpion/shifted-square-root-fourier-classification","trust":"high","domain":"math.CA","source":"palomar","authors":["Jamie Martin","Li Shen"],"reviews":0,"subject":"math.CA","summary":"For 0 < θ < 1, this Lean 4 formalization classifies tempered atomic measures whose support and Fourier support are contained in the shifted square-root set Λθ = {±√(n + θ) | n ∈ ℕ₀}. In an equivalent polynomial-growth coefficient model, it proves that the −1 and i Fourier eigenspaces vanish, identifies the surviving 1 and −i eigenspaces as one-dimensional lines generated by explicit generalized eta products up to the respective thresholds θ ≤ 1/8 and θ ≤ 3/8, and proves that the full admissible space has dimension 2, 1, or 0 in the resulting three θ ranges.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-25","reactions":{},"formalized":true,"formalizes":[{"title":"Crystalline Measures on Shifted Square-Root Sets","identifier":"","relationship":"formalizes"}]}