pmnsParameterCount
plain-language theorem explainer
The PMNS neutrino mixing matrix is parameterized by exactly five quantities in the Recognition Science framework. Neutrino physicists aligning oscillation data with the phi-ladder structure would cite this count to match the configuration dimension. The equality follows from a direct decision procedure on the finite type whose five constructors enumerate the solar angle, atmospheric angle, reactor angle, CP phase, and Majorana phases.
Claim. The finite type of PMNS parameters has cardinality five, where the parameters are the solar mixing angle, atmospheric mixing angle, reactor mixing angle, Dirac CP phase, and Majorana phases.
background
The module records structural observations on the PMNS matrix: the solar angle satisfies tan theta12 approximately equal to the inverse golden ratio, the atmospheric angle is maximal at pi/4 corresponding to J minimum, and the reactor angle is small. The inductive type PMNSParameter enumerates these five quantities explicitly as theta12, theta23, theta13, deltaCP, and majoranaPhases, with an automatic Fintype instance derived from the constructors. The module documentation states that this enumeration equals the configuration dimension D equal to 5.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the cardinality statement. The tactic succeeds because the inductive definition supplies a decidable enumeration of exactly five elements and the Fintype instance is generated automatically by the deriving clause.
why it matters
The result supplies the five_params component of the pmnsCert definition that certifies the full RS-derived PMNS structure. It closes the parameter count for the mixing matrix in the S4-depth analysis, consistent with the framework's eight-tick octave and the identification of five parameters with configuration dimension. The downstream certificate also incorporates the maximal mixing and solar tangent band results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.