nu_sum_bound_consistent
The theorem shows that the sum of the three phi-ladder neutrino mass predictions lies strictly below the Planck cosmological upper limit of 0.12 eV. Cosmologists and model builders working in the Recognition Science Standard Model extension cite it when fixing absolute masses from oscillation data and large-scale structure constraints. The proof unfolds the rung-specific mass definitions, proves three elementary bounds on negative powers of phi together with their positivity, and closes the inequality by nlinarith.
claimLet $m_1$, $m_2$, $m_3$ be the predicted neutrino masses obtained from the yardstick at rung $-28$ scaled by the indicated negative powers of phi, and let $B$ be the Planck sum-mass bound. Then $m_1 + m_2 + m_3 < B$.
background
In the Recognition Science Standard Model module, neutrino masses are constructed via the seesaw mechanism with the right-handed scale fixed by the phi-ladder relation proved in seesaw_scale_phi_connection. The yardstick nuYardstick supplies the base mass at rung $-28$; the three generations are then placed at rungs $-28$, $-26$ and $-20$. The function sum_mass_bound is the numerical Planck limit expressed in the same units. Upstream lemmas supply the rung map from Compat.Constants and the discrete scale phi^k from Cosmology.LargeScaleStructureFromRS, which together embed all masses on the phi-ladder.
proof idea
The tactic proof begins by unfolding m_nu1_pred, m_nu2_pred, m_nu3_pred, nuMassAtRung, nuYardstick and sum_mass_bound. It then constructs three auxiliary facts (h20, h26, h28) showing that phi to the powers $-20$, $-26$ and $-28$ are each strictly less than 1, together with the three positivity statements pos20, pos26, pos28. The final step applies nlinarith to the resulting linear combination and obtains the strict inequality.
why it matters in Recognition Science
nu_sum_bound_consistent is invoked directly inside nuAbsMassCert to supply the sum_bound field of the absolute-mass certificate. It thereby confirms that the phi-predicted seesaw masses remain compatible with the cosmological bound stated in the module comment on absolute mass intervals. The result supports the mass formula yardstick times phi to the appropriate rung offset and closes one consistency check required by the eight-tick octave assignment of fermion generations.
scope and limits
- Does not compute numerical mass values beyond the inequality.
- Does not derive the seesaw scale or yardstick from first principles.
- Does not distinguish normal from inverted hierarchy.
- Does not incorporate renormalization-group running of the masses.
Lean usage
have h : m_nu1_pred + m_nu2_pred + m_nu3_pred < sum_mass_bound := nu_sum_bound_consistentformal statement (Lean)
246theorem nu_sum_bound_consistent :
247 m_nu1_pred + m_nu2_pred + m_nu3_pred < sum_mass_bound := by
proof body
Tactic-mode proof.
248 unfold m_nu1_pred m_nu2_pred m_nu3_pred nuMassAtRung nuYardstick sum_mass_bound
249 have h20 : phi ^ (-20 : ℤ) < 1 := by
250 have := zpow_neg_lt_one 20 (by norm_num)
251 simp at this; exact this
252 have h26 : phi ^ (-26 : ℤ) < 1 := by
253 have := zpow_neg_lt_one 26 (by norm_num)
254 simp at this; exact this
255 have h28 : phi ^ (-28 : ℤ) < 1 := by
256 have := zpow_neg_lt_one 28 (by norm_num)
257 simp at this; exact this
258 have pos20 : (0 : ℝ) < phi ^ (-20 : ℤ) := zpow_pos phi_pos _
259 have pos26 : (0 : ℝ) < phi ^ (-26 : ℤ) := zpow_pos phi_pos _
260 have pos28 : (0 : ℝ) < phi ^ (-28 : ℤ) := zpow_pos phi_pos _
261 nlinarith
262
263/-! ## Absolute Mass Intervals from Seesaw Scale
264
265The seesaw scale M_R = 1.2×10^19 / φ^13 (proved: seesaw_scale_phi_connection).
266With m_D ≈ m_top ≈ 172 GeV at the seesaw scale, the Dirac mass is φ-related:
267 m_D = φ^21 × E_coh (GeV) × conversion_factor
268
269The absolute neutrino masses follow from:
270 m_νᵢ = m_D² / M_R = (m_D²) × φ^13 / 1.2×10^19 GeV
271
272This calibrates nuYardstick. With nuYardstick ≈ 0.0031 eV, the predictions:
273- m_ν₁ = 0.0031 × φ^(-28) ≈ 3.3 × 10^(-15) eV (below cosmological sensitivity)
274- m_ν₂ = 0.0031 × φ^(-26) ≈ 8.6 × 10^(-15) eV
275- m_ν₃ = 0.0031 × φ^(-20) ≈ 1.0 × 10^(-12) eV
276
277These are far too small — the yardstick calibration needs the full seesaw formula.
278For the oscillation-calibrated yardstick (0.0031 eV at rung -28 as an effective scale):
279The oscillation data gives m_ν₁ ≈ 0 (lightest), m_ν₂ ≈ 8.6 meV, m_ν₃ ≈ 50 meV.
280-/
281
282/-- Effective absolute mass of ν₁ is below 12 meV (cosmological sum bound / 10). -/