qlo_pos
plain-language theorem explainer
The positivity lemma for the certified lower bound on the fourth root of the golden ratio asserts that this explicit rational exceeds zero. Researchers performing interval arithmetic on negative fractional powers of φ cite it to secure sign conditions in exponentiation steps. The proof reduces the claim to the concrete numerical value through simplification and normalization tactics.
Claim. $0 < φ^{1/4}_{lo}$ where $φ^{1/4}_{lo}$ denotes the certified lower rational bound 1.12783847 for the fourth root of the golden ratio $φ = (1 + √5)/2$.
background
The module supplies rigorous bounds on the golden ratio using algebraic inequalities on its square root. It establishes 2.236 < √5 < 2.237 from squaring comparisons, yielding 1.618 < φ < 1.6185, with further refinements for higher precision. The auxiliary definition provides a certified lower rational bound specifically for φ to the power one-fourth.
proof idea
The proof proceeds as a one-line term wrapper. Simplification unfolds the explicit definition of the lower bound, after which numerical normalization confirms the positive inequality.
why it matters
It underpins the lower bound theorem for φ to the power -231/4 in the same module. This supports numerical checks in the Recognition Science pipeline for the phi-ladder mass formula and the self-similar fixed point at T6. The result closes a minor verification step in the interval bounds that feed into the eight-tick octave and spatial dimension derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.