sterile_bound
plain-language theorem explainer
The sterile_bound definition supplies a numerical threshold for any hypothetical fourth neutrino generation on the Recognition Science mass ladder. A physicist imposing the three-generation constraint from the surjectivity of genOf onto Fin 3 would cite this bound when modeling neutrino spectra. The definition is constructed as the product of the coherence energy and phi to the twentieth power, acting as a placeholder for the rung above 19.
Claim. The sterile neutrino mass bound is defined as $E_0 = E_{coh} phi^{20}$, where $E_{coh}$ is the coherence energy scale and $phi$ is the golden ratio fixed point.
background
In Recognition Science, fermion masses sit on the phi-ladder with rung numbers fixing the exponent of phi. The genOf function from RSBridge.Anchor maps the three known neutrinos (nu1, nu2, nu3) onto Fin 3, enforcing exactly three generations. Constants.E_coh is the base coherence energy taken from the CPM constants bundle that also supplies Knet, Cproj, and Ceng.
proof idea
This is a one-line definition that directly multiplies Constants.E_coh by Constants.phi raised to the power 20.
why it matters
This placeholder bound supports the sterile exclusion modeling choice by placing any fourth neutrino above the phi^20 rung. It is referenced by the downstream lemma sterile_bound_placeholder, which proves the bound is positive. The construction aligns with the phi-ladder mass formula and the three-generation surjectivity assumption documented in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.