inductive
definition
UniversalityClass
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.CriticalPhenomenaFromJCost on GitHub at line 21.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
18namespace IndisputableMonolith.Physics.CriticalPhenomenaFromJCost
19open Common.CanonicalJBand
20
21inductive UniversalityClass where
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