heisenberg_eta_in_band
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.