phi_pow59_lt
plain-language theorem explainer
The inequality goldenRatio^59 < 2139810000000 is established in the reals by factoring the exponent and chaining prior upper bounds. Mass verification code in the Recognition framework cites this result when confirming the phi-ladder placement for particle masses at rung 59. The proof rewrites the power as a product, invokes the established bounds on the factors, and closes the chain with linear arithmetic and numerical normalization.
Claim. $phi^{59} < 2139810000000$ where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
This module supplies rigorous upper bounds on successive powers of the golden ratio using its minimal polynomial and interval comparisons on sqrt(5). The module strategy starts from 2.236 < sqrt(5) < 2.237 to obtain 1.618 < phi < 1.6185, then lifts these base bounds to higher exponents by multiplication. The local setting imports the Mathlib definition of goldenRatio together with real power and positivity tactics.
proof idea
The proof begins with a ring normalization that rewrites goldenRatio^59 as the product goldenRatio^51 * goldenRatio^8. It retrieves the upstream theorems phi_pow51_lt (goldenRatio^51 < 45537549354) and phi_pow8_lt (goldenRatio^8 < 46.99), adds a positivity fact for the eighth power, and applies a calc block that multiplies the first bound by the second factor, replaces the factor by its own bound, and finishes with norm_num.
why it matters
The result is invoked by the lemma phi59_lt inside IndisputableMonolith.Masses.Verification, which rewrites Constants.phi to goldenRatio and applies this bound directly. It supplies a concrete numerical anchor for the phi-ladder mass formula at exponent 59, consistent with the self-similar fixed point phi and the eight-tick octave. The declaration closes one link in the precomputed ladder used for mass verification; no scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.