nu1_frac_pred_bounds
plain-language theorem explainer
The lemma establishes tight bounds placing the fractional predicted mass of the lightest neutrino between 0.00352 and 0.00355 after eV calibration. Researchers checking the Recognition Science deep-ladder neutrino masses against NuFIT oscillation data would cite this result. The proof unfolds the mass display calibration, splits the exponent using the rung spacing relation, and combines multiplication inequalities from the golden ratio power bounds.
Claim. Let $m_1$ be the predicted mass in eV for the lightest neutrino obtained by scaling the structural mass by the golden ratio to the power of the assigned rung. Then $0.00352 < m_1 < 0.00355$.
background
The NeutrinoSector module derives neutrino masses by assigning them to deep rungs on the phi-ladder, far below the electron rung at 2. The structural mass is supplied by the electron mass necessity result, treated as MeV and converted to eV by multiplying by 10^6. The scale function from LargeScaleStructureFromRS defines powers of phi as the mass scaling operator. The toReal function transports values from the logic reals to the standard reals for numerical comparison. The local theoretical setting is the T14 hypothesis that neutrinos occupy even integers around -50 to -58 with a quarter-ladder spacing of 4.
proof idea
The proof begins by unfolding the legacy mass display calibration and the MeV to eV conversion. It imports the structural mass bounds and equates the golden ratio to its real definition. Using the rung spacing equality, it rewrites the exponent for the lightest neutrino rung as the exponent for the next rung minus 2. It then applies the proved inequalities on phi to the power -231/4 and on phi to the power -2. Multiplication inequalities are chained to bound the product, which is then scaled by the positive structural mass and the 1e6 factor to reach the target interval.
why it matters
This bound is directly invoked by the row_nu1_frac theorem in the NeutrinoMassScaleScoreCard and supplies the m1 value used in the delta m squared consistency checks dm2_21_frac_pred_in_nufit_1sigma and dm2_31_frac_pred_in_nufit_2sigma. It completes the numerical verification step for the lightest neutrino rung in the T14 neutrino sector derivation. Within the Recognition Science framework it supports the phi-ladder mass formula by confirming the deep ladder produces values inside experimental bands. It leaves open the replacement of the calibration seam by a native RS unit derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.