zpow_neg_lt_one
plain-language theorem explainer
The lemma shows that phi to any negative integer power is strictly less than 1. Neutrino mass hierarchy calculations cite it to bound predicted absolute masses below 0.012 eV and to confirm the sum lies under the Planck limit. The tactic proof multiplies by the positive power to recover 1, applies one_lt_pow with the phi_gt_onePointSixOne bound, and closes via nlinarith on positivity.
Claim. For every positive integer $n$, $phi^{-n} < 1$, where $phi > 1$ is the golden ratio.
background
The NeutrinoMassHierarchy module predicts neutrino masses on the phi-ladder via nuMassAtRung and nuYardstick, with negative exponents producing the small values needed to match cosmological bounds. The golden ratio satisfies phi > 1.61 by the upstream lemma phi_gt_onePointSixOne. Upstream structures such as PhiForcingDerived.of encode the J-cost and LedgerFactorization.of calibrate the underlying multiplicative group.
proof idea
The proof first obtains phi ≠ 0 from phi_pos. It rewrites phi^{-n} * phi^n = 1 via zpow_add₀ and zpow_natCast. It then shows 1 < phi^n by one_lt_pow₀ using linarith on phi_gt_onePointSixOne. nlinarith with zpow_pos finishes the inequality.
why it matters
The lemma is invoked by nu1_abs_mass_upper, nu2_abs_mass_upper, and nu_sum_bound_consistent to discharge the phi^{-k} < 1 steps that convert ladder predictions into concrete eV bounds. It operationalizes the phi > 1 property from the forcing chain (T5 J-uniqueness) so that the eight-tick octave and D = 3 dimensions yield neutrino masses inside the observed alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.