pith. machine review for the scientific record. sign in
structure definition def or abbrev high

that

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 192structure that can be assumed in downstream theorems and discharged
 193when the analytic infrastructure becomes available. -/
 194
 195/-- Hypothesis structure: phi-ladder Poisson summation.
 196
 197If `f : ℝ → ℝ` is rapidly decreasing and we form the lattice sum
 198`Σ_{r ∈ ℤ} f(r · log φ)`, the Poisson identity states this equals
 199`(1/log φ) · Σ_{m ∈ ℤ} f̂(2π m / log φ)` where `f̂` is the Fourier
 200transform.  This is a special case of standard Poisson summation
 201on `ℝ` for the lattice `Λ_φ = (log φ) · ℤ` with dual lattice
 202`Λ_φ* = (2π/log φ) · ℤ`.
 203
 204We package the statement as a Prop. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (15)

Lean names referenced from this declaration's body.