eta_stable_band_lower
plain-language theorem explainer
The lower edge of the η-stable band is supplied as the real constant 0.035. A physicist comparing bootstrap critical exponents for O(N) models to the Q3 geometry prediction would cite this value when verifying that Ising, XY, and Heisenberg η lie inside the narrow window. The definition is a direct numeric assignment with no computation or lemmas.
Claim. The lower bound of the stable band for the critical exponent η is defined as 0.035.
background
The module maps O(N) universality classes to subgroups of the automorphism group of the Q3 cube. It supplies leading-order critical exponents in D=3 via this geometric structure, with reference bootstrap values η ≈ 0.03630 for Ising (O(1)), 0.03810 for XY (O(2)), and 0.03784 for Heisenberg (O(3)). The supplied doc-comment states that η values across O(N) remain stable near 0.036-0.038 because η is fixed primarily by Q3 cube geometry and is independent of the spin symmetry group.
proof idea
The declaration is a direct numeric definition that assigns the real number 0.035. No lemmas or tactics are applied; the value is used verbatim in the three downstream band-membership theorems.
why it matters
This constant supplies the lower edge required by the three in-band theorems (ising_eta_in_band, xy_eta_in_band, heisenberg_eta_in_band). Those theorems unfold the definition together with the bootstrap η values to confirm membership in the stable interval. The placement supports the module claim that η is determined by Q3 geometry rather than the specific O(N) symmetry group.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.