qhi_pos
plain-language theorem explainer
The lemma establishes that the certified upper rational bound for φ^{1/4} is strictly positive. Numerics researchers cite it when building interval bounds for quarter-ladder exponents in Recognition Science. The proof is a one-line wrapper that unfolds the definition via simp and verifies the numerical constant with norm_num.
Claim. $0 < 1.12783849$ where $1.12783849$ is the certified upper rational bound for the fourth root of the golden ratio φ.
background
The module supplies rigorous algebraic bounds on the golden ratio φ = (1 + √5)/2. It starts from 2.236² < 5 < 2.237² to obtain 1.618 < φ < 1.6185 and then tightens these for fractional powers. The sibling definition phi_quarter_hi supplies the concrete upper rational 1.12783849 for φ^{1/4}.
proof idea
One-line wrapper that applies simp to unfold phi_quarter_hi and norm_num to confirm the positive constant.
why it matters
This positivity check is required to support quarter/half-ladder neutrino rungs without numeric axioms. It is invoked directly by phi_neg2174_gt to establish the lower bound on φ^{-217/4} = φ^{-54} · φ^{-1/4} via splitting the exponent and monotone multiplication. The result aligns with the module strategy of combining proven integer-power bounds with Real.rpow_add.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.