phi_inv3_interval_proven
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove that the true value of (φ^{-1})^3 lies inside the interval.
- Does not supply bounds for other exponents or for φ itself.
- Does not rely on floating-point or approximate arithmetic.
formal statement (Lean)
434def phi_inv3_interval_proven : Interval where
435 lo := 2359 / 10000
proof body
Definition body.
436 hi := 237 / 1000
437 valid := by norm_num
438