eta_onsager
plain-language theorem explainer
eta_onsager supplies the Onsager critical exponent η = 1/4 for the two-dimensional Ising model. Researchers verifying scaling relations or comparing Recognition Science predictions to exact solutions in D = 2 cite this value. The definition is a direct constant assignment with no computational steps.
Claim. In the two-dimensional Ising model the critical exponent η equals 1/4.
background
The module examines the exact Onsager solution for the 2D Ising model, where critical exponents take rational values: ν = 1, η = 1/4, β = 1/8, γ = 7/4, α = 0 (log divergence), δ = 15. Recognition Science derives D = 3 as the unique physical dimension from the forcing chain (T0 to T8), so its leading-order formula ν₀ = φ^{-1} does not match the Onsager ν = 1. This declaration provides the input η for the scaling relations that recover the other exponents.
proof idea
The declaration is a direct definition that sets eta_onsager to the rational number 1/4.
why it matters
This value enters the scaling theorems beta_from_scaling, delta_from_scaling, and fisher_onsager, which recover β = 1/8, δ = 15, and γ = 7/4 from ν and η. It supports the Ising2DCert structure that records the discrepancy between Onsager ν = 1 and the RS prediction φ^{-1} ≈ 0.618. The module thereby isolates the dimensional specificity of Recognition Science, which forces D = 3 via the eight-tick octave and J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.