pith. sign in
module module high

IndisputableMonolith.Physics.PMNSScoreCard

show as:
view Lean formalization →

The PMNSScoreCard module assembles a scorecard for the PMNS neutrino mixing parameters derived from the Recognition Science framework. It defines rows for the angles theta12, theta13, theta23, the Jarlskog invariant, and a certificate confirming agreement with experimental bands. The module draws directly on the geometric mixing derivation and the phi-angle PMNS construction without adding new proofs.

claimThe scorecard certifies that the RS-derived PMNS mixing angles satisfy the experimental ranges: $33.0^circ < theta_{12} < 34.0^circ$, $8.0^circ < theta_{13} < 9.0^circ$, $40^circ < theta_{23} < 52^circ$, together with the Jarlskog invariant $J$ and delta_CP lying in the open band.

background

This module sits inside Phase 7.2 of the Recognition Science program. The upstream MixingDerivation module formalizes the geometric derivation of the mixing matrix elements from the cubic ledger structure, replacing numerical matches with topological proofs. The PMNSMatrix module derives the Pontecorvo-Maki-Nakagawa-Sakata neutrino mixing matrix from RS, with nu_e, nu_mu, nu_tau as flavor eigenstates whose mixing is fixed by phi-angles.

proof idea

This is a definition module, no proofs. It structures the scorecard by defining individual parameter rows and then assembling them into the single certificate PMNSScoreCardCert whose holding theorem simply invokes the upstream derivations.

why it matters in Recognition Science

The module supplies the terminal scorecard for the PMNS sector, confirming that the phi-angle predictions match experiment. It completes the mixing-matrix chain begun in the cubic-ledger derivation and the SM-014 PMNS construction, providing a compact validation object for the full set of neutrino parameters.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)