NeutrinoState
plain-language theorem explainer
NeutrinoState enumerates five neutrino configurations as three mass eigenstates on the phi-ladder plus normal and inverted hierarchy types. Cosmologists working in the Recognition Science framework cite this enumeration to fix the structural count at five, matching configDim D. The declaration is a direct inductive definition that automatically derives the required typeclass instances.
Claim. The inductive type consists of three constructors for neutrino mass eigenstates on the phi-ladder together with two constructors for the normal and inverted hierarchy orderings.
background
The module places three neutrino masses m1 < m2 < m3 on the phi-ladder so that the ratio of adjacent mass-squared splittings equals phi squared, then adjoins the two hierarchy scenarios. Their total of five states is identified with configDim D. The definition introduces no hypotheses and serves as the base enumeration for the module's certification structure.
proof idea
The declaration is the inductive type definition with five constructors, followed by a deriving clause that installs DecidableEq, Repr, BEq, and Fintype instances.
why it matters
NeutrinoState supplies the five-state enumeration required by NeutrinoHierarchyCert, which asserts cardinality five and split ratio phi plus one. It anchors the structural claim of the neutrino hierarchy from the phi-ladder, aligning with the Recognition Science mass formula and the forcing chain that yields D = 3. No open questions are closed by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.