phi_ne_one
plain-language theorem explainer
The golden ratio φ satisfies φ ≠ 1. Researchers building the phi-ladder lattice and deriving J-cost positivity cite this to anchor strict inequalities away from the identity event. The proof is a one-line term application of ne_of_gt to the upstream fact that φ > 1.
Claim. Let φ = (1 + √5)/2. Then φ ≠ 1.
background
The phi-ladder lattice module defines φ as the golden ratio (1 + √5)/2 forced by self-similarity (RS theorem T6). On ℝ>0 the ladder is the geometric sequence {φ^r : r ∈ ℤ}; on the log scale it becomes the additive lattice {r log φ}. The J-cost is the Recognition Composition Law functional J(x) = (x + x^{-1})/2 - 1, which vanishes only at x = 1. Upstream lemmas supply phi_gt_one (φ > 1) together with structures from ObserverForcing (identity event at J-minimum) and PhiForcingDerived (J-cost calibration).
proof idea
The proof is a one-line term-mode wrapper that applies ne_of_gt directly to the sibling lemma phi_gt_one.
why it matters
This basic inequality is invoked by Jcost_phi_pos (Constants), J_phi_pos (SpectralEmergence), hubble_tension_pos and dmCrossSection_pos (Cosmology). It supplies the strict departure from unity required for the phi-ladder reciprocal symmetry and for the positivity half of the Recognition Composition Law. The result closes an early step toward the eight-tick octave and D = 3 emergence while leaving the phi-Poisson summation hypothesis open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.