Foundation Seesaw Mechanism Rs V3

The seesaw estimate

The seesaw mechanism is a standard physics idea for why neutrinos are so light. If a heavy right-handed neutrino with mass M_R exists, the ordinary neutrino mass m_ν is approximately m_D² / M_R, where m_D is a Dirac mass comparable to a charged lepton or quark. Put in a large M_R and the neutrino mass gets suppressed; the heavier the right-handed partner, the lighter the left-handed neutrino. That is the seesaw in one line.

The framework's module Seesaw_Mechanism_RS_v3 makes a structural estimate. It takes the right-handed mass at the grand unified theory scale, roughly 2×10¹⁶ GeV, and the Dirac mass at the top quark mass, 173 GeV. The formula gives m_ν ≈ (173 GeV)² / (2×10¹⁶ GeV) ≈ 1.5×10^-3 eV. The measured neutrino mass scale is around 0.05 eV. The estimate is within about a factor of thirty, which is the usual quality for a structural guess in this area; it is not a precise prediction.

What the machine-checked library establishes is narrower and cleaner. The module defines a cost function domainCost(m, e) = J(m/e), where J is the recognition cost function from the framework's core. It then proves three general facts about that cost: it vanishes when the two inputs are equal, it is nonnegative for positive inputs, and the constant φ − 3/2 is positive. Those are real theorems, checked by the library's kernel. But they are facts about the cost function itself, not about neutrinos. The module contains no definition of m or e in neutrino terms, so the seesaw physics is a research note attached to the file, not a proved result.

In Recognition Science, the same cost function J(x) = (x + 1/x)/2 − 1 is the unique function forced by five plain conditions, and it appears throughout the framework as a measure of mismatch. The seesaw module is an application attempt: it models the ratio of two masses as an input to that cost. The three proved facts are the cost's basic hygiene properties. The interesting physics, the link from the cost to neutrino masses, remains open.

The lesson for a reader is to separate the two layers. The seesaw formula is a classical physics estimate with a long history and a clear structural role. The framework's module proves a small set of general cost properties and attaches a research note about neutrinos. The note is the motivation; the theorems are the content. Knowing which is which is the whole game.

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The module does not prove the seesaw formula or any neutrino mass value. The framework does not derive the fine-structure constant or any coupling constant. The estimate 1.5e-3 eV is not a measured value and carries no uncertainty.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/Seesaw_Mechanism_RS_v3.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: