phiLatticePoint_neg
plain-language theorem explainer
The result shows that the phi-lattice point at rung -r equals the negative of the point at rung r. Number theorists and Recognition Science researchers modeling reciprocal symmetry on the phi-ladder would reference this when establishing involution properties. The proof proceeds by unfolding the definition of the lattice point and applying ring normalization after casting integers to reals.
Claim. For every integer $r$, the phi-lattice point at $-r$ equals the negative of the phi-lattice point at $r$, where the phi-lattice point at rung $r$ is $r · log φ$.
background
The phi-ladder arises from RS theorem T6, where self-similarity forces the golden ratio φ. On the log scale, the ladder becomes the lattice {r log φ : r ∈ ℤ}. The function phiLatticePoint(r) computes the position r · log φ, as defined by unfolding to (r : ℝ) * Real.log phi. This module formalizes the lattice and its symmetries, including the reciprocal map r ↦ -r corresponding to x ↦ 1/x. The upstream definition supplies the explicit formula used here.
proof idea
The proof is a one-line wrapper that unfolds the definition of phiLatticePoint, pushes the integer cast, and invokes the ring tactic to verify the algebraic identity.
why it matters
This theorem supports the reciprocal involution phiLatticePoint_reciprocal, which encodes the self-duality of the phi-ladder under inversion. It fills the discrete analog of reciprocal symmetry in the Recognition framework, linking to the cost function symmetries and preparing for Poisson summation on the lattice. It touches the open analytic content in PhiLadderPoissonSummation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.