module module

`IndisputableMonolith.StandardModel.PMNSMatrix`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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