phi_pow51_interval_proven
plain-language theorem explainer
phi_pow51_interval_proven supplies the closed rational interval with endpoints 45537548334 and 45537549354 that is asserted to contain φ^51. Numerics work in the Recognition framework cites this definition when certifying enclosures for golden-ratio powers that feed mass-ladder calculations. The definition is witnessed by a single norm_num tactic that certifies the endpoint ordering.
Claim. Define the closed interval $I$ with rational endpoints $lo = 45537548334$ and $hi = 45537549354$ satisfying $lo ≤ hi$.
background
The module supplies rigorous rational bounds on powers of the golden ratio φ = (1 + √5)/2. An Interval is the structure consisting of rational endpoints lo and hi together with a proof that lo ≤ hi. The module strategy begins from the algebraic inequalities 2.236² < 5 < 2.237² and tightens them for higher powers of φ.
proof idea
The definition constructs the Interval record directly. The validity field is discharged by a single norm_num tactic that reduces the comparison of the two literal rationals to a decidable numerical fact.
why it matters
This definition supplies the concrete bounds required by the theorem phi_pow51_in_interval_proven that certifies φ^51 lies inside the interval. The same endpoints are reused to define phi_pow_51_interval in the Pow module for neutrino-mass predictions. It closes the numerical certification step that begins from the self-similar fixed point φ in the Recognition forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.