nu_2D_Ising
plain-language theorem explainer
The definition assigns the value 1 to the correlation length exponent for the two-dimensional Ising model. Researchers studying phase transitions cite this constant when verifying scaling relations such as Fisher's identity or Josephson hyperscaling in two dimensions. It is introduced as a direct numerical assignment to match the exact Onsager solution.
Claim. The correlation length critical exponent for the two-dimensional Ising universality class equals 1.
background
The module derives critical exponents from φ-scaling near phase transitions. Quantities such as the correlation length diverge as |t|^{-ν} where t denotes the reduced temperature. For the 2D Ising class, Recognition Science fixes this exponent at 1 to enforce consistency with known exact results and the φ-ladder constraints described in the module documentation on universal exponents from golden ratio scaling.
proof idea
The declaration is a direct definition that sets the exponent to the real number 1. No lemmas or tactics are applied.
why it matters
It supplies the numerical value of the correlation length exponent used in the Fisher relation and Josephson hyperscaling theorems for the two-dimensional case. The module targets the paper proposition on universal critical exponents from golden ratio scaling. Within the Recognition framework it instantiates the two-dimensional case of the φ-scaling mechanism for critical phenomena, prior to the three-dimensional Ising exponents listed as siblings in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.