phi_ne_zero
plain-language theorem explainer
The golden ratio is nonzero. Researchers modeling the phi-ladder hierarchy in Recognition Science cite this fact whenever divisions by phi or exponentiations appear in cost calculations or lattice points. The proof applies the positivity of phi in a single step.
Claim. Let $phi = (1 + sqrt(5))/2$ be the golden ratio. Then $phi neq 0$.
background
The module defines the phi-ladder as the geometric sequence of powers of the golden ratio $phi = (1 + sqrt(5))/2$ on the positive reals. On the log scale this forms an additive lattice admitting Poisson summation. The theorem states that phi is not zero, a prerequisite for inverses and field operations throughout the lattice.
proof idea
The proof is a term-mode one-liner that applies ne_of_gt directly to the positivity of phi.
why it matters
This nonzeroness result anchors the phi-ladder lattice and its reciprocal symmetry. It feeds into downstream results on adjacency gaps, golden division ratios, nucleosynthesis tiers, Lyapunov exponents, orbital gap bands, and forecast skill decay. It supports the self-similar fixed point T6 and the eight-tick octave T7 in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.