inductive definition def or abbrev

`Quark`

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

formal statement (Lean)

  31inductive Quark where
  32  | up | down | strange | charm | bottom | top
  33  deriving DecidableEq, Repr, BEq, Fintype
  34

used by (33)

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

CubeFaceUniversalityCert in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
fermion_antifermion_total in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
quark_has_6 in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
quark_lepton_sum in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
lepton_baseline_matches_anchor in IndisputableMonolith.Masses.BaselineDerivation decl_use
lepton_rungs in IndisputableMonolith.Masses.BaselineDerivation decl_use
downquark_sector_params in IndisputableMonolith.Masses.QuarkVerification decl_use
compute_rung in IndisputableMonolith.Masses.RungConstructor.Motif decl_use
down_generation_ordering in IndisputableMonolith.Masses.SectorDependentTorsion decl_use
lepton_total_span in IndisputableMonolith.Masses.SectorDependentTorsion decl_use
tauon_rung_minus_electron_rung in IndisputableMonolith.Masses.SMVerification decl_use
phi_ladder_verified in IndisputableMonolith.Masses.Verification decl_use
acceptable_leptons in IndisputableMonolith.PDG.Fits decl_use
lepton_hierarchy in IndisputableMonolith.Physics.Hierarchy decl_use
no_fourth_generation in IndisputableMonolith.Physics.MassHierarchy decl_use
reactor_weight in IndisputableMonolith.Physics.MixingGeometry decl_use
SMDerivation in IndisputableMonolith.Physics.ParticleSummary decl_use
pionDecayConstant_MeV in IndisputableMonolith.Physics.PionMasses decl_use
H_charm_mass_match in IndisputableMonolith.Physics.QuarkMasses decl_use
residues_match_steps in IndisputableMonolith.Physics.QuarkMasses decl_use
res_up in IndisputableMonolith.Physics.QuarkMasses decl_use
lepton_gauge in IndisputableMonolith.Physics.SectorYardsticks decl_use
up_quark_gauge in IndisputableMonolith.Physics.SectorYardsticks decl_use
leptonDoublet in IndisputableMonolith.Physics.WeakForceEmergence decl_use
experimentalStatus in IndisputableMonolith.QFT.Confinement decl_use
HadronMass in IndisputableMonolith.QFT.Confinement decl_use
mass_without_mass in IndisputableMonolith.QFT.Confinement decl_use
bottom_mass_match in IndisputableMonolith.RRF.Physics.QuarkMasses decl_use
predicted_mass in IndisputableMonolith.RRF.Physics.QuarkMasses decl_use
cert_tau in IndisputableMonolith.RSBridge.ResidueData decl_use

… and 3 more