UniversalityClass
plain-language theorem explainer
The inductive definition enumerates the five canonical universality classes of critical phenomena as Ising, Heisenberg, XY, mean-field, and percolation. Condensed matter theorists would cite it when mapping J-cost thresholds at critical points to observed scaling exponents. It is realized as a direct inductive type whose Fintype, DecidableEq, and related instances are derived automatically.
Claim. Let the set of universality classes be the finite collection consisting of the Ising, Heisenberg, XY, mean-field, and percolation classes.
background
In the Critical Phenomena from J-Cost module, phase transitions are described by the order parameter ratio crossing the J-function at the critical point, with J(r_critical) required to lie inside the canonical band (0.11, 0.13). The upstream UniversalityClass structure from the UniversalityClasses module characterizes each class by its O(N) symmetry rank N together with the critical exponents nu and eta, subject to the four thermodynamic scaling relations. This inductive type supplies the concrete enumeration of the five standard classes, which the module identifies with configuration dimension D = 5.
proof idea
The declaration is a direct inductive enumeration of the five named constructors, with Lean automatically synthesizing the DecidableEq, Repr, BEq, and Fintype instances.
why it matters
The definition supplies the finite set whose cardinality is certified equal to 5 by universalityClassCount and is embedded in CriticalPhenomenaCert alongside the CanonicalCert for the critical threshold. It realizes the module statement that five canonical universality classes equal configDim D = 5, placing the J-cost model of condensed-matter transitions inside the Recognition Science framework whose constants derive from the phi-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.