phi
plain-language theorem explainer
The declaration introduces the golden ratio φ as the real number (1 + sqrt(5))/2. Researchers modeling physical scales via the φ-ladder hypothesis cite this as the fundamental self-similar constant. The definition is a direct noncomputable assignment of the standard algebraic expression for the positive root of x² - x - 1 = 0.
Claim. Let φ = (1 + √5)/2.
background
The module RRF.Hypotheses.PhiLadder states the φ-ladder hypothesis: privileged physical scales satisfy X = X₀ · φⁿ for integer n, with examples such as particle masses m = B · E_coh · φ^r and timescales τ = τ₀ · φ^n. This definition supplies the base numerical value in the reals. The module treats the ladder as an explicit hypothesis that generates empirical prediction obligations rather than a definitional truth.
proof idea
The definition is a direct assignment of the closed-form expression (1 + Real.sqrt 5)/2. No lemmas or tactics are applied; the body is a simple arithmetic expression using Mathlib real operations.
why it matters
This definition anchors the φ-ladder hypothesis, which organizes scales by powers of φ and connects to the self-similar fixed point in the unified forcing chain (T6). It supplies the base for downstream mass formulas and Berry creation thresholds. No used-by edges are recorded, leaving open its precise integration with the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.