phi_quarter_lo_pow4_lt_phi_lo
plain-language theorem explainer
This lemma certifies that raising the rational lower bound 1.12783847 for φ^{1/4} to the fourth power stays strictly below 1.61803395. Numerics researchers tightening interval bounds on the golden ratio in Recognition Science cite it to anchor subsequent monotonicity arguments. The proof is a one-line wrapper that unfolds the bound definition and dispatches the numerical comparison.
Claim. Let φ_{1/4}^- := 1.12783847. Then (φ_{1/4}^-)^4 < 1.61803395.
background
The module supplies rigorous rational bounds on φ = (1 + √5)/2 by first establishing 2.236 < √5 < 2.237 from squaring comparisons, then deriving 1.618 < φ < 1.6185 and tightening the decimals for higher precision. The upstream definition phi_quarter_lo supplies the certified lower rational bound 1.12783847 for φ^{1/4}.
proof idea
The proof is a one-line wrapper. It applies simp to unfold phi_quarter_lo and then norm_num to verify the concrete numerical inequality.
why it matters
The lemma feeds the theorem phi_quarter_gt, which proves the strict inequality phi_quarter_lo < φ^{1/4} via monotonicity of x ↦ x^4. It anchors the chain of φ bounds that support the self-similar fixed point T6 and the constants (c = 1, ħ = φ^{-5}) in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.