eta_stable_band_upper
plain-language theorem explainer
The definition supplies the constant upper bound 0.039 for the stable interval of the critical exponent η in three-dimensional O(N) models. Researchers verifying bootstrap or renormalization-group results for the Ising, XY, and Heisenberg universality classes would cite this bound to confirm that their computed η values lie inside the predicted window. It is introduced as a direct real-number assignment with no computation or lemmas required.
Claim. The upper endpoint of the stable band for the anomalous dimension η in three-dimensional O(N) models is the real number 0.039.
background
The module identifies O(N) universality classes with subgroups of the automorphism group of the three-dimensional cube Q₃ and supplies reference bootstrap values for the critical exponents at D = 3: Ising (O(1)) η ≈ 0.03630, XY (O(2)) η ≈ 0.03810, Heisenberg (O(3)) η ≈ 0.03784. The stable band is delimited by a pair of real constants that bracket these reference values. No upstream lemmas are required; the definition stands alone as a numeric constant.
proof idea
The declaration is a direct constant assignment of the real number 0.039. No lemmas are invoked and no tactics are executed; the body consists solely of the literal numeric value.
why it matters
The bound is invoked by the three theorems that place the bootstrap η values for the Ising, XY, and Heisenberg models strictly inside the stable band. It thereby supports the module's claim that the Q₃ automorphism structure reproduces the known three-dimensional universality classes. The construction is consistent with the Recognition Science result that spatial dimension D equals 3 arises from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.