fisher_relation_2D
plain-language theorem explainer
The Fisher scaling relation holds for the 2D Ising critical exponents: the susceptibility exponent equals the correlation-length exponent times two minus the anomalous-dimension exponent. Condensed-matter physicists checking universality classes would cite it to verify internal consistency of the RS-derived values. The proof is a direct algebraic check obtained by unfolding the three constant definitions and normalizing the resulting arithmetic.
Claim. $γ_{2D} = ν_{2D} (2 - η_{2D})$ where $γ_{2D}$, $ν_{2D}$, and $η_{2D}$ are the susceptibility, correlation-length, and anomalous-dimension exponents of the two-dimensional Ising universality class.
background
The module derives universal critical exponents from φ-scaling near phase transitions, where quantities such as susceptibility diverge as powers of the reduced temperature. The three upstream definitions supply the exact 2D Ising values: eta_2D_Ising := 1/4, gamma_2D_Ising := 7/4, and nu_2D_Ising := 1. These match the known analytic results for the 2D Ising class and are required to satisfy standard scaling identities such as the Fisher relation.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definitions of gamma_2D_Ising, nu_2D_Ising, and eta_2D_Ising, then applies norm_num to reduce the resulting rational-number equality to a trivial identity.
why it matters
The theorem supplies a consistency check that the φ-scaling exponents chosen for the 2D Ising class obey the Fisher relation, a necessary condition for any proposed set of critical exponents. It supports the module's claim that RS φ-scaling reproduces universal behavior and aligns with the paper proposition on universal critical exponents from golden-ratio scaling. No downstream results depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.