phiLatticePoint_succ
plain-language theorem explainer
The theorem establishes that consecutive rungs on the phi-ladder lattice differ by exactly log φ. Researchers formalizing self-similar hierarchies or Poisson summation in Recognition Science cite it to confirm the additive spacing on the log scale. The proof is a direct algebraic reduction obtained by unfolding the lattice-point definition and applying ring simplification after casting.
Claim. For any integer $r$, the phi-lattice point at rung $r+1$ equals the phi-lattice point at rung $r$ plus the natural logarithm of the golden ratio: $r+1$ maps to $r + 1$ on the additive lattice generated by $r · log φ$.
background
The phi-ladder lattice arises from the self-similar fixed point forced by Recognition Science theorem T6. On the positive reals the ladder is the geometric sequence {φ^r : r ∈ ℤ}; under the logarithm t = log x it becomes the additive arithmetic progression {r · log φ : r ∈ ℤ}, a true lattice in ℝ that admits Poisson summation. The function phiLatticePoint(r) is defined to be exactly this lattice point r · log φ. The module also records the reciprocal involution r ↦ -r, which corresponds to the cost reciprocal x ↦ 1/x and is used in downstream cost-symmetry statements.
proof idea
The proof is a one-line wrapper. It unfolds the definition of phiLatticePoint, pushes the integer cast into the reals, and invokes ring to verify the additive spacing identity.
why it matters
This spacing result is invoked by the phi_ladder_certificate theorem that assembles the structural facts of the lattice. It supplies the additive group structure required for the phi-Poisson summation sub-conjecture stated as a hypothesis interface in the same module. The construction directly realizes the discrete hierarchy forced by T6 self-similarity and supplies the rung indexing used in the mass formula yardstick · φ^(rung-8+gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.