inductive definition def or abbrev

`UniversalityClass`

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

formal statement (Lean)

  21inductive UniversalityClass where
  22  | Ising | Heisenberg | XY | meanField | percolation
  23  deriving DecidableEq, Repr, BEq, Fintype
  24

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

CriticalPhenomenaCert in IndisputableMonolith.Physics.CriticalPhenomenaFromJCost decl_use
universalityClassCount in IndisputableMonolith.Physics.CriticalPhenomenaFromJCost decl_use
heisenberg_bootstrap in IndisputableMonolith.Physics.UniversalityClasses decl_use
ising_bootstrap in IndisputableMonolith.Physics.UniversalityClasses decl_use
satisfies_scaling in IndisputableMonolith.Physics.UniversalityClasses decl_use
scaling_always_holds in IndisputableMonolith.Physics.UniversalityClasses decl_use
spherical_exact in IndisputableMonolith.Physics.UniversalityClasses decl_use
UniversalityClass in IndisputableMonolith.Physics.UniversalityClasses decl_use
xy_bootstrap in IndisputableMonolith.Physics.UniversalityClasses decl_use

Lean names referenced from this declaration's body.

UniversalityClass in IndisputableMonolith.Physics.UniversalityClasses decl_use