phi_def
plain-language theorem explainer
The lemma equates the Recognition Science constant φ to Mathlib's Real.goldenRatio. It is cited by the immediate sibling lemmas that establish φ > 1, φ ≠ 0, and the quadratic identity φ² = φ + 1. The proof is a one-line term-mode reflexivity that unfolds the constant definition from the imported Constants structure.
Claim. Let φ denote the golden-ratio constant appearing in the CPM constants bundle. Then φ equals the classical golden ratio (1 + √5)/2.
background
The PhiSupport.Lemmas module supplies elementary algebraic facts about the golden ratio for use in Recognition Science certificates. It depends on the Constants structure from LawOfExistence, an abstract bundle packaging Knet, Cproj, Ceng, Cdisp with the non-negativity hypothesis 0 ≤ Knet, and on Mathlib's Real.goldenRatio. The module setting is restricted to real-algebraic identities that support the phi-ladder and fixed-point properties.
proof idea
The proof is a one-line term proof consisting solely of reflexivity (rfl). This succeeds because Constants.phi is definitionally equal to Real.goldenRatio in the imported module.
why it matters
The equality anchors φ to the standard mathematical object whose fixed-point property φ = 1 + 1/φ and quadratic relation φ² = φ + 1 are required for T5 (J-uniqueness) and T6 (phi forced as self-similar fixed point) in the unified forcing chain. It is used directly by the lemmas one_lt_phi, phi_ne_zero, and phi_squared, which in turn feed mass formulas on the phi-ladder and the eight-tick octave. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.