Golden Ratio Identities

Abstract

The real golden ratio satisfies its radical, fixed-point, and conjugate identities.

Theorem 1.1 (Radical, fixed-point, and conjugate identities).

$$\phi =\frac{1+\sqrt{5}}{2}\wedge {\phi }^2=\phi +1\wedge 1-\phi =-\frac{1}{\phi }$$

Proof. Machine-checked in Lean as D5/S0/Carrier/GoldenRatio.golden_ratio_spec (✓ std3). ∎

Citation. Thomas Koshy (2001). Fibonacci and Lucas Numbers with Applications. DOI: 10.1002/9781118033067.

Commentary.

One kernel-checked conjunction records the radical definition, the quadratic fixed point, and the negative-reciprocal conjugate identity.

References

• Truth anchor: D5/S0/Carrier/GoldenRatio.golden_ratio_spec
• Narrative reference: D5/S0/Conventions/Notation