Golden Reciprocal Fixed Point

Abstract

The real golden ratio satisfies the reciprocal fixed-point equation.

Theorem 1.1 (The golden ratio is a reciprocal fixed point).

$$\phi =1+\frac{1}{\phi }$$

Proof. Machine-checked in Lean as D5/S0/Tower/GoldenFixedPoint.golden_ratio_reciprocal_fixed_point (✓ std3). ∎

Source. Repository-derived.

Commentary.

The equation is an arithmetic instance of the fixed-point clause in the source atom. It is obtained directly from the library’s exact golden-ratio reciprocal and conjugate identities.

This is an honest partial closure of that one equation only. The source’s combinator, diagonal, representability, convergence, and self-application readings remain unresolved.

References

• Truth anchor: D5/S0/Tower/GoldenFixedPoint.golden_ratio_reciprocal_fixed_point