inductive definition def or abbrev

`Sector`

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

formal statement (Lean)

  20inductive Sector | Lepton | Neutrino | UpQuark | DownQuark | Electroweak
  21  deriving DecidableEq, Repr
  22
  23/-- Sector mapping for the rung constructor. -/

used by (40)

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

totalCost_nonneg in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton decl_use
SpectralSector in IndisputableMonolith.Foundation.SpectralEmergence decl_use
B_pow in IndisputableMonolith.Masses.Anchor decl_use
E_coh in IndisputableMonolith.Masses.Anchor decl_use
r0 in IndisputableMonolith.Masses.Anchor decl_use
r0_Electroweak_eq in IndisputableMonolith.Masses.Anchor decl_use
Sector in IndisputableMonolith.Masses.Anchor decl_use
yardstick in IndisputableMonolith.Masses.Anchor decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
B_pow_alt in IndisputableMonolith.Masses.AnchorDerivation decl_use
B_pow_eq_alt in IndisputableMonolith.Masses.AnchorDerivation decl_use
r0_alt in IndisputableMonolith.Masses.AnchorDerivation decl_use
r0_eq_alt in IndisputableMonolith.Masses.AnchorDerivation decl_use
cross_sector_shift in IndisputableMonolith.Masses.AnchorPolicy decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
predict_mass in IndisputableMonolith.Masses.AnchorPolicy decl_use
predict_mass_sdgt in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung_sdgt in IndisputableMonolith.Masses.AnchorPolicy decl_use
cos2_theta_W_bounds in IndisputableMonolith.Masses.BosonVerification decl_use
cos2_theta_positive in IndisputableMonolith.Masses.ElectroweakMasses decl_use
mass_rung_scaling in IndisputableMonolith.Masses.MassLaw decl_use
predict_mass in IndisputableMonolith.Masses.MassLaw decl_use
predict_mass_pos in IndisputableMonolith.Masses.MassLaw decl_use
QuarkAbsoluteMassResidual in IndisputableMonolith.Masses.QuarkScoreCard decl_use
down_generation_spacing in IndisputableMonolith.Masses.QuarkVerification decl_use
quark_mass_positive in IndisputableMonolith.Masses.QuarkVerification decl_use
r_down_values in IndisputableMonolith.Masses.QuarkVerification decl_use
Sector in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
sectorOf in IndisputableMonolith.Masses.RSBridge.Anchor decl_use

… and 10 more

depends on (11)

Lean names referenced from this declaration's body.

rung in IndisputableMonolith.Compat.Constants decl_use
Lepton in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Sector in IndisputableMonolith.Masses.Anchor decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Sector in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Lepton in IndisputableMonolith.Physics.AnomalousMoments decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use
Sector in IndisputableMonolith.RSBridge.Anchor decl_use