module module

`IndisputableMonolith.StandardModel.CPPhaseDerivation`

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.StandardModel.JarlskogInvariant module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.CycleOperator module_import
IndisputableMonolith.Foundation.FaceWinding module_import
IndisputableMonolith.Foundation.GrayCodeChirality module_import
IndisputableMonolith.StandardModel.CKMFromCube module_import

declarations in this module (19)

def TransportPath L66
def canonicalPath L70
theorem canonical_path_closed L74
theorem canonical_returns L80
def phasePerFlip L97
def berryPhasePerCycle L100
theorem berry_gen1 L104
theorem berry_gen2 L110
theorem berry_gen3 L116
theorem berryPhase_generation_dependent L123
def cpPhaseRaw L139
theorem cp_phase_nonzero L145
theorem cp_phase_positive L152
theorem cp_phase_changes_sign_under_reversal L166
theorem cpt_phase_zero L174
theorem theta_qcd_cost_minimized_at_zero L194
theorem strong_cp_resolved_with_ckm_cp L207
structure CPPhaseCert L214
def cpPhaseCert L222