phi_inv5_lt
plain-language theorem explainer
phi_inv5_lt establishes that the fifth power of the reciprocal of the golden ratio is strictly less than 0.091. Numerics work in Recognition Science cites it when tightening bounds on phi powers that enter constants such as hbar. The proof obtains the second and third power bounds, records positivity, rewrites the fifth power as their product, and finishes with nlinarith.
Claim. $ (φ^{-1})^5 < 0.091 $ where $ φ = (1 + √5)/2 $ is the golden ratio.
background
The module supplies rigorous upper bounds on powers of the reciprocal golden ratio using algebraic inequalities from bounds on √5. The Interval structure is a closed interval with rational endpoints lo and hi satisfying lo ≤ hi. Upstream results phi_inv2_lt and phi_inv3_lt supply the concrete inequalities (φ^{-1})^2 < 0.383 and (φ^{-1})^3 < 0.237, each proved by nlinarith after positivity checks.
proof idea
The tactic proof first records the second and third power bounds. It proves positivity of the inverse and its second and third powers via inv_pos and pow_pos. A ring step rewrites the fifth power as the product of those two powers. nlinarith then closes the goal.
why it matters
The result is invoked by phi_inv5_in_interval_proven to place the value inside a certified interval. It supports numerical certification of phi powers that appear in RS-native units, including ħ = φ^{-5} and the phi-ladder for mass formulas. It fills a concrete step in the phi-bound chain without touching open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.