phi_ne_zero
plain-language theorem explainer
The golden ratio φ satisfies φ ≠ 0. Researchers building phi-ladder models in astrophysics, climate forecasting, and composition analysis cite this fact to license divisions by powers of φ. The proof is a one-line wrapper that applies the standard inequality-to-non-equality lemma to the established positivity of φ.
Claim. Let φ be the golden ratio, the unique positive real solution to x² = x + 1. Then φ ≠ 0.
background
Recognition Science defines φ as the self-similar fixed point arising in the forcing chain at step T6. The Constants module records its elementary algebraic properties in RS-native units where the fundamental time quantum equals one tick. Positivity φ > 0 is established upstream in PhiLadderLattice (whose doc-comment states φ is not zero) and in PhiSupport.Lemmas (which reduces it to Real.goldenRatio_pos).
proof idea
The proof is a one-line wrapper that applies ne_of_gt directly to the positivity fact phi_pos.
why it matters
This non-vanishing lemma is invoked in more than forty downstream results that manipulate ratios and exponents of φ. It supplies the hypothesis needed for the phi-ladder step in nucleosynthesis tiers, the Lyapunov ratio decay in PIC simulations, the orbit-gap band in planetary formation, and the forecast-skill decay in climate models. The result closes a routine but ubiquitous scaffolding requirement for the Recognition Composition Law and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.