module module

`IndisputableMonolith.Physics.ParticlePhysicsGenerationsFromRS`

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

declarations in this module (12)

def generationCount L20
def fermionsPerGeneration L21
def totalFermions L22
theorem generations_eq_D L24
theorem fermions_per_gen_eq_4 L25
theorem total_fermions_eq_12 L26
def cubeEdges L29
theorem total_fermions_eq_cube_edges L30
inductive FermionGeneration L32
theorem generationTypeCount L36
structure GenerationCert L38
def generationCert L44