universalityClassCount
plain-language theorem explainer
The declaration asserts that the Recognition Science model admits exactly five universality classes for critical phenomena. Condensed matter physicists classifying phase transitions via the J-cost function would cite this enumeration. The proof is a one-line decision procedure that exhausts the finite inductive type.
Claim. The set of universality classes has cardinality five, where the classes are Ising, Heisenberg, XY, mean-field, and percolation.
background
In the Critical Phenomena from J-Cost module, phase transitions occur when the order parameter ratio r crosses J(φ) at the critical point, with J(r_critical) in the canonical band (0.11, 0.13). The framework sets configDim D = 5 for these phenomena. The inductive type UniversalityClass enumerates the five classes and derives Fintype. An upstream structure defines a universality class by symmetry rank N together with exponents nu and eta, subject to the four thermodynamic scaling relations.
proof idea
The proof is a one-line wrapper that applies the decide tactic to Fintype.card on the inductive type UniversalityClass, which already derives DecidableEq, Repr, BEq, and Fintype.
why it matters
This supplies the five_classes field to criticalPhenomenaCert, confirming the enumeration required for the J-cost model of critical phenomena. It realizes the Recognition Science claim of five canonical classes at configDim D = 5, separate from spatial D = 3. The result closes the finite list needed to anchor the canonical J-band threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.