typicalDiracMass
plain-language theorem explainer
typicalDiracMass fixes the Dirac neutrino mass scale at 100 in Recognition Science units. Neutrino modelers applying the seesaw mechanism cite it to recover the observed 1e-10 suppression scale. The declaration is a direct constant assignment with no computational steps.
Claim. The typical Dirac neutrino mass scale equals 100 in the framework's natural units.
background
The NeutrinoMassHierarchy module examines observed mass differences for neutrinos in the Standard Model. typicalDiracMass supplies the representative Dirac mass input to the seesaw formula. The module imports Constants and PhiBounds to keep scales consistent with phi-ladder predictions.
proof idea
This declaration is a one-line definition that directly assigns the real number 100.
why it matters
It supplies the Dirac mass input to the seesaw_gives_small_mass theorem, which proves the effective neutrino mass equals 1e-10. This supports the φ-Connection to the Seesaw Scale section. In the broader framework it aligns with the mass formula on the phi-ladder and the T5 J-uniqueness plus T6 phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.