universalityClassCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute the critical exponents nu and eta for each class.
- Does not derive the J-cost band bounds from the functional equation.
- Does not address universality classes outside the five enumerated cases.
- Does not prove scaling relations or hyperscaling.
Lean usage
theorem use : Fintype.card UniversalityClass = 5 := universalityClassCountformal statement (Lean)
25theorem universalityClassCount : Fintype.card UniversalityClass = 5 := by decide
proof body
26