ising2DCert
plain-language theorem explainer
This definition assembles the exact Onsager critical exponents for the two-dimensional Ising model into a single certificate verifying all standard scaling relations. A physicist studying critical phenomena in low dimensions would cite it to confirm consistency with Rushbrooke, Fisher, Widom, and hyperscaling equalities while highlighting the mismatch with Recognition Science's leading-order prediction. The construction is a direct record instantiation that references the pre-proved Onsager identities.
Claim. Let α, β, γ, ν, η, δ denote the Onsager critical exponents for the two-dimensional Ising model with D = 2. The certificate asserts α + 2β + γ = 2, γ = ν(2 − η), γ = β(δ − 1), 2ν = 2 − α, α = 0, and ϕ⁻¹ < ν, where ϕ is the golden ratio.
background
The module examines the exactly solvable two-dimensional Ising model whose critical exponents were derived by Onsager in 1944. These exponents take the exact rational values ν = 1, η = 1/4, β = 1/8, γ = 7/4, α = 0 (logarithmic divergence), and δ = 15. The structure collects the four scaling relations together with the statements that α = 0 and that the Recognition Science leading-order formula ν₀ = ϕ⁻¹ lies below the true ν. Upstream theorems establish each relation by direct substitution and ring simplification.
proof idea
The definition constructs the certificate by a direct record literal. Each field is populated by the corresponding theorem: rushbrooke_onsager supplies the Rushbrooke equality, fisher_onsager the Fisher relation, widom_onsager the Widom relation, hyperscaling_onsager the hyperscaling relation, alpha_onsager_eq the statement α = 0, and rs_leading_order_below_onsager the inequality ϕ⁻¹ < ν.
why it matters
This certificate demonstrates that the Onsager solution satisfies all thermodynamic scaling relations in two dimensions while exposing the mismatch with the Recognition Science prediction derived under the assumption of three spatial dimensions. It supports the framework claim that D = 3 emerges uniquely from the forcing chain and that the phi-ladder formulas are dimension-specific. The result closes the diagnostic loop for D = 2 without providing a counterexample to the overall theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.