widom_onsager
plain-language theorem explainer
The Widom scaling relation equates the susceptibility exponent to the product of the order-parameter exponent and one less than the critical-isotherm exponent using the exact Onsager values for the two-dimensional Ising model. Researchers checking scaling hypotheses or comparing exact solutions against renormalization-group predictions would cite this identity. The proof is a direct algebraic reduction after unfolding the three constant definitions.
Claim. In the two-dimensional Ising model the Widom relation states that the susceptibility exponent equals the order-parameter exponent times one less than the critical-isotherm exponent: $7/4 = (1/8) (15 - 1)$.
background
The module verifies that the exact Onsager exponents for the two-dimensional Ising model satisfy all standard scaling relations. The three relevant constants are defined directly as beta_onsager = 1/8, gamma_onsager = 7/4, and delta_onsager = 15. These values are known to obey Rushbrooke, Fisher, Widom, and hyperscaling identities, even though the Recognition Science leading-order formula for the correlation-length exponent does not reproduce the Onsager value of one when D equals two.
proof idea
The term proof unfolds the three constant definitions for gamma_onsager, beta_onsager, and delta_onsager, then applies the ring tactic to confirm the algebraic identity.
why it matters
This theorem supplies the Widom entry inside the ising2DCert certificate that collects all four scaling relations for the Onsager solution. It forms part of the module's diagnostic showing that the phi-algebraic formulas of Recognition Science are dimension-specific and correctly force D equals three rather than two, consistent with the eight-tick octave and the derivation of spatial dimensions in the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.