PMNSParameters
plain-language theorem explainer
The PMNSParameters structure collects the four real numbers that parametrize the standard neutrino mixing matrix relating flavor to mass eigenstates. Neutrino phenomenologists fitting oscillation data or model builders deriving angles from symmetries would cite this record. It is introduced as a plain structure definition with no computation or proof obligations.
Claim. A record containing four real parameters: the solar mixing angle $θ_{12}$, atmospheric angle $θ_{23}$, reactor angle $θ_{13}$, and CP-violating phase $δ_{CP}$, which together specify the unitary matrix $U$ in the standard parametrization of neutrino flavor mixing.
background
The module derives the PMNS matrix from Recognition Science by treating neutrino mixing angles as φ-quantized quantities. Large observed angles, especially the near-maximal atmospheric angle, are linked to underlying symmetries in the eight-tick construction. The supplied doc-comment gives the explicit 3×3 form of $U$ in terms of cosines and sines of the three angles together with the complex phase factor $e^{iδ_{CP}}$.
proof idea
Structure definition that declares four fields of type ℝ, each carrying a comment that identifies its physical interpretation as one of the standard PMNS parameters.
why it matters
The record is instantiated by the downstream bestFitPMNS definition to store observed central values. It supplies the parameter container required by the module's target of deriving the PMNS matrix from φ-angles and golden-ratio geometry. The construction draws on the eight-tick phase (T7) and the complex phase map from the RiemannHypothesis wedge, advancing the claim that neutrino mixing follows from the same Recognition Science primitives that fix D=3 and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.