pmnsCert
plain-language theorem explainer
pmnsCert assembles a certificate confirming that the five PMNS neutrino mixing parameters align with Recognition Science predictions from the phi ladder. Neutrino model builders would cite it to verify the solar angle band around arctan(1/phi) and maximal atmospheric mixing. The definition is a direct record construction pulling in the pre-proved parameter count, tangent identity, and interval bounds.
Claim. The PMNS certificate is the structure satisfying $ # (PMNSParameter) = 5 $, $ tan(pi/4) = 1 $, and $ 0.617 < solarTangent < 0.623 $.
background
The module derives PMNS neutrino mixing angles from Recognition Science by associating the atmospheric angle with the J-cost minimum at maximal mixing and the solar angle with the golden ratio. PMNSCert is the structure that packages three facts: the parameter count equals five, the atmospheric mixing satisfies tan(pi/4) equals one, and the solar tangent lies in the open interval (0.617, 0.623) matching 1/phi. Upstream, maximal_mixing establishes the tangent equality by simplification, pmnsParameterCount decides the cardinality, and solarTangent_band proves the interval using the bounds on phi.
proof idea
pmnsCert is defined by constructing the PMNSCert record with five_params assigned to pmnsParameterCount, maximal_mix to maximal_mixing, and solar_tangent_band to solarTangent_band. It is a pure structure literal that references the three sibling results without further computation.
why it matters
This definition supplies the explicit certificate for the PMNS sector in the Recognition Science framework, realizing the five-parameter count and the angle relations tied to phi and maximal mixing. It completes the local claims in the PMNSMixingAnglesFromRS module and supports extensions that incorporate these neutrino properties into the broader forcing chain. The construction embodies T5 J-uniqueness through the maximal mixing condition and the phi fixed point for the solar angle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.