phi_quarter_hi
plain-language theorem explainer
The declaration supplies the concrete numerical upper bound 1.12783849 for the fourth root of the golden ratio φ. Interval-arithmetic and certified-numerics work in the Recognition Science framework cites this constant when sandwiching fractional powers of φ. The definition is a direct real-number assignment that downstream lemmas discharge via simp and norm_num.
Claim. Let $φ^{1/4}_hi := 1.12783849$. This constant functions as a certified upper bound for $φ^{1/4}$ where $φ = (1 + √5)/2$.
background
The Numerics.Interval.PhiBounds module supplies rigorous bounds on φ = (1 + √5)/2 by algebraic comparison of squares: 2.236² < 5 < 2.237² yields 1.618 < φ < 1.6185, with further decimal refinement for quarter roots. The module imports Basic interval machinery together with Mathlib facts on goldenRatio and real powers. Sibling definitions such as phi_quarter_lo and phi_gt_1618 establish the matching lower endpoint and coarser φ bounds.
proof idea
This is a direct definition that assigns the literal real value 1.12783849. No tactic steps or lemmas are invoked inside the declaration itself.
why it matters
The constant enters phi_quarter_bounds to produce the two-sided interval for φ^{1/4}, which is then inverted to obtain phi_neg_quarter_bounds and applied to high negative exponents in phi_neg2174_gt and phi_neg2314_lt. It anchors the numerical side of the phi-ladder used for mass formulas and the eight-tick octave in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.