module module high

`IndisputableMonolith.Physics.UniversalityClasses`

This module defines universality classes in Recognition Science as objects labeled by O(N) symmetry rank together with their critical exponents. Condensed-matter physicists mapping RS to phase-transition data would cite these definitions when classifying models. The module supplies the core type and a handful of scaling lemmas; it contains no deep proofs.

claimA universality class is an object labeled by an integer $N$ (the rank of the O(N) symmetry) together with the associated critical exponents.

background

The module imports the RS time quantum τ₀ = 1 tick and the Q₃ cube spectral formalism. The latter records that the graph Laplacian of the 3-dimensional hypercube has eigenvalues {0, 2, 2, 2, 4, 4, 4, 6} and supplies the combinatorial substrate for critical-exponent corrections in three dimensions. UniversalityClass is introduced exactly as stated in the module doc-comment: each class is characterized by its O(N) symmetry rank and the corresponding critical exponents.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the classification layer that later results on Ising, XY and Heisenberg models instantiate. It therefore sits between the D = 3 forcing step (T8) and the concrete exponent calculations that use the cube-spectrum corrections.

scope and limits

Does not derive numerical values of any critical exponent.
Does not treat symmetries outside the O(N) family.
Does not address dynamical or non-equilibrium universality classes.
Does not contain the explicit mass or coupling formulas of the phi-ladder.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Physics.CubeSpectrum module_import

declarations in this module (16)

structure UniversalityClass L29
def satisfies_scaling L35
theorem scaling_always_holds L41
def ising_bootstrap L51
def xy_bootstrap L52
def heisenberg_bootstrap L53
def spherical_exact L54
def nu_0_ising L65
def eta_stable_band_lower L70
def eta_stable_band_upper L71
theorem ising_eta_in_band L73
theorem xy_eta_in_band L79
theorem heisenberg_eta_in_band L85
theorem nu_monotone_ising_xy L92
theorem nu_monotone_xy_heisenberg L96
theorem nu_monotone_heisenberg_spherical L100