phi_quarter_lo
plain-language theorem explainer
This definition supplies the numerical constant 1.12783847 as a certified lower bound for the fourth root of the golden ratio. Numerics researchers establishing interval enclosures for powers of φ in the Recognition Science framework would cite it to anchor subsequent inequalities. The declaration is a direct assignment of the decimal value with no computation or lemmas applied.
Claim. Define the constant $b = 1.12783847$. Then $b$ serves as a certified lower rational bound for $φ^{1/4}$, where $φ = (1 + √5)/2$.
background
The module develops rigorous numerical bounds for the golden ratio φ using algebraic inequalities on √5. It begins from the relations 2.236² < 5 < 2.237² to obtain 1.618 < φ < 1.6185 and refines the estimates with additional decimal places for quarter-root bounds. The local setting is interval arithmetic for the self-similar fixed point φ that appears in the Recognition Science forcing chain.
proof idea
This is a direct definition that assigns the decimal value 1.12783847 to the lower bound constant. No lemmas or tactics are invoked; the value is supplied as a hardcoded rational approximation.
why it matters
The bound feeds the consolidated statement phi_quarter_bounds and the monotonicity arguments in phi_quarter_gt, which in turn support interval results for negative powers such as φ^{-217/4} and φ^{-231/4}. Within the framework it supplies a concrete enclosure for the self-similar fixed point φ (T6) used in the phi-ladder mass formulas and the eight-tick octave. It closes a numerical scaffolding step for verifiable bounds on the Recognition Composition Law quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.