module module high

`IndisputableMonolith.StandardModel.PMNSMatrix`

This module declares the three PMNS mixing angles, their observed values, and the phi-based predictions used inside the Recognition Science Standard Model. It is referenced by any work that scores lepton-sector mixing data against RS outputs. The module is a pure collection of numeric constants and derived expressions with no proof obligations.

claimThe solar mixing angle satisfies $θ_{12}≈33.44°$ ($sin²θ_{12}≈0.307$), together with definitions for $θ_{23}$, $θ_{13}$, $δ_{CP}$, the record PMNSParameters, the best-fit tuple bestFitPMNS, and the three phi predictions phi_prediction_theta12, maximal_theta23, phi_prediction_theta13.

background

The module imports the RS time quantum $τ_0=1$ tick from Constants. It introduces the record PMNSParameters and the best-fit values, then supplies both PDG-style observed angles and the phi-ladder predictions for each angle. The local theoretical setting is the lepton-mixing sector of the Standard Model inside Recognition Science, where the phi-ladder supplies the numerical targets that later feed the PMNS scorecard.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the predicted sin²θ values and deltaCP band that the downstream PMNSScoreCard uses to assemble the Phase 2 PMNS mixing scorecard. It thereby closes the RS prediction pipeline for neutrino mixing angles that originates in the forcing chain and the phi-ladder.

scope and limits

Does not derive any angle from the J-function or Recognition Composition Law.
Does not construct the explicit 3×3 unitary PMNS matrix.
Does not compute Jarlskog invariants or link to CKM geometry.
Does not address running or renormalization of the angles.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.PMNSScoreCard module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (33)

def theta12_degrees L44
def sin2_theta12_observed L45
def theta23_degrees L48
def sin2_theta23_observed L49
def theta13_degrees L52
def sin2_theta13_observed L53
def deltaCP_degrees L56
structure PMNSParameters L68
def bestFitPMNS L75
def phi_prediction_theta12 L89
def maximal_theta23 L97
def phi_prediction_theta13 L104
def TBM_theta12 L114
def TBM_theta23 L115
def TBM_theta13 L116
def GRM_theta12 L127
def TBM_correction_theta12 L139
theorem eight_tick_generation_connection L148
def deltam21_sq L163
def deltam31_sq L164
def mass_ratio L166
theorem mass_ratio_phi_connection L172
def predicted_deltaCP L193
theorem deltaCP_prediction_matches L195
structure MajoranaPhases L239
def predictions L252
theorem pmns_axes_symmetric L280
theorem deltaCP_pmns_leading_order_zero L286
def deltaCP_pmns_torsion_correction L292
theorem deltaCP_pmns_in_third_quadrant L296
theorem deltaCP_pmns_range L305
def experiments L321
structure PMNSFalsifier L334