pith. sign in
module module moderate

IndisputableMonolith.Physics.PMNSScoreCard

show as:
view Lean formalization →

The PMNSScoreCard module assembles a compact certification of RS-derived PMNS mixing parameters against experimental bands. Neutrino phenomenologists comparing geometric predictions to oscillation data would cite the row theorems and top-level certificate. The module structure is a collection of row definitions drawn from the imported mixing derivation and PMNS matrix construction, closed by a single conjunction theorem.

claimThe scorecard certifies the derived values: $\text{PMNSScoreCardCert} \equiv \text{row}_{\theta_{12}} \land \text{row}_{\theta_{13}} \land \text{row}_{\theta_{23}} \land \text{row}_{J} \land \text{row}_{J>0} \land \text{row}_{\delta_{\text{CP}} \in \text{band}}$.

background

The module imports the geometric derivation of mixing matrices from the cubic ledger structure (MixingDerivation) and the explicit PMNS construction from phi-angles (StandardModel.PMNSMatrix). These upstream modules supply the phi-ladder expressions for the three mixing angles and the Jarlskog invariant that the scorecard rows then compare to measured intervals.

No new foundational objects are introduced; the module simply packages the already-derived PMNS quantities into named row certificates plus a single top-level conjunction that all rows hold simultaneously.

proof idea

This is a definition and certification module. Each row is a direct comparison of the upstream phi-derived angle or Jarlskog value against its experimental band; the certificate theorem is the conjunction of those rows.

why it matters in Recognition Science

The module closes the PMNS sector of Phase 7.2 mixing-matrix derivation by supplying a single citable object that collects all parameter matches. It feeds any later global consistency check that combines CKM and PMNS results under the same Recognition Science ledger.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)