theorem
proved
universalityClassCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.CriticalPhenomenaFromJCost on GitHub at line 25.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
22 | Ising | Heisenberg | XY | meanField | percolation
23 deriving DecidableEq, Repr, BEq, Fintype
24
25theorem universalityClassCount : Fintype.card UniversalityClass = 5 := by decide
26
27structure CriticalPhenomenaCert where
28 five_classes : Fintype.card UniversalityClass = 5
29 critical_threshold : CanonicalCert
30
31noncomputable def criticalPhenomenaCert : CriticalPhenomenaCert where
32 five_classes := universalityClassCount
33 critical_threshold := cert
34
35end IndisputableMonolith.Physics.CriticalPhenomenaFromJCost