phi_inv5_in_interval_proven
plain-language theorem explainer
The result shows that the fifth power of the reciprocal of the golden ratio satisfies 0.089 < (φ^{-1})^5 < 0.091. Workers confirming numerical intervals for golden-ratio powers in Recognition Science cite this bound when checking constants such as ħ. The tactic proof splits interval membership into separate lower and upper inequalities drawn from dedicated lemmas and applies le_of_lt after norm_num rewrites.
Claim. Let φ = (1 + √5)/2. Then 0.089 ≤ φ^{-5} ≤ 0.091.
background
The module derives rigorous bounds on φ using comparisons of squares near 5. It shows 2.236² < 5 < 2.237² to sandwich √5 and thus φ between 1.618 and 1.6185, with tighter decimal bounds obtained by the same method. An interval is a structure carrying rational lower and upper endpoints that satisfy lo ≤ hi. Containment of a real x holds precisely when lo ≤ x and x ≤ hi.
proof idea
The proof unfolds the containment predicate and applies the constructor tactic to the resulting conjunction. For the lower bound it invokes the dedicated lower lemma together with a norm_num calculation that rewrites 89/1000 to 0.089, then uses le_of_lt. The upper bound is obtained symmetrically from the upper lemma and the matching rewrite of 91/1000 to 0.091.
why it matters
The bound supplies a concrete numerical check for φ^{-5} that is invoked by the theorem establishing containment of the negative fifth power in the Pow module. Within Recognition Science it certifies the constant ħ = φ^{-5} that appears in the forcing chain after the self-similar fixed point is fixed. The result closes a numerical verification step without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.