phi_quarter_gt
plain-language theorem explainer
The theorem establishes that a precomputed numerical lower bound is strictly less than the fourth root of the golden ratio. Numerics researchers tightening interval bounds on φ within the Recognition Science framework cite it to support consolidated quarter-root estimates. The proof reduces the claim to a fourth-power comparison via monotonicity of x ↦ x^4 on the positive reals, then chains two prior strict inequalities before invoking rpow_lt_rpow_iff.
Claim. Let ϕ⁻_{1/4} denote the numerical lower-bound constant. Then ϕ⁻_{1/4} < φ^{1/4}, where φ = (1 + √5)/2.
background
This module supplies rigorous numerical bounds on the golden ratio φ using algebraic comparisons with rational approximations to √5. The local setting is interval arithmetic for φ-powers that supports downstream calculations in the φ-ladder for mass formulas. The module strategy begins from the inequalities 2.236² < 5 < 2.237² to bound √5 and hence φ between 1.618 and 1.6185, with tighter decimal versions obtained by the same method.
proof idea
The proof first records non-negativity of both sides and positivity of the exponent 4. It normalizes the right-hand exponent to 4^{-1}, shows that the fourth power of the left side is less than φ by applying phi_quarter_lo_pow4_lt_phi_lo followed by phi_gt_161803395 and lt_trans, then lifts the fourth-power inequality back to the original claim via Real.rpow_lt_rpow_iff. A final simpa closes the normalized form.
why it matters
This result is the lower half of the consolidated quarter-root bounds theorem phi_quarter_bounds, which pairs it with the corresponding upper estimate. It supplies the numerical infrastructure required for the Recognition Science φ-ladder (yardstick · φ^{rung-8+gap(Z)}) and for the self-similar fixed point and eight-tick octave constructions (T6, T7). No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.