m2_approx_bounds
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 in Recognition Science
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.
scope and limits
- Does not derive absolute neutrino masses from the J-cost or Recognition Composition Law.
- Does not address the full three-neutrino mixing matrix or CP phases.
- Does not prove the rung assignment itself; it assumes rung_nu2 = -58 from upstream.
- Does not replace the display calibration seam that reuses electron_structural_mass in MeV units.
Lean usage
have h_m2 := m2_approx_boundsformal statement (Lean)
717lemma m2_approx_bounds : (0.0086 : ℝ) < m2_approx ∧ m2_approx < (0.0088 : ℝ) := by
proof body
Tactic-mode proof.
718 simp only [m2_approx, dm2_21_exp]
719 constructor
720 · -- 0.0086 < sqrt(7.53e-5)
721 have h1 : (0.0086 : ℝ)^2 < 7.53e-5 := by norm_num
722 have h_pos : (0 : ℝ) < 7.53e-5 := by norm_num
723 have h_sqrt_pos : 0 < Real.sqrt (7.53e-5) := Real.sqrt_pos.mpr h_pos
724 have h_086_pos : (0 : ℝ) ≤ 0.0086 := by norm_num
725 rw [← Real.sqrt_sq h_086_pos]
726 exact Real.sqrt_lt_sqrt (sq_nonneg _) h1
727 · -- sqrt(7.53e-5) < 0.0088
728 have h1 : (7.53e-5 : ℝ) < 0.0088^2 := by norm_num
729 have h_pos : (0 : ℝ) ≤ 7.53e-5 := by norm_num
730 have h_088_pos : (0 : ℝ) < 0.0088 := by norm_num
731 rw [← Real.sqrt_sq (le_of_lt h_088_pos)]
732 exact Real.sqrt_lt_sqrt h_pos h1
733
734/-- m2 matches the -58 rung to within tolerance (< 0.001 eV).
735
736 Proof: From nu2_pred_bounds and m2_approx_bounds,
737 |0.0082 - 0.0087| ≈ 0.0005 < 0.001 ✓ -/