inductive definition def or abbrev

`Generation`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  21inductive Generation | first | second | third
  22deriving DecidableEq, Repr
  23

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

all_examples_cproj_two_statement in IndisputableMonolith.CPM.ConstantsAudit decl_use
gauge_order_product in IndisputableMonolith.Foundation.GaugeFromCube decl_use
three_generations_from_dimension in IndisputableMonolith.Foundation.ParticleGenerations decl_use
gauge_generators_eq_edges in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Generation in IndisputableMonolith.Foundation.SpectralEmergence decl_use
closure_populates_next in IndisputableMonolith.Foundation.StillnessGenerative decl_use
biologyCost in IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization decl_use
biologyCost_self in IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization decl_use
biologyCost_symm in IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization decl_use
biologyInterpret in IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization decl_use
biologyRealization in IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization decl_use
Generation in IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization decl_use
yardstick in IndisputableMonolith.Masses.Anchor decl_use
predict_mass in IndisputableMonolith.Masses.AnchorPolicy decl_use
color_offset_eq_quark_baseline in IndisputableMonolith.Masses.BaselineDerivation decl_use
r_tau in IndisputableMonolith.Masses.MassHierarchy decl_use
bottom_down_equal_Z in IndisputableMonolith.Masses.QuarkScoreCard decl_use
quark_mass_positive in IndisputableMonolith.Masses.QuarkVerification decl_use
genOfTorsion in IndisputableMonolith.Masses.Ribbons decl_use
ResidueCert in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
match_rsbridge_rung in IndisputableMonolith.Masses.RungConstructor.Proofs decl_use
N_diff_eq_edges_at_D3 in IndisputableMonolith.Masses.SectorDependentTorsion decl_use
all_fermion_masses_pos in IndisputableMonolith.Masses.SMVerification decl_use
tau_g in IndisputableMonolith.Physics.CKM decl_use
tauStepCoefficientDerived_matches_paper in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
bits_bijection in IndisputableMonolith.Physics.ThreeGenerations decl_use
dimensions_from_log in IndisputableMonolith.Physics.ThreeGenerations decl_use
dimensionToGeneration in IndisputableMonolith.Physics.ThreeGenerations decl_use
Generation in IndisputableMonolith.Physics.ThreeGenerations decl_use
neutrino_generations_match in IndisputableMonolith.Physics.ThreeGenerations decl_use

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.

Generation in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Generation in IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization decl_use
Generation in IndisputableMonolith.Physics.ThreeGenerations decl_use
Generation in IndisputableMonolith.RecogSpec.RSLedger decl_use