pmnsScoreCardCert_holds
plain-language theorem explainer
The theorem establishes existence of a PMNS scorecard certificate by bundling verified matches for the three mixing angles, Jarlskog invariant, its sign, and the CP phase band against PDG centers. Neutrino physicists comparing Recognition Science predictions to NuFIT data would cite this when checking the packaged error bounds. The proof is a direct term construction that assembles the six upstream row theorems into the required structure.
Claim. There exists a certificate structure $C$ satisfying $|sin^2θ_{12}^{pred}-0.307|<0.01$, $|sin^2θ_{13}^{pred}-0.022|<0.002$, $|sin^2θ_{23}^{pred}-0.546|<0.01$, $|J^{pred}-3.08×10^{-5}|<0.6×10^{-5}$, $J^{pred}>0$, and $π<δ_{CP}^{pred}<2π$.
background
The PMNSScoreCardCert structure collects absolute-error bounds on the predicted sine-squared mixing angles, the Jarlskog invariant, its positivity, and the CP-violating phase lying in the open interval (π, 2π). These predictions originate from the MixingDerivation and PMNSMatrix modules, while the observed centers (0.307, 0.022, 0.546, 3.08e-5) are taken from PDG and NuFIT compilations. The upstream row theorems establish each bound individually: row_pmns_theta12 proves the θ12 match, row_jarlskog proves the Jarlskog match, and row_deltaCP_pmns_in_open_band places the phase in the required band, with the CKM jarlskog definition supplying the invariant construction reused here.
proof idea
The proof is a term-mode construction that directly instantiates the PMNSScoreCardCert structure. It supplies the field theta12 with the theorem row_pmns_theta12, theta13 with row_pmns_theta13, theta23 with row_pmns_theta23, jarlskog with row_jarlskog, j_pos with row_jarlskog_pos, and deltaCP_band with row_deltaCP_pmns_in_open_band. No additional tactics or reductions are required beyond this assembly of the pre-proved row results.
why it matters
This theorem completes the PMNS scorecard by demonstrating that all component matches can be simultaneously satisfied, thereby certifying the Recognition Science predictions for neutrino mixing against experimental data. It builds on the individual row theorems and the Jarlskog definition from the CKM module, feeding into the broader Phase 2 particle spectrum claims. Within the framework, it addresses the PMNS sector of the eight-tick octave and mixing derivations, leaving scheme dependence of sin²θ_W as a noted residual. The module documentation identifies this as a partial theorem whose falsifier is a sufficiently large shift in NuFIT centers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.