satisfies_scaling

formal source

  32  eta : ℝ
  33
  34/-- The four thermodynamic scaling relations constrain any universality class. -/
  35def satisfies_scaling (uc : UniversalityClass) (D : ℝ) : Prop :=
  36  let alpha := 2 - D * uc.nu
  37  let beta := uc.nu * (D - 2 + uc.eta) / 2
  38  let gamma := uc.nu * (2 - uc.eta)
  39  alpha + 2 * beta + gamma = 2
  40
  41theorem scaling_always_holds (uc : UniversalityClass) (D : ℝ) :
  42    satisfies_scaling uc D := by
  43  unfold satisfies_scaling; ring
  44
  45/-! ## Known Bootstrap Values (D = 3)
  46
  47These are the high-precision conformal bootstrap values for reference.
  48They serve as targets for the RS derivation.
  49-/
  50
  51def ising_bootstrap : UniversalityClass := ⟨1, 0.629971, 0.0362978⟩
  52def xy_bootstrap : UniversalityClass := ⟨2, 0.67169, 0.03810⟩
  53def heisenberg_bootstrap : UniversalityClass := ⟨3, 0.71164, 0.03784⟩
  54def spherical_exact : UniversalityClass := ⟨0, 1.0, 0.0⟩
  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 ν₀ = φ⁻¹. -/
  65def nu_0_ising : ℝ := 1 / phi