eta_2D_Ising
plain-language theorem explainer
The 2D Ising critical exponent eta is assigned the exact value 1/4. Phase transition researchers cite this constant to close scaling relations such as the Fisher identity in two dimensions. The declaration is a direct numerical definition with no computation or lemmas applied.
Claim. The critical exponent $η$ for the two-dimensional Ising universality class equals $1/4$.
background
Critical exponents quantify power-law divergences in thermodynamic quantities near phase transitions, including the pair correlation function decaying as $r^{-(d-2+η)}$ at criticality. In Recognition Science, these exponents follow from φ-scaling of J-cost fluctuations, which enforce universality depending only on dimension and symmetry class. The module THERMO-005 implements this mechanism by supplying the exact 2D Ising values, with the present definition fixing η at 1/4 to match the Onsager solution.
proof idea
This is a direct definition that assigns the constant 1/4. No lemmas are applied and no tactics are used; the value is supplied explicitly as the known exact result for the two-dimensional Ising model.
why it matters
The definition supplies the η value required by the downstream Fisher relation theorem, which states gamma_2D_Ising = nu_2D_Ising * (2 - eta_2D_Ising). It contributes to the module's target of deriving universal critical exponents from φ-scaling, as described in the paper proposition on golden-ratio constraints. In the broader framework it aligns with T6 self-similar fixed-point forcing and the eight-tick octave that fixes low-dimensional exponents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.