module module

`IndisputableMonolith.Physics.MixingGeometry`

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 (6)

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

IndisputableMonolith.Physics.CKMGeometry module_import
IndisputableMonolith.Physics.Hierarchy module_import
IndisputableMonolith.Physics.MixingDerivation module_import
IndisputableMonolith.Physics.ParticleSummary module_import
IndisputableMonolith.Physics.PMNSCorrections module_import
IndisputableMonolith.Physics.QuarkMasses module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.Alpha module_import
IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (17)

def vertex_edge_slots L20
theorem vertex_edge_slots_eq_24 L22
def edge_dual_ratio L29
def fine_structure_leakage L34
def torsion_overlap L39
def solar_weight L42
def solar_radiative_correction L46
theorem solar_angle_forced L51
def atmospheric_weight L57
def atmospheric_radiative_correction L61
theorem atmospheric_angle_forced L66
def reactor_weight L72
def step_top_bottom L77
def step_bottom_charm L80
def step_charm_strange L83
def cabibbo_radiative_correction L87
theorem cabibbo_scaling_forced L92