module module

`IndisputableMonolith.StandardModel.CKMExact`

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.Foundation.UnifiedForcingChain module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.EightTick module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import
IndisputableMonolith.StandardModel.CKMMatrix module_import

declarations in this module (56)

inductive Q3Vertex L45
inductive Q3Edge L50
theorem q3_vertex_count L56
theorem q3_edge_count L57
def grayFlipAxis L62
def flipCount L72
theorem flip_axis0 L77
theorem flip_axis1 L78
theorem flip_axis2 L79
theorem total_flips L81
theorem gray_asymmetry L85
theorem gray_axis12_symmetric L88
def tau L93
def deltaTau12 L98
def deltaTau23 L99
theorem deltaTau12_eq L101
theorem deltaTau23_eq L102
theorem forty_four_connection L104
def A_structural L109
theorem A_structural_eq L111
theorem A_structural_pos L114
def faceFlux L125
theorem faceFlux_12 L129
theorem faceFlux_23 L133
theorem faceFlux_13 L137
def berryCorrection L144
theorem berry_correction_eq L148
theorem berry_correction_pos L151
theorem berry_sq_eq L154
def A_corrected L160
theorem A_corrected_exact L163
theorem A_corrected_pos L167
theorem A_corrected_tight L172
theorem A_in_pdg_1sigma L176
theorem A_distance_from_pdg L180
theorem gap_nearly_closed L185
def lambda_RS L191
theorem lambda_RS_pos L193
theorem lambda_RS_interval L195
def lambda_PDG L221
theorem lambda_PDG_in_window L223
theorem lambda_structural_discrepancy L228
theorem lambda_correction_target L246
def jarlskog_rs L252
theorem jarlskog_pos L254
theorem forty_four_governs_three_constants L262
theorem nine_from_color_squared L269
theorem eleven_is_torsion_gap L272
theorem A_from_color_and_torsion L275
theorem four_from_chirality L281
theorem eleven_from_torsion L284
theorem six_from_torsion L287
theorem three_halves_from_asymmetry L291
theorem nine_elevenths_forced L295
structure CKMExactCert L301
def ckmExactCert L316