module module

`IndisputableMonolith.Physics.ThreeGenerations`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (22)

abbrev TickIndex L50
def tickToBits L53
def bitsToTick L59
theorem bits_bijection L67
inductive Generation L77
theorem three_generations L84
def dimensionsFromTicks L90
theorem dimensions_from_log L93
def dimensionToGeneration L102
def massRatio L111
def massHierarchyPattern L120
theorem mass_from_phi_ladder L125
theorem why_exactly_three L134
theorem no_fourth_generation L141
structure CKMElement L148
theorem ckm_from_phase_overlap L158
def cabibboAngle L162
structure PMNSElement L168
theorem neutrino_generations_match L178
def experimentalTests L188
structure GenerationFalsifier L202
def experimentalStatus L209