ising_eta_in_band
plain-language theorem explainer
The theorem confirms that the anomalous dimension η for the O(1) Ising universality class, taken from the bootstrap tuple, lies strictly inside the interval (0.035, 0.039). Workers on critical phenomena in three dimensions cite the result to verify that η remains stable across O(N) classes when fixed by Q₃ cube geometry. The proof reduces to unfolding the three constant definitions and discharging the two inequalities by direct numerical normalization.
Claim. $0.035 < η < 0.039$, where $η$ is the anomalous dimension component of the Ising universality class tuple with symmetry rank 1, correlation-length exponent approximately 0.62997, and the stable band bounds are the constants 0.035 and 0.039.
background
The module frames O(N) universality classes as subgroups of Aut(Q₃). The Ising class is the concrete tuple ⟨1, 0.629971, 0.0362978⟩. The stable band for η is introduced by the two constants 0.035 and 0.039; its doc-comment states that η values remain remarkably stable (~0.036-0.038) because they are fixed primarily by the Q₃ cube geometry rather than by the spin symmetry group N. The upstream satisfies_scaling relation enforces the thermodynamic identity α + 2β + γ = 2 for any class in D dimensions.
proof idea
The term proof unfolds eta_stable_band_lower, eta_stable_band_upper, and ising_bootstrap to expose the literals 0.035, 0.039, and 0.0362978. Constructor splits the conjunction into two goals; norm_num then verifies both strict inequalities by direct arithmetic.
why it matters
The declaration places the Ising η inside the geometry-derived band, reinforcing that η is insensitive to N once D = 3 is fixed by the eight-tick octave. It supplies a concrete numerical check for the bootstrap reference values listed in the module documentation. No downstream theorems are recorded, yet the result supports the larger claim that critical exponents descend from the Recognition Composition Law and the forcing chain steps T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.