PMNSParameter
plain-language theorem explainer
PMNSParameter enumerates the five neutrino mixing parameters of the PMNS matrix as an inductive type. Neutrino physicists in the Recognition Science setting cite it to establish that the mixing matrix carries exactly five degrees of freedom matching configDim D = 5. The definition lists five constructors and derives the standard decidable-equality and finite-type instances in one step.
Claim. Let the PMNS parameters be the finite set consisting of the solar angle $θ_{12}$, atmospheric angle $θ_{23}$, reactor angle $θ_{13}$, Dirac CP phase $δ_{CP}$, and Majorana phases.
background
The module treats neutrino mixing angles inside Recognition Science by linking observed PMNS values to the golden-ratio structure. It records $θ_{23} ≈ π/4$ as maximal mixing where the J-cost reaches its minimum, and $θ_{12} ≈ arctan(φ^{-1})$ with φ the self-similar fixed point. The five-parameter count is identified with configDim D = 5.
proof idea
Inductive definition that introduces five named constructors and derives DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters
The type supplies the cardinality statement proved in pmnsParameterCount and the five_params field of PMNSCert. It anchors the RS claim that neutrino mixing arises from the eight-tick octave and phi-ladder, with D = 5 internal degrees of freedom before angle values are recovered from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.