phi_neg_quarter_bounds
plain-language theorem explainer
The theorem establishes that the reciprocal of the upper quarter-root bound lies below the golden ratio to the negative one-quarter power, which itself lies below the reciprocal of the lower quarter-root bound. Numerics code in Recognition Science applications cites it when chaining bounds for negative phi powers in mass formulas and decay estimates. The proof is a tactic sequence that invokes the positive quarter bounds, rewrites the negative exponent as a reciprocal, and applies the reciprocal inequality lemma twice before reassembling the ∧.
Claim. Let ϕ denote the golden ratio. Let ϕ_quarter_lo and ϕ_quarter_hi be the lower and upper bounds on ϕ^{1/4}. Then (1 / ϕ_quarter_hi) < ϕ^{-1/4} < (1 / ϕ_quarter_lo).
background
The module supplies rigorous algebraic bounds on powers of the golden ratio ϕ = (1 + √5)/2. It starts from the comparison 2.236² < 5 < 2.237² to obtain 2.236 < √5 < 2.237, then derives the quarter-root interval ϕ_quarter_lo < ϕ^{1/4} < ϕ_quarter_hi by taking fourth roots and refining decimal places as described in the module strategy paragraph.
proof idea
The proof obtains the positive quarter bounds from phi_quarter_bounds. It establishes positivity of goldenRatio via Real.goldenRatio_pos and of its positive quarter power via rpow_pos_of_pos. The negative exponent is rewritten as the reciprocal using rpow_neg. Two calls to one_div_lt_one_div_of_lt invert the inequalities on each side, after which constructor and simpa reassemble the conjunction while normalizing the exponent notation.
why it matters
This supplies the inversion step for negative exponents on the phi-ladder, directly enabling the downstream results phi_neg2174_gt, phi_neg2174_lt and phi_neg58_lt that bound high negative powers for nucleosynthesis and complexity numerics. It supports the Recognition Science mass formula and the eight-tick octave by keeping all rational multiples of 1/4 under explicit control. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.