PMNSElement
plain-language theorem explainer
PMNSElement packages the data for each entry in the neutrino PMNS mixing matrix as a triple of flavor index, mass eigenstate index, and complex amplitude. Neutrino phenomenologists and model builders extending the Standard Model would cite it when linking lepton mixing to the 8-tick by 3D generation mechanism. The declaration is a bare structure definition that introduces the record type with no proof obligations or computational reduction.
Claim. A PMNS element is a record consisting of a flavor index $i$ in the finite set of three neutrino flavors, a mass-eigenstate index $j$ in the finite set of three mass states, and a complex amplitude $U_{ij} in the complex numbers.
background
The module SM-011 derives the existence of exactly three fermion generations from the 8-tick cycle in three spatial dimensions. The tick is the fundamental RS time quantum, with one octave defined as eight ticks. The imported Lepton inductive type enumerates the six lepton states (electron, muon, tau and their neutrinos). This structure supplies the concrete data type needed to represent the Pontecorvo-Maki-Nakagawa-Sakata matrix that mixes neutrino flavor states with mass eigenstates, the leptonic counterpart of the CKM matrix.
proof idea
The declaration is a direct structure definition. It introduces the three fields fromFlavor, toMass and amplitude with no tactics, no lemmas applied, and no proof body.
why it matters
The definition supplies the record type required to encode PMNS matrix elements inside the larger argument that both charged-lepton and neutrino generations equal three because they arise from the same 8-tick by 3D phase structure. It supports the module's target of a PRL paper deriving the generation number from Recognition Science. The construction remains open on whether the resulting amplitudes reproduce the measured mixing angles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.