ising_bootstrap

formal source

  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
  66
  67/-- The η values across O(N) are remarkably stable (~0.036-0.038).
  68    RS interpretation: η is determined primarily by the Q₃ cube geometry,
  69    which is independent of the spin symmetry group. -/
  70def eta_stable_band_lower : ℝ := 0.035
  71def eta_stable_band_upper : ℝ := 0.039
  72
  73theorem ising_eta_in_band :
  74    eta_stable_band_lower < ising_bootstrap.eta ∧
  75    ising_bootstrap.eta < eta_stable_band_upper := by
  76  unfold eta_stable_band_lower eta_stable_band_upper ising_bootstrap
  77  constructor <;> norm_num
  78
  79theorem xy_eta_in_band :
  80    eta_stable_band_lower < xy_bootstrap.eta ∧
  81    xy_bootstrap.eta < eta_stable_band_upper := by