Neutrino Mass: Formal Verification of Oscillation, Seesaw, and Cosmological Constraints
Abstract
We present a formally verified treatment of neutrino mass physics, establishing 15 theorems covering oscillation phenomenology, mass splittings, cosmological constraints, seesaw mechanisms, and leptogenesis compatibility. The proofs span from surface-level observational results (oscillation implies mass, tritium endpoint bounds) to deep theoretical structures (Type-I and Type-II seesaw, hierarchy minimum sums, seesaw-leptogenesis compatibility). All theorems are verified at L3 level in the Platonic proof kernel, with connections established to baryogenesis (via Sakharov conditions) and dark matter (via sterile neutrino bounds). The formalization provides a rigorous foundation for BSM neutrino physics.
Keywords: neutrino oscillation, neutrino mass, seesaw mechanism, leptogenesis, PMNS matrix, cosmological bounds, formal verification
MSC 2020: 81V25 (Other elementary particle theory), 83F05 (Cosmology)