D2
plain-language theorem explainer
The definition assigns the real number two to the spatial dimension D for the two-dimensional Ising model. Researchers verifying Onsager's exact critical exponents against scaling relations would cite this constant when parameterizing the model. It is introduced via direct assignment with no computation or lemmas required.
Claim. The spatial dimension in the two-dimensional Ising model is defined as $D = 2$.
background
The module examines the exactly solvable two-dimensional Ising model whose critical exponents are known exactly from Onsager's 1944 solution: ν = 1, η = 1/4, β = 1/8, γ = 7/4, α = 0, δ = 15. These values verify scaling relations including Rushbrooke, Fisher, Widom, and hyperscaling. The local setting tests whether the Recognition Science φ-algebraic formulas, which derive D = 3 as the unique physical dimension, extend to D = 2, where the leading-order ν₀ = φ^{-1} fails to match the Onsager value.
proof idea
The declaration is a direct constant definition with no proof body or lemmas applied.
why it matters
This constant supplies the dimension parameter for all Onsager exponent relations in the module, including alpha_onsager := 2 - D2 * nu_onsager and hyperscaling_onsager : D2 * nu_onsager = 2 - alpha_onsager. It anchors the diagnostic that the Recognition Science framework, which forces D = 3 via the eight-tick octave and J-uniqueness, produces a 38% discrepancy with the D = 2 Onsager value as quantified in Ising2DCert. The declaration therefore demarcates the boundary between the framework's native dimension and the exactly solvable lower-dimensional case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.