mass_ratio_phi4
plain-language theorem explainer
The theorem shows that the ratio of estimated neutrino masses m3 to m2, scaled by phi to the fourth power, satisfies an absolute deviation from 1 of less than 0.2. Neutrino model builders checking golden-ratio patterns against oscillation data would cite it. The tactic proof unfolds the square-root estimates from the two observed squared mass splittings, inserts the interval bounds 1.618 < phi < 1.6185, and verifies the numerical ratio interval is compatible with phi^4 within the stated tolerance.
Claim. Let $m_3 = (2.51times10^{-3})^{1/2}$ and $m_2 = (7.42times10^{-5})^{1/2}$ (in eV). Then $left| (m_3/m_2)/phi^4 - 1 right| < 0.2$.
background
The module treats observed neutrino mass-squared differences as fixed numerical inputs: deltam21_sq = 7.42e-5 and deltam31_sq = 2.51e-3. From these it forms the estimates m2_estimate = sqrt(deltam21_sq) and m3_estimate = sqrt(deltam31_sq), then defines m3_m2_ratio as their quotient. Upstream lemmas supply the tight interval 1.618 < goldenRatio < 1.6185 together with the auxiliary bound phi_pow4 that converts the interval into 6.8 < phi^4 < 6.9. The local setting is the section on observed mass differences for the neutrino sector.
proof idea
Unfold m3_m2_ratio, m3_estimate, m2_estimate, deltam31_sq and deltam21_sq. Replace phi by goldenRatio and invoke phi_gt_1618 together with phi_lt_16185. Establish that sqrt(2.51e-3 / 7.42e-5) lies strictly between 5.8 and 5.9. Bound phi^4 from above by 6.9 and from below by 6.8 via phi_pow4 and linarith. Apply lt_div_iff0 and sub_lt_iff_lt_add (after clearing the common factor 1000) to obtain the two sides of abs_lt.
why it matters
The result supplies a quantitative consistency check that the observed neutrino mass ratio sits close to phi^4, consistent with the Recognition Science mass formula yardstick * phi^(rung-8+gap(Z)) on the phi-ladder. It therefore supports the claim that the eight-tick octave and self-similar fixed point phi govern the Standard Model fermion spectrum. No downstream theorems are recorded, indicating the declaration functions as an isolated numerical verification rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.