phiLatticePoint
The definition assigns to each integer rung r the real value r log phi, placing the phi-ladder points on the additive log scale. Number theorists and Recognition Science researchers working on self-similar hierarchies and Poisson summation would cite this construction. It is supplied by a direct one-line definition that scales the rung index by the fixed positive constant log phi.
claimFor each integer rung $r$, the lattice point on the log scale is $r log phi$, where $phi$ denotes the golden ratio.
background
The phi-ladder is the discrete hierarchy forced by RS theorem T6: self-similarity selects the golden ratio phi, so the multiplicative sequence is {phi^r : r in Z}. On the log scale t = log x this becomes the additive lattice {r log phi : r in Z}, which admits Poisson summation. The module also records that phi > 1, log phi > 0, and phi satisfies phi^2 = phi + 1 together with the reciprocal relation phi^{-1} = phi - 1.
proof idea
Direct definition: the body is the cast of r multiplied by Real.log phi. No lemmas or tactics are invoked; the declaration simply introduces the primitive map from rung index to lattice coordinate.
why it matters in Recognition Science
This definition supplies the lattice points required by the phi_ladder_certificate theorem, which assembles the structural facts (positivity, golden-ratio identity, discrete self-similarity) for the entire phi-ladder. It is used to prove closure under negation, successor, and reciprocal involution, all zero-sorry results. The construction realizes the additive lattice needed for the phi-Poisson summation sub-conjecture A.2 stated as a hypothesis structure in the same module.
scope and limits
- Does not prove any algebraic or analytic properties of the lattice points.
- Does not relate the lattice to the cost function J.
- Does not address the analytic content of Poisson summation.
- Does not extend the construction beyond integer rungs.
formal statement (Lean)
126def phiLatticePoint (r : ℤ) : ℝ := (r : ℝ) * Real.log phi
proof body
Definition body.
127