phi_pow58_lt
The inequality supplies an upper bound phi^58 < 1.324e12 that closes a numerical step in the phi-ladder. Researchers deriving neutrino mass scales from Recognition Science would cite it when converting the phi^58 ceiling into a lower bound on phi^(-58). The proof rewrites the exponent as a product via phi_pow58_eq then chains the prior bounds phi_pow54_lt and phi_pow4_lt through a calc block with nlinarith.
claim$ (1 + 2.236)/2 < 1.618 < phi < 1.6185 < (1 + 2.237)/2 $ implies $ phi^{58} < 1.324 times 10^{12} $, where $ phi = (1 + sqrt{5})/2 $ is the golden ratio.
background
The Numerics.Interval.PhiBounds module supplies rigorous numerical ceilings on powers of the golden ratio by first tightening bounds on sqrt{5} from the inequalities 2.236^2 < 5 < 2.237^2, which immediately give 1.618 < phi < 1.6185. These base bounds are lifted to higher powers through repeated application of the algebraic identity phi^{m+n} = phi^m * phi^n together with explicit numerical comparisons. Upstream results used here are the equality phi^58 = phi^54 * phi^4, the bound phi^54 < 192983018016, and the bound phi^4 < 6.86.
proof idea
The tactic proof first rewrites the target via phi_pow58_eq. It then obtains the two factors from phi_pow54_lt and phi_pow4_lt, records positivity of both powers, and closes the claim with a three-step calc: the product is bounded by nlinarith, the second factor is replaced by its numerical ceiling by nlinarith, and the final multiplication is verified by norm_num.
why it matters in Recognition Science
This bound is invoked directly by the downstream theorem phi_neg58_gt that produces the lower bound phi^(-58) > 7.55e-13 required for neutrino mass predictions on the phi-ladder. It therefore supports the mass formula yardstick * phi^(rung - 8 + gap(Z)) and the T5 J-uniqueness step that forces phi as the self-similar fixed point in the eight-tick octave. The result tightens the numerical scaffolding needed to reach the alpha band and D = 3 spatial dimensions from the forcing chain.
scope and limits
- Does not give the exact decimal expansion of phi^58.
- Does not apply outside the real numbers.
- Does not replace the upstream bounds on phi^54 or phi^4.
- Does not establish a matching lower bound on phi^58.
Lean usage
have h58 : goldenRatio ^ 58 < (1.324e12 : ℝ) := phi_pow58_ltformal statement (Lean)
654theorem phi_pow58_lt : goldenRatio ^ 58 < (1.324e12 : ℝ) := by
proof body
Tactic-mode proof.
655 rw [phi_pow58_eq]
656 have h54 := phi_pow54_lt -- φ^54 < 192983018016
657 have h4 := phi_pow4_lt -- φ^4 < 6.86
658 have hpos54 : (0 : ℝ) < goldenRatio ^ 54 := by positivity
659 have hpos4 : (0 : ℝ) < goldenRatio ^ 4 := by positivity
660 calc goldenRatio ^ 54 * goldenRatio ^ 4 < (192983018016 : ℝ) * goldenRatio ^ 4 := by nlinarith
661 _ < (192983018016 : ℝ) * (6.86 : ℝ) := by nlinarith
662 _ < (1.324e12 : ℝ) := by norm_num
663
664/-! ## φ^(-58) bounds (for neutrino mass predictions) -/
665
666/-- φ^(-58) > 7.55e-13 (using φ^58 < 1.324e12) -/