phi_ne_one
plain-language theorem explainer
Golden ratio phi satisfies phi not equal to 1. Researchers deriving positivity of J-cost in cosmology and spectral emergence cite it to block zero denominators and degeneracy in the phi-ladder. The proof is a one-line wrapper applying ne_of_gt directly to the upstream strict inequality 1 less than phi.
Claim. Let φ be the golden ratio. Then φ ≠ 1.
background
The Constants module places phi alongside the RS time quantum τ₀ set to one tick. Upstream one_lt_phi in the same module and in PhiSupport establishes 1 < phi via square-root comparisons and norm_num. The NumberTheory.PhiLadderLattice module carries an identical statement, confirming the fact is required for lattice constructions.
proof idea
This is a one-line wrapper that applies ne_of_gt to the lemma one_lt_phi.
why it matters
The lemma is invoked by Jcost_phi_pos in Constants and by J_phi_pos in SpectralEmergence to obtain 0 < J(φ). It also appears in dmCrossSection_pos and hubble_tension_pos, securing positivity results tied to the Recognition Composition Law and the T6 self-similar fixed-point step. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.