phi_ladder_certificate
plain-language theorem explainer
The phi-ladder certificate assembles positivity of the golden ratio, its quadratic identity, the reciprocal relation phi inverse equals phi minus one, additive spacing log phi on the integer rungs, involutivity of the rung-reciprocal map, and invariance of the cost function under that map. Number theorists and physicists working on self-similar discrete spectra cite it to invoke the complete algebraic structure of the phi-lattice without rederiving components. The proof is a term-mode refinement that packages six supporting lemmas into the top-
Claim. Let $phi = (1 + sqrt(5))/2$. Then $0 < phi land 1 < phi$, $phi^2 = phi + 1$, $phi^{-1} = phi - 1$, for every integer $r$ the lattice point at rung $r+1$ equals the point at $r$ plus $log phi$, the map $r mapsto -r$ is an involution on the rungs, and the cost evaluated at $phi^r$ equals the cost at $phi^{-r}$.
background
The phi-ladder is the discrete hierarchy forced by RS theorem T6 on the multiplicative half-line, realized as the geometric sequence $phi^r$ for $r in Z$. On the log scale this becomes the additive lattice $r cdot log phi$ in the reals. The module defines phiLatticePoint $r$ as this position and phiLatticeReciprocal $r$ as the map to $-r$, which encodes inversion $x mapsto 1/x$. Upstream results include the lemma phi_sq_eq establishing $phi^2 = phi + 1$ from the minimal polynomial and the reciprocal automorphism in CostAlgebra that encodes inversion symmetry of the J-cost.
proof idea
The proof is a term-mode refinement that constructs the six-part conjunction. It supplies phi_pos and phi_gt_one for the first conjunct, phi_sq_eq for the quadratic identity, phi_inv_eq_phi_minus_one for the reciprocal relation, and then three separate intro-exact steps that apply phiLatticePoint_succ, phiLatticeReciprocal_involutive, and cost_phi_ladder_reciprocal to the universal quantifiers.
why it matters
This declaration supplies the complete structural certificate for the phi-ladder lattice, closing the algebraic scaffolding for the phi-Poisson summation hypothesis structure noted in the module documentation. It realizes the self-similar fixed point of T6 and the reciprocal symmetry required by the Recognition Composition Law. The certificate underpins cost invariance on the ladder and supports applications that rank spectral features by rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.