sterile_bound_placeholder
plain-language theorem explainer
This lemma proves the positivity of the sterile neutrino mass bound in the Recognition Science framework. Model builders enforcing exactly three neutrino generations would cite it to ensure any fourth state exceeds a derived threshold. The term-mode proof multiplies the known positivity of the coherence energy with that of phi to the twentieth power after invoking the relevant constant lemmas.
Claim. Let $E_0$ denote the coherence energy and let $J$ be the J-cost function with fixed point $phi$. The sterile bound $E_0 phi^{20}$ satisfies $E_0 phi^{20} > 0$.
background
The SterileExclusion module encodes the modelling choice that only three neutrino generations exist, implemented via surjectivity of genOf onto Fin 3. The sterile_bound is defined as Constants.E_coh multiplied by phi raised to the twentieth power and serves as a placeholder threshold: any sterile m_ν4 must exceed φ^{19+Δ} E_coh with Δ>0 (exclusion if detected in the band). Upstream results include E_coh_pos lemmas from ConstantDerivations and PhiForcing that establish positivity from phi_pos in the forcing chain, together with the abstract Constants bundle from LawOfExistence.
proof idea
The proof first obtains phi > 0 and E_coh > 0 from Constants.phi_pos and Constants.E_coh_pos. It then applies Real.rpow_pos_of_pos to confirm phi^20 > 0 and concludes with mul_pos after commuting factors via simpa.
why it matters
This placeholder lemma supports the sterile neutrino exclusion assumption by verifying that the derived bound exceeds zero, consistent with the three-generation restriction. It aligns with forcing-chain landmarks T5 (J-uniqueness), T7 (eight-tick octave) and T8 (D = 3) by enforcing generational discreteness. The result closes a modelling stub without new hypotheses and feeds into downstream statements such as no_sterile_of_assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.