pith. machine review for the scientific record. sign in
def definition def or abbrev

spherical_exact

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  54def spherical_exact : UniversalityClass := ⟨0, 1.0, 0.0⟩

proof body

Definition body.

  55
  56/-! ## RS Leading-Order Framework
  57
  58The RS conjecture: the leading-order ν₀(N) is determined by the Q₃
  59automorphism structure. The simplest parameterization uses a symmetry
  60factor g(N) such that ν₀(N) = φ⁻¹ · (1 + f(N)) where f captures the
  61effect of the O(N) symmetry on the φ-ladder RG step.
  62-/
  63
  64/-- Leading-order Ising ν₀ = φ⁻¹. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.