pith. machine review for the scientific record. sign in
theorem proved term proof high

heisenberg_eta_in_band

show as:
view Lean formalization →

The O(3) Heisenberg universality class satisfies the geometric stability constraint on its critical exponent eta. Physicists studying phase transitions in three-dimensional magnets would cite this result to align bootstrap calculations with the Recognition Science prediction of a narrow eta band independent of symmetry group. The verification proceeds by direct numerical comparison after expanding the constant definitions.

claim$0.035 < 0.03784 < 0.039$, where 0.03784 is the critical exponent eta for the O(3) Heisenberg model.

background

The module maps O(N) symmetry groups to critical exponents through the automorphism structure of the Q3 cube in three dimensions. Bootstrap reference values are supplied for the Ising, XY, Heisenberg, and spherical models, with the Heisenberg eta fixed at 0.03784. The stable band for eta is introduced as the interval from 0.035 to 0.039, reflecting the geometric determination of this exponent independent of the specific symmetry rank N.

proof idea

The proof unfolds the definitions of eta_stable_band_lower, eta_stable_band_upper, and heisenberg_bootstrap, then splits the conjunction via constructor and resolves both numerical inequalities with norm_num.

why it matters in Recognition Science

This theorem verifies that the Heisenberg bootstrap value lies inside the eta stability band derived from Q3 geometry, consistent with the module's claim that eta is largely independent of N. It forms part of a family of similar statements for Ising and XY classes, supporting the broader assertion that all O(N) models in three dimensions respect the geometric constraint. The result aligns with the Recognition Science emphasis on D=3.

scope and limits

formal statement (Lean)

  85theorem heisenberg_eta_in_band :
  86    eta_stable_band_lower < heisenberg_bootstrap.eta ∧
  87    heisenberg_bootstrap.eta < eta_stable_band_upper := by

proof body

Term-mode proof.

  88  unfold eta_stable_band_lower eta_stable_band_upper heisenberg_bootstrap
  89  constructor <;> norm_num
  90
  91/-- The ν values increase monotonically with N. -/

depends on (5)

Lean names referenced from this declaration's body.