PMNSCert
plain-language theorem explainer
PMNSCert packages three RS-derived facts on the PMNS neutrino mixing matrix: exactly five parameters, maximal atmospheric mixing with tan(π/4)=1, and the solar tangent inside (0.617,0.623). Neutrino phenomenologists cite it to anchor the golden-ratio prediction for θ₁₂ against oscillation data. The structure is assembled directly from the five-element inductive enumeration of PMNSParameter and the definition of solarTangent as phi inverse.
Claim. Let PMNSParameter be the five-element set consisting of the three mixing angles θ₁₂, θ₂₃, θ₁₃ together with the Dirac CP phase and the two Majorana phases. Then PMNSCert is the structure asserting that this set has cardinality 5, that tan(π/4)=1, and that 0.617 < φ⁻¹ < 0.623, where φ denotes the golden ratio.
background
PMNSParameter is the inductive type with constructors theta12, theta23, theta13, deltaCP, majoranaPhases; its Fintype instance immediately yields cardinality 5. solarTangent is the noncomputable definition phi⁻¹, which the module identifies with the solar mixing tangent. The module sets the local context by noting that maximal mixing θ₂₃=45° corresponds to J=0 (symmetric mixing) while θ₁₂ ≈ arctan(φ⁻¹), and that the five parameters equal configDim D=5.
proof idea
The structure is introduced by enumerating its three fields directly: the cardinality fact is supplied by the Fintype instance on PMNSParameter, the maximal-mixing equality is the standard trigonometric identity tan(π/4)=1, and the solar-tangent band is the explicit interval check on the definition solarTangent := phi⁻¹.
why it matters
PMNSCert supplies the certified facts assembled into the downstream definition pmnsCert. It fills the module claim that the PMNS parameter count equals configDim D=5 and that the solar tangent lies inside the golden-ratio band (0.617,0.623). The construction connects to the Recognition Science forcing chain through the explicit appearance of phi and the J-minimum condition for maximal mixing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.