phi_ne_zero'
The lemma shows that the golden ratio φ is nonzero. Researchers deriving running couplings via φ-ladder scaling in QFT would cite it to justify divisions or logs involving φ. The proof is a one-line term application of the negation-of-greater-than lemma to the positivity fact for φ inside the Constants bundle.
claimLet φ be the golden ratio. Then φ ≠ 0.
background
The module derives running of electromagnetic, strong, and weak couplings from φ-ladder scaling, where each rung sets an energy scale and J-cost optimization yields the beta functions. The Constants structure from LawOfExistence bundles the core CPM parameters (Knet, Cproj, Ceng, Cdisp and others) together with nonnegativity constraints such as 0 ≤ Knet. The local setting treats φ as the self-similar fixed point that labels the rungs.
proof idea
Term-mode one-liner that applies ne_of_gt directly to the positivity statement Constants.phi_pos.
why it matters in Recognition Science
It supplies the basic nonzeroness fact required for any φ-scaling expression in the running-couplings target. The fact rests on the T6 forcing of φ as self-similar fixed point in the unified chain. No downstream uses are recorded, yet the lemma underpins sibling constructions such as phiLadderScale and the beta-function lemmas.
scope and limits
- Does not prove positivity of φ.
- Does not supply a numerical value for φ.
- Does not derive any explicit beta function or running formula.
- Does not address extensions to complex or negative scalars.
formal statement (Lean)
76lemma phi_ne_zero' : phi ≠ 0 := ne_of_gt Constants.phi_pos
proof body
Term-mode proof.
77
78/-- φ > 1. -/