delta_onsager
plain-language theorem explainer
delta_onsager records the exact Onsager value of the critical exponent δ = 15 for the two-dimensional Ising model. Researchers checking scaling identities such as Widom's relation or the Ising2DCert structure would cite this constant. The definition is a direct numerical assignment with no computation or derivation steps.
Claim. The Onsager critical exponent $δ$ for the two-dimensional Ising model is defined as 15.
background
The module states that the two-dimensional Ising model is exactly solvable with Onsager exponents ν = 1, η = 1/4, β = 1/8, γ = 7/4, α = 0 (logarithmic divergence), and δ = 15. These values are used to test whether RS φ-algebraic formulas extend to D = 2. The module notes that the RS leading-order formula ν₀ = φ^{-1} does not reproduce ν = 1, as expected because the framework derives D = 3 as the unique physical dimension from the forcing chain T0 to T8.
proof idea
This is a direct definition that assigns the constant 15.
why it matters
The definition supplies the value required by delta_from_scaling to recover δ = (D2 + 2 - eta_onsager)/(D2 - 2 + eta_onsager) = 15 and by the Ising2DCert structure to certify the Widom relation gamma_onsager = beta_onsager * (delta_onsager - 1). It marks the explicit discrepancy between Onsager exponents and RS φ-based predictions, reinforcing that the eight-tick octave and D = 3 emerge uniquely from the forcing chain while D = 2 serves only as a diagnostic case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.