m2_approx_bounds
plain-language theorem explainer
The bound on the approximate second neutrino mass shows that its value, obtained as the square root of the experimental solar mass-squared difference 7.53 × 10^{-5} eV², satisfies 0.0086 eV < m₂ < 0.0088 eV. Neutrino phenomenology groups using the Recognition Science framework would reference this to confirm consistency with the deep-ladder rung assignment at -58. The proof reduces the inequality to squared comparisons via algebraic simplification and applies the strict monotonicity of the positive square root function.
Claim. $0.0086 < m_2 < 0.0088$ (in eV), where $m_2 = (7.53 × 10^{-5})^{1/2}$ is the square root of the experimental solar mass-squared splitting.
background
The NeutrinoSector module places neutrino masses on the deep phi-ladder at even integer rungs near -50 to -60, with m3 at rung -54 and m2 at rung -58. The quantity m2_approx is obtained directly as the square root of dm2_21_exp, the experimental solar mass-squared difference fixed at 7.53 × 10^{-5} eV². This supplies a numerical check against the structural mass prediction m_struct · phi^{-58} ≈ 0.0082 eV. Upstream rung definitions from RSBridge.Anchor assign the ladder positions for fermions, while the module doc notes that the residue difference Δ_{32} = 4 suggests a quarter-ladder spacing.
proof idea
The tactic proof first simplifies m2_approx and dm2_21_exp to unfold the square root expression. It splits the conjunction into two inequalities. For the lower bound, norm_num confirms 0.0086² < 7.53e-5, positivity is recorded, and Real.sqrt_lt_sqrt is applied after rewriting with sqrt_sq. The upper bound follows identically by verifying 7.53e-5 < 0.0088² and invoking the same monotonicity lemma.
why it matters
This lemma is invoked inside nu2_match to establish that the predicted mass at rung_nu2 lies within 0.001 eV of the experimental scale. It completes the verification step for the solar neutrino mass in the T14 neutrino sector derivation, anchoring the phi-ladder mass formula to observed Δm² values. In the Recognition Science framework it supports extension of the eight-tick octave and deep-ladder structure beyond the electron rung, confirming consistency with the yardstick · phi^(rung - 8 + gap) scaling for neutrinos.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.