phi_pos
plain-language theorem explainer
The theorem establishes that the golden ratio φ is strictly positive. Researchers working on the φ-ladder hypothesis cite this fact when assigning rungs to mass scales or timescales in the Recognition framework. The proof is a short term-mode reduction that unfolds the definition of φ, invokes positivity of the square root of five, and closes by linear arithmetic.
Claim. Let φ = (1 + √5)/2. Then 0 < φ.
background
The module states the φ-ladder hypothesis: privileged physical scales satisfy X = X₀ · φⁿ for integer n. Examples include particle masses m = B · E_coh · φʳ and timescales τ = τ₀ · φⁿ. The declaration supplies the elementary positivity fact presupposed by all rung calculations on the ladder.
proof idea
The proof unfolds the definition of φ, applies Real.sqrt_pos to obtain 0 < √5, and closes with linarith.
why it matters
This positivity result underpins the φ-ladder hypothesis in the RRF module and supports derivations of mass scales via the phi-ladder. It connects to the self-similar fixed point φ forced in the T6 step of the unified forcing chain. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.