eta_stable_band_upper

formal source

  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
  96theorem nu_monotone_xy_heisenberg :
  97    xy_bootstrap.nu < heisenberg_bootstrap.nu := by
  98  unfold xy_bootstrap heisenberg_bootstrap; norm_num
  99
 100theorem nu_monotone_heisenberg_spherical :
 101    heisenberg_bootstrap.nu < spherical_exact.nu := by