that
plain-language theorem explainer
The phi-ladder Poisson summation hypothesis states that the lattice sum of a rapidly decreasing f over integer multiples of log φ equals the scaled dual sum of its Fourier transform. Researchers deriving continuum limits from discrete phi-rungs in Recognition Science cite the packaged Prop when they need the identity for lattice sums. The declaration is a structure definition with no proof body that simply records the statement for later discharge.
Claim. Let $f : ℝ → ℝ$ be rapidly decreasing. Then $∑_{r ∈ ℤ} f(r log φ) = (1 / log φ) ∑_{m ∈ ℤ} ˆf(2π m / log φ)$, where ˆf is the Fourier transform. The identity is the standard Poisson summation formula applied to the lattice Λ_φ = (log φ) ℤ whose dual is Λ_φ* = (2π / log φ) ℤ.
background
The phi-ladder is the geometric sequence φ^r for r ∈ ℤ forced by self-similarity (T6). On the log scale t = log x it becomes the additive lattice r log φ, which admits Poisson summation because it is a true lattice in ℝ. The module records the basic facts phi_pos, log_phi_pos, phiLatticeReciprocal_involutive and phiRung_recip that establish the lattice and its reciprocal symmetry x ↦ 1/x.
proof idea
This is a structure definition that packages the Poisson summation statement as a Prop. It contains no proof body and functions as a hypothesis interface to be assumed until the required Fourier-analytic infrastructure is available.
why it matters
The structure records Sub-conjecture A.2, supplying the analytic bridge between discrete phi-ladder sums and their Fourier duals. Downstream results in Action.EulerLagrange and Action.FunctionalConvexity rely on the lattice symmetries it encodes when proving rigidity and convexity of the J-action. It marks the precise point where the formalization awaits discharge of the Poisson identity via mathlib Fourier tools.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.