pith. sign in
module module moderate

IndisputableMonolith.Masses.NeutrinoYardstick

show as:
view Lean formalization →

The NeutrinoYardstick module supplies the three rung assignments for neutrino mass eigenstates on the RS phi-ladder. Researchers computing neutrino mass sums or hierarchies inside the Recognition framework cite these definitions to obtain concrete mass values from the yardstick. The module consists entirely of definitions and elementary lemmas establishing positivity, ordering, and sum relations.

claimLet $r_1 < r_2 < r_3$ be the rung triple for the three neutrino mass eigenstates. The individual masses are $m_i = Y_0 · ϕ^{r_i - 8}$ and the sum is $m_1 + m_2 + m_3 = Y_0 · f$ where $Y_0$ is the neutrino yardstick and $f$ is the sum factor derived from the rung differences.

background

Recognition Science quantizes particle masses on the phi-ladder with base yardstick scaled by ϕ to the power (rung − 8). The imported Constants module fixes the fundamental time quantum τ₀ = 1 tick. This module specializes the general mass formula to neutrinos by introducing nu_rungs as the explicit integer triple, nuMass as the mass map, and nuMassSum together with sumFactor for the total mass.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The rung assignments close the neutrino sector of the mass formula and feed the general yardstick scaling used throughout the Masses domain. They support explicit numerical predictions for the neutrino mass sum while remaining consistent with the eight-tick octave and phi self-similarity of the forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)