phi_inv3_interval_proven
plain-language theorem explainer
This definition supplies a closed rational interval guaranteed to contain (φ^{-1})^3. Numerics work in the Recognition framework cites it when certifying bounds on negative powers of the golden ratio. The construction is a direct record with a norm_num tactic discharging the endpoint inequality.
Claim. The closed interval $[2359/10000, 237/1000]$ containing $(φ^{-1})^3$.
background
The module derives rigorous bounds on φ = (1 + √5)/2 from algebraic comparisons of squares: 2.236² < 5 < 2.237² implies 2.236 < √5 < 2.237 and therefore 1.618 < φ < 1.6185. An Interval is the structure with rational endpoints lo, hi satisfying lo ≤ hi. This definition records one such interval specialized to (φ^{-1})^3.
proof idea
The definition constructs the Interval record with explicit rational fields lo := 2359/10000 and hi := 237/1000. The valid field is discharged by a single norm_num tactic that verifies the rational inequality.
why it matters
It supplies the concrete interval used by the downstream theorem phi_inv3_in_interval_proven to certify actual containment and by phi_pow_neg3_interval in the Pow module. The construction supports the phi-ladder mass formula and the eight-tick octave by providing error-free bounds on φ^{-3} = φ^{-1} cubed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.