phi_hi_lt_phi_quarter_hi_pow4
plain-language theorem explainer
The lemma confirms that 1.6180340 lies strictly below the fourth power of the upper approximation phi_quarter_hi to φ^{1/4}. Researchers maintaining interval bounds on the golden ratio in Recognition Science numerics cite this verification. The proof proceeds by direct simplification of the bound constant followed by numerical evaluation.
Claim. Let $1.6180340$ be the lower numerical approximation to the golden ratio φ and let φ_quarter_hi be the upper numerical bound on φ^{1/4}. Then $1.6180340 <$ φ_quarter_hi$^4$.
background
The module supplies rigorous numerical bounds on the golden ratio φ = (1 + √5)/2 by bounding √5 between successive decimals such as 2.236 and 2.237. This yields the base interval 1.618 < φ < 1.6185, which is tightened by higher-precision constants. The local setting is algebraic verification of these bounds to support the φ-ladder in physical derivations.
proof idea
simp unfolds the definition of phi_quarter_hi. norm_num then confirms the concrete numerical inequality.
why it matters
The result is invoked by the theorem phi_quarter_lt that proves goldenRatio^{1/4} < phi_quarter_hi via monotonicity of the fourth-power map. It anchors the phi-ladder construction central to the Recognition Science framework, specifically the self-similar fixed point at T6 and the eight-tick octave at T7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.