spherical_exact
plain-language theorem explainer
The spherical_exact definition supplies the O(infinity) universality class with nu set to 1 and eta set to 0. Researchers working on large-N expansions or mean-field limits in critical phenomena cite these exact values. It is introduced as a direct structure constructor matching the known spherical-model result in three dimensions.
Claim. The spherical universality class is characterized by symmetry rank $N=0$, critical exponent $nu=1$, and $eta=0$.
background
A UniversalityClass is the structure recording symmetry rank N together with the two critical exponents nu and eta. The module maps O(N) classes to subgroups of Aut(Q3) and lists reference values for D=3, with the spherical model (infinite-N limit) assigned nu=1.0 and eta=0.0. Upstream structures such as PhiForcingDerived calibrate the J-cost that underlies the phi-ladder RG steps used to assign these exponents.
proof idea
The definition is a one-line constructor that directly assembles the UniversalityClass record with the triple (0, 1.0, 0.0). No lemmas or tactics are applied; the values are taken verbatim from the spherical-model solution stated in the module documentation.
why it matters
This definition supplies the upper endpoint for the monotonicity result nu_monotone_heisenberg_spherical, which proves the Heisenberg nu is strictly less than the spherical value. It completes the set of reference classes (Ising, XY, Heisenberg, spherical) listed for D=3 and sits inside the Recognition Science mapping of symmetry rank to phi-ladder RG steps. The construction anchors the large-N end of the bootstrap sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.