phi_gt_one
plain-language theorem explainer
The golden ratio satisfies φ > 1. Workers on the φ-ladder hypothesis cite this to guarantee that positive integer powers increase scale values in mass and time formulas. The proof unfolds the definition of φ as (1 + √5)/2 and reduces the claim to √5 > 1 via square-root monotonicity and linear arithmetic.
Claim. Let φ = (1 + √5)/2. Then 1 < φ.
background
The module states the φ-ladder hypothesis: privileged physical scales satisfy X = X₀ · φⁿ for integer n, generating predictions for particle masses m = B · E_coh · φʳ and timescales τ = τ₀ · φⁿ. This is an explicit hypothesis, not a definitional truth, with falsification criteria including privileged scales whose ratios are not integer powers of φ. The constant φ is the positive root of x² = x + 1, introduced here to organize the ladder.
proof idea
The tactic proof unfolds the definition of φ. It introduces facts that 5 > 0, (√5)² = 5, and 1² = 1, then shows √5 > 1 by rewriting against √1 = 1 and applying sqrt monotonicity on the positives 1 < 5. The final step closes the original inequality with linarith.
why it matters
This inequality anchors the φ-ladder hypothesis in the RRF module, which supplies the scale organization used by phiScale, OnPhiLadder, and computeRung. It supports the self-similar fixed point φ in the unified forcing chain and the mass formula on the phi-ladder. The result is a proved basic fact with no downstream uses yet recorded in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.