phi_pow_neg3_in_interval
plain-language theorem explainer
The theorem shows that the golden ratio raised to the power -3 lies inside the closed rational interval with endpoints 0.2359 and 0.237. Numerics researchers constructing verified bounds for the Recognition Science phi-ladder would cite this when validating mass formulas that scale by phi to negative rungs. The proof rewrites the power via the golden-ratio definition, reduces it to the cubed reciprocal case, and applies linear arithmetic to a prior containment result.
Claim. Let $phi = (1 + sqrt(5))/2$. Then $phi^{-3}$ belongs to the closed interval $[0.2359, 0.237]$.
background
The module supplies interval arithmetic for the power function on positive reals, using the identity $x^y = exp(y log x)$ together with direct computation for integer exponents. An Interval is a structure carrying rational endpoints lo and hi with the invariant lo <= hi; the predicate contains asserts that a real number x satisfies lo <= x <= hi. The local theoretical setting is rigorous numerical verification of powers of phi to support the Recognition framework's mass and constant formulas.
proof idea
The tactic proof simplifies the containment predicate, rewrites via the golden-ratio formula, and applies real-power identities to equate phi^{-3} with (phi^{-1})^3. It then invokes the already-proven containment for the cubed reciprocal and finishes with constructor plus linarith after norm_num conversions of the rational endpoints.
why it matters
This result supplies a concrete verified bound for the phi^{-3} term that appears in the Recognition Science mass formula and the dream-fraction threshold. It closes a verification step in the numerics layer that feeds the phi-ladder construction (T5 J-uniqueness and T6 phi fixed point). No downstream theorems yet reference it directly, but it removes a scaffolding obligation for interval-based checks of the eight-tick octave and alpha-band constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.