phi_quarter_bounds
plain-language theorem explainer
The declaration consolidates certified rational bounds on the fourth root of the golden ratio. Numerics work in the Recognition Science framework cites it when constructing interval bounds for negative fractional powers such as φ^{-231/4}. The proof is a term-mode pairing of the separately established lower and upper inequalities.
Claim. Let φ denote the golden ratio. Then 1.12783847 < φ^{1/4} < 1.12783849, where the constants are the certified rational lower and upper bounds for the fourth root.
background
The module supplies rigorous algebraic bounds on φ = (1 + √5)/2. It begins from the inequalities 2.236² < 5 < 2.237², which imply 2.236 < √5 < 2.237 and therefore 1.618 < φ < 1.6185, then tightens the decimals for higher precision. The quarter-root bounds are defined as the certified rationals phi_quarter_lo = 1.12783847 and phi_quarter_hi = 1.12783849. Upstream results establish the separate lower and upper inequalities by monotonicity of the map x ↦ x^4 together with positivity of φ.
proof idea
The proof is a term-mode constructor that directly pairs the lower-bound theorem (proved via monotonicity of fourth power after normalizing the exponent) with the upper-bound theorem (proved by the same monotonicity argument). No additional tactics are required.
why it matters
It supplies the base interval used by the downstream theorems phi_neg_quarter_bounds, phi_neg2314_gt and phi_neg2314_lt. These intervals support the phi-ladder numerics required for the mass formula and the eight-tick octave in the Recognition Science framework. The module doc-comment records the algebraic strategy that generates all such bounds from square inequalities on √5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.