m3_estimate
plain-language theorem explainer
This definition supplies an estimate for the heaviest neutrino mass by scaling the square root of the atmospheric mass-squared difference to milli-electronvolt units. Particle physicists testing Recognition Science mass predictions against oscillation data would reference it when constructing ratios on the phi ladder. It is implemented as a direct one-line extraction from the constant deltam31_sq.
Claim. Define the neutrino mass estimate $m_3 := 1000 sqrt(Delta m_{31}^2)$, where the input $Delta m_{31}^2$ equals 2.51 times 10^{-3} in units of eV squared.
background
The module addresses observed mass differences in the neutrino sector under the Recognition Science framework. Upstream, deltam31_sq is defined as the constant 2.51e-3 eV² representing the squared mass splitting between the third and first neutrino mass eigenstates. An identical definition appears in the PMNSMatrix module to maintain consistency in the hierarchy calculations.
proof idea
The definition is a one-line wrapper that computes the square root of deltam31_sq and multiplies the result by 1000.
why it matters
m3_estimate enters the definition of m3_m2_ratio, which is used in the theorem mass_ratio_phi4 to verify that the ratio lies within 0.2 of phi to the fourth power. This supports the connection between observed neutrino splittings and the self-similar fixed point phi in the eight-tick octave structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.