pith. machine review for the scientific record. sign in
def definition def or abbrev high

deltam31_sq

show as:
view Lean formalization →

The definition supplies the experimental atmospheric neutrino mass-squared splitting Δm₃₁² = 2.51 × 10^{-3} eV² for use in RS neutrino calculations. Neutrino modelers cite it when checking mass ratios against φ^7. The assignment is a direct numerical constant with no internal steps.

claimThe atmospheric neutrino mass-squared difference equals $2.51 × 10^{-3}$ in units of eV².

background

The PMNSMatrix module develops the Pontecorvo-Maki-Nakagawa-Sakata matrix from φ-quantized angles in Recognition Science. Neutrino flavor mixing involves large angles unlike the CKM matrix, with θ₂₃ near 45° suggesting symmetry. This definition provides the input Δm₃₁² drawn from the upstream NeutrinoMassHierarchy module for mass ratio computations. The local setting is SM-014 targeting derivation of PMNS from RS with patent potential in PRD on golden ratio geometry.

proof idea

The declaration is a one-line definition assigning the numerical constant 2.51e-3 directly to the real-valued constant.

why it matters in Recognition Science

This constant is referenced by the mass_ratio definition and the theorems mass_ratio_phi4 and mass_ratio_phi7, which bound the deviation from φ^7. It fills the numerical input for the paper proposition on neutrino mixing angles from golden ratio geometry. Within the framework it supports the phi-ladder mass formulas and connects to the self-similar fixed point phi.

scope and limits

formal statement (Lean)

 164noncomputable def deltam31_sq : ℝ := 2.51e-3  -- eV²

proof body

Definition body.

 165

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.