neutrinoHierarchyCert
plain-language theorem explainer
Neutrino masses sit on the φ-ladder with adjacent mass-squared splitting ratio φ². The certificate definition packages the five-state enumeration together with the ratio equality and positivity into NeutrinoHierarchyCert for cosmology derivations. Cosmologists modeling neutrino patterns in Recognition Science would cite it to confirm consistency with the phi-based mass formula. The construction is a direct record instantiation that pulls the state count from a decision procedure and the ratio facts from unfolding lemmas.
Claim. The neutrino hierarchy certificate asserts that the number of neutrino states is 5, the mass-squared splitting ratio equals $φ + 1$, and the ratio is positive.
background
In the Recognition Science cosmology module, three neutrino mass eigenstates are placed on the φ-ladder so that the ratio of adjacent mass-squared splittings equals φ². Adding the two hierarchy scenarios (normal and inverted) produces a total of five configurations, matching the module's configDim D. The NeutrinoHierarchyCert structure requires exactly these three properties: Fintype.card NeutrinoState = 5, massSplitRatio = φ + 1, and 0 < massSplitRatio.
proof idea
The definition constructs the NeutrinoHierarchyCert record by direct field assignment. The five_states field receives the result of neutrinoState_count, which decides the cardinality is 5. The split_ratio_phi_sq field receives massSplitRatio_eq, which unfolds massSplitRatio to the phi square identity. The split_ratio_pos field receives massSplitRatio_pos, which applies the positivity of powers to φ.
why it matters
This definition supplies the concrete certificate that closes the structural enumeration for neutrino hierarchies on the φ-ladder. It realizes the mass formula application in the cosmology module and confirms zero-sorry status for the hierarchy claim. The construction ties directly to the self-similar fixed point φ and the forcing chain that yields spatial dimension D = 3, while leaving the certificate available for later integration with absolute mass values or experimental bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.