inductive
definition
QCDPhase
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.QuantumChromodynamicsFromRS on GitHub at line 33.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
30theorem color_times_gluon : colorCount * gluonCount = 24 := by decide
31theorem color_gluon_is_b3half : colorCount * gluonCount = 48 / 2 := by decide
32
33inductive QCDPhase where
34 | hadronic | quarkGluonPlasma | colorSuperconductor | nuclear | vacuum
35 deriving DecidableEq, Repr, BEq, Fintype
36
37theorem qcdPhaseCount : Fintype.card QCDPhase = 5 := by decide
38
39structure QCDCert where
40 color_3 : colorCount = 3
41 gluon_8 : gluonCount = 8
42 product_24 : colorCount * gluonCount = 24
43 five_phases : Fintype.card QCDPhase = 5
44
45def qcdCert : QCDCert where
46 color_3 := colorCount_eq_D
47 gluon_8 := gluonCount_eq_8
48 product_24 := color_times_gluon
49 five_phases := qcdPhaseCount
50
51end IndisputableMonolith.Physics.QuantumChromodynamicsFromRS