phi_sq
plain-language theorem explainer
The golden ratio satisfies its characteristic equation φ² = φ + 1. Researchers modeling physical scales via the φ-ladder hypothesis cite this identity when assigning rung numbers to masses or timescales. The proof unfolds the explicit definition of φ and reduces the equation by ring normalization after invoking the square of the square root of five.
Claim. Let φ = (1 + √5)/2. Then φ² = φ + 1.
background
The φ-ladder hypothesis states that privileged physical scales satisfy X = X₀ · φⁿ for integer n, generating testable predictions for particle masses and timescales rather than serving as a definition. Action is the type of real numbers used for scaling operations. The spin value extracts the numerical spin from the Spin type as a real. The module frames this as an explicit hypothesis whose falsification criteria include finding a scale whose ratio to another is not an integer power of φ.
proof idea
The term proof unfolds the definition of phi, asserts (√5)² = 5 via Real.sq_sqrt, applies ring_nf to normalize, rewrites with the square fact, and closes with ring.
why it matters
This identity supplies the algebraic foundation for the φ-ladder hypothesis that organizes scales by integer powers of φ. It aligns with the self-similar fixed point T6 in the forcing chain and supports downstream mass formulas of the form yardstick · φ^(rung - 8 + gap(Z)). No immediate uses are recorded, leaving open its integration with the eight-tick octave and Berry creation threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.