PhiLadderPoissonSummation
plain-language theorem explainer
The declaration packages the Poisson summation identity on the phi-ladder lattice as a hypothesis structure. For rapidly decreasing f the sum over integer multiples of log phi equals the scaled dual sum of the Fourier transform. Researchers deriving spectral properties or continuum limits from the phi-ladder would cite it when invoking analytic duality. The proof is a one-line wrapper that applies trivial after introducing the assumptions.
Claim. Let $phi = (1 + sqrt(5))/2$. For any rapidly decreasing function $f: R to R$, the lattice sum $sum_{r in Z} f(r log phi)$ equals $(1/log phi) sum_{m in Z} hat f (2 pi m / log phi)$, where hat f is the Fourier transform. This identity is asserted as a proposition on the lattice Lambda_phi = (log phi) Z with dual (2 pi / log phi) Z.
background
The phi-ladder is the geometric sequence {phi^r : r in Z} on the positive reals; under t = log x it becomes the additive lattice {r log phi : r in Z} in R. The module defines phi as the golden ratio, phiLatticePoint r as the point r log phi, and phiLatticeReciprocal as the involution r to -r that encodes x to 1/x. Upstream results supply the J-cost factorization on (R_+, times) and the identity event at the J-cost minimum x=1, both of which presuppose the lattice structure for cost symmetry.
proof idea
The proof is a one-line wrapper that applies trivial. It refines the structure by introducing the rapid-decrease and summability assumptions and then discharges the remaining propositional claim with the trivial tactic.
why it matters
This fills sub-conjecture A.2 of the phi-ladder module, supplying the analytic content for Poisson summation that is not yet formalized in mathlib. It supports derivations of spectral emergence and continuum bridges that rely on lattice duality, linking to T6 (phi as self-similar fixed point) and T7 (eight-tick octave). The open question it touches is the concrete Fourier-transform definition needed to turn the hypothesis into a theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.