structure definition def or abbrev

`Hadron`

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

formal statement (Lean)

  23structure Hadron where
  24  q1 : RSBridge.Fermion
  25  q2 : RSBridge.Fermion
  26  binding : ℤ := 1

proof body

Definition body.

used by (6)

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

composite_rung in IndisputableMonolith.Physics.Hadrons decl_use
hadron_equal_z_degenerate in IndisputableMonolith.Physics.Hadrons decl_use
hadron_mass in IndisputableMonolith.Physics.Hadrons decl_use
gluon_confinement in IndisputableMonolith.QFT.Confinement decl_use
HadronMass in IndisputableMonolith.QFT.Confinement decl_use
mass_without_mass in IndisputableMonolith.QFT.Confinement decl_use

depends on (4)

Lean names referenced from this declaration's body.

Fermion in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Fermion in IndisputableMonolith.Masses.SMVerification decl_use
RSBridge in IndisputableMonolith.RecogSpec.RSBridge decl_use
Fermion in IndisputableMonolith.RSBridge.Anchor decl_use