rung_nu3
plain-language theorem explainer
The definition rung_nu3 sets the third neutrino rung to the integer -54 on the phi-ladder. Modelers of neutrino masses within Recognition Science cite this assignment to compute the atmospheric scale from the structural mass. It is a direct constant definition requiring no lemmas or tactics.
Claim. The rung for the third neutrino mass eigenstate is the integer $-54$.
background
In the T14 Neutrino Sector module, neutrinos occupy the deep ladder at even integers near -50, well below the electron rung of 2. The documentation assigns m3 to rung -54, so that m3 ≈ m_struct ⋅ φ^{-54} ≈ 0.056 eV after converting the structural mass from MeV to eV via the display calibration. This setup draws on the phi-ladder mass formula and upstream bounds such as structural_mass_bounds from ElectronMass.Necessity. The residue Δ32 = 4 suggests a quarter-ladder spacing.
proof idea
This declaration is a bare definition that directly assigns the constant -54 to rung_nu3. No lemmas are applied and the proof body is empty.
why it matters
rung_nu3 provides the input rung for NeutrinoMassCert, which packages the m3 and m2 match certificates, and for nu3_match which verifies the atmospheric scale to within 0.01 eV. It realizes the deep ladder hypothesis in the Recognition framework, linking to the mass scaling on the phi-ladder and the eight-tick structure. It leaves open the derivation of the specific rung choice from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.