nu_0_ising

formal source

  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
  82  unfold eta_stable_band_lower eta_stable_band_upper xy_bootstrap
  83  constructor <;> norm_num
  84
  85theorem heisenberg_eta_in_band :
  86    eta_stable_band_lower < heisenberg_bootstrap.eta ∧
  87    heisenberg_bootstrap.eta < eta_stable_band_upper := by
  88  unfold eta_stable_band_lower eta_stable_band_upper heisenberg_bootstrap
  89  constructor <;> norm_num
  90
  91/-- The ν values increase monotonically with N. -/
  92theorem nu_monotone_ising_xy :
  93    ising_bootstrap.nu < xy_bootstrap.nu := by
  94  unfold ising_bootstrap xy_bootstrap; norm_num
  95