NeutrinoHierarchyCert
plain-language theorem explainer
NeutrinoHierarchyCert bundles three assertions into a single structure: the neutrino sector contains exactly five states, the adjacent mass-squared splitting ratio equals phi squared, and that ratio is positive. Cosmologists working inside the Recognition Science phi-ladder model cite the certificate when confirming that the structural count matches the configuration dimension. The declaration is a bare structure with no proof obligations or computational body.
Claim. A certificate for the neutrino mass hierarchy consists of a finite enumeration of five states together with the conditions that the adjacent mass-squared splitting ratio equals $phi^2$ and that this ratio is strictly positive.
background
The module models three neutrino mass eigenstates on the phi-ladder with an adjacent mass-squared splitting ratio of phi squared, augmented by the two hierarchy scenarios (normal and inverted). Their inductive type NeutrinoState enumerates exactly these five cases. The noncomputable definition massSplitRatio sets the ratio to phi to the power two, which equals phi plus one by the defining equation of the golden ratio.
proof idea
The declaration is a structure definition whose three fields directly encode the required assertions; no lemmas are applied and no tactics are executed.
why it matters
The structure is instantiated by the downstream neutrinoHierarchyCert definition, supplying a concrete witness for the five-state count. It thereby certifies the structural match to configuration dimension D inside the Recognition Science framework, consistent with the eight-tick octave and the derivation of three spatial dimensions. No open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.