nu2_abs_mass_interval
plain-language theorem explainer
The theorem establishes that the predicted absolute mass of the second neutrino lies strictly between zero and 0.012 in natural units. Neutrino physicists working within the Recognition Science framework would cite it when bounding the solar neutrino mass scale on the phi-ladder. The proof is a one-line term wrapper that pairs the positivity result with the upper bound derived from the phi-ladder rung at -26.
Claim. $0 < m_2 < 0.012$, where $m_2$ is the absolute mass of the second neutrino predicted from the solar splitting floor via the phi-ladder mass formula.
background
The module treats observed neutrino mass differences inside Recognition Science, with masses placed on the phi-ladder via the yardstick times phi to a rung power. The definition m_nu2_pred sets the rung to -26 to match the solar splitting floor, yielding a noncomputable real that inherits positivity and scaling from phi properties. Upstream, the positivity theorem applies mul_pos to the yardstick and zpow_pos on phi, while the upper-bound theorem invokes zpow_neg_lt_one followed by nlinarith to cap the value below 0.012.
proof idea
The proof is a term-mode constructor that directly pairs the two upstream theorems: the positivity result and the upper-bound result for the same predicted mass. No additional tactics or reductions are performed; the conjunction is formed by the angle-bracket syntax.
why it matters
The interval supplies a concrete absolute-mass anchor for the second neutrino inside the solar sector of the hierarchy. It rests on the phi-ladder mass formula and the rung assignment tied to observed splittings, consistent with the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain. No downstream theorems are recorded yet, leaving open whether it will feed sum_mass_bound or seesaw-scale relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.