module module

`IndisputableMonolith.Foundation.MassWeakBases`

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.CKMFromCube module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.CycleOperator module_import
IndisputableMonolith.Foundation.GaugeFromCube module_import
IndisputableMonolith.Foundation.GrayCodeChirality module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import
IndisputableMonolith.Masses.TorsionForcing module_import

declarations in this module (17)

inductive MassBasisAssignment L81
theorem edge_dressed_prefers_axis0 L90
def evenFlipGenerator L111
def evenFlipOnVertex L117
theorem evenFlip_involution L124
inductive WeakBasisAssignment L139
def weakComplementAxis L147
theorem weakComplement_is_identity L153
def massBasisAxis L168
def weakBasisAxis L174
theorem both_bases_label_axes L185
structure MixingAngleData L203
def mixingData L215
theorem cabibbo_largest_angle L238
theorem vub_smallest L243
theorem ckm_hierarchy_from_torsion_gaps L249
theorem ckm_parameter_count L256