phi_inv3_in_interval_proven
plain-language theorem explainer
phi_inv3_in_interval_proven establishes that the cube of the reciprocal of the golden ratio lies inside the rational interval with endpoints 0.2359 and 0.237. Mass and numerics modules cite the result to bound φ^{-3} in Recognition Science calculations. The tactic proof unfolds the containment predicate and discharges each side by invoking the companion lemmas phi_inv3_gt and phi_inv3_lt together with norm_num normalization.
Claim. $0.2359 < ((1 + √5)/2)^{-3} < 0.237$, where the bounds are the rational endpoints of the closed interval phi_inv3_interval_proven.
background
This module supplies rigorous rational bounds on powers of the golden ratio φ = (1 + √5)/2 using only algebraic inequalities. An Interval is a structure of rational endpoints lo and hi together with a proof that lo ≤ hi. The predicate contains asserts that a real number x satisfies lo ≤ x ≤ hi. The local strategy begins from the inequalities 2.236² < 5 < 2.237² to bound √5, then φ, and finally its reciprocal cubed. Upstream lemmas phi_inv3_gt and phi_inv3_lt supply the strict inequalities 0.2359 < φ^{-1}^3 and φ^{-1}^3 < 0.237.
proof idea
The proof is a short tactic script. It first simplifies the containment goal to the two-sided inequality via simp only [Interval.contains, phi_inv3_interval_proven]. The constructor splits into lower and upper bounds. For the lower bound it invokes the lemma phi_inv3_gt and rewrites the rational 2359/10000 into a real for comparison via calc and norm_num. The upper bound similarly uses phi_inv3_lt and normalizes 237/1000.
why it matters
This theorem closes the direct rational envelope for φ^{-3} and is invoked by the zpow-form bound phi_pow_neg3_in_interval in the Pow submodule. It supports the mass-ladder calculations that rely on phi^{-3} as a scaling factor in the Recognition framework. The bounds replace an earlier legacy statement and ensure that all subsequent numerical claims remain inside the phi-ladder without external floating-point libraries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.