module module high

`IndisputableMonolith.StandardModel.PMNSMatrix`

The PMNSMatrix module supplies observed PDG values and Recognition Science predictions for the three neutrino mixing angles together with the CP phase. Neutrino phenomenologists comparing RS outputs to oscillation data would cite these constants when scoring the PMNS matrix. The module consists entirely of numerical definitions and no deductive proofs.

claimThe solar mixing angle satisfies $θ_{12}≈33.44°$ with $sin²θ_{12}≈0.307$; analogous observed values are supplied for $θ_{23}$, $θ_{13}$ and $δ_{CP}$, together with RS predictions $φ$-prediction for each angle and the best-fit PMNS parameter tuple.

background

Recognition Science obtains all particle properties from the J-cost functional and the phi-ladder fixed point. The PMNSMatrix module resides in the StandardModel domain and imports only the base time quantum $τ_0=1$ tick from Constants. It introduces the PMNSParameters record, the bestFitPMNS tuple, and the explicit phi-based predictions phi_prediction_theta12, maximal_theta23 and phi_prediction_theta13 that reuse the self-similar geometry already fixed by the upstream forcing chain.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module is imported by PMNSScoreCard to assemble the Phase-2 PMNS mixing scorecard. It supplies the predicted sin²θ* values and the deltaCP_pmns_torsion_correction that are compared against PDG targets via the Jarlskog construction already packaged in the downstream scorecard.

scope and limits

Does not derive the numerical angle values from the T5–T8 forcing chain.
Does not construct the explicit 3×3 PMNS matrix elements.
Does not include renormalization-group running or sterile-neutrino extensions.

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