balancedscorpion/shifted-square-root-fourier-classification
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.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-08-25-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-25-000001/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-25-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'