xy_eta_in_band
plain-language theorem explainer
The XY universality class eta exponent satisfies the strict inequality between the lower and upper bounds of the stable eta band. Researchers modeling O(2) critical phenomena in three dimensions would cite this to confirm consistency with Q3 geometry predictions. The proof unfolds the three constant definitions and applies constructor with norm_num to verify the numerical bounds.
Claim. $0.035 < 0.03810 < 0.039$, where 0.03810 is the eta critical exponent of the XY universality class and the bounds 0.035 and 0.039 define the stable band for O(N) classes.
background
The module maps O(N) universality classes to subgroups of Aut(Q3) and supplies bootstrap reference values for D=3, including O(2) XY with eta equal to 0.03810. The stable band lower bound is defined as 0.035 with the accompanying note that eta values across O(N) remain remarkably stable near 0.036-0.038 because eta is fixed primarily by Q3 cube geometry independent of the spin symmetry group. The upper bound is 0.039. The xy_bootstrap definition packages the XY class as the triple with N=2, nu=0.67169 and eta=0.03810.
proof idea
The term proof unfolds eta_stable_band_lower, eta_stable_band_upper and xy_bootstrap, then splits the conjunction via constructor and discharges both inequalities by norm_num on the resulting numerical literals.
why it matters
The result confirms that the XY eta value sits inside the band whose stability is attributed to Q3 geometry, reinforcing the module's claim that eta is largely insensitive to the choice of O(N) subgroup. It forms part of the consistency checks alongside the Ising and Heisenberg cases listed in the same module. No downstream theorems are recorded, leaving open whether the band bounds themselves will be derived from the Recognition functional equation or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.