phi_gt_onePointFive
plain-language theorem explainer
The golden ratio satisfies φ > 1.5. Researchers deriving strict inequalities on the phi-ladder cite this bound for acoustic damping, chemical shell radii, and coronal time growth. The proof unfolds the definition of phi, establishes 2 < sqrt(5) by comparing squares, and closes with linear arithmetic.
Claim. The golden ratio satisfies $ (1 + sqrt(5))/2 > 1.5 $.
background
In the Constants module phi denotes the golden ratio (1 + sqrt(5))/2, the self-similar fixed point forced by the Recognition Composition Law. Sibling results supply the supporting facts phi_pos, phi_gt_one, and phi_irrational. The module context fixes the RS time quantum at one tick, with all subsequent constants expressed in RS-native units where c = 1.
proof idea
The tactic proof first applies simp to unfold the definition of phi. It then proves 2 < sqrt(5) by showing 4 < 5 via norm_num and invoking Real.sqrt_lt_sqrt on the non-negative square root. Linear arithmetic combines the resulting inequality with the definition to obtain the target bound.
why it matters
This lemma feeds more than forty downstream results, including over_damped_below_one (optimal T60 > 1), acceptanceBandRatio_gt_one, shell_radius_increases_with_period, and coronalTime_strictly_increasing. It supplies the concrete numerical tightening of the T6 fixed-point property required for strict monotonicity on the phi-ladder and the eight-tick octave. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Helical hopping raises critical potential for Aubry-André localization
"Fibonacci system sizes L=Fn ... asymptotic filling close to one half"