module module moderate

`IndisputableMonolith.Physics.Ising2D`

The Physics.Ising2D module states the Onsager critical exponents for the two-dimensional Ising model inside Recognition Science. It sets nu_onsager to 1 and obtains alpha_onsager = 2 - 2*1 = 0, together with eta, beta, gamma, delta and the Rushbrooke, Fisher and hyperscaling relations. Statistical mechanicians cite these exact values to benchmark RS against the solvable 2D case. The module is a collection of direct definitions that import only the base time quantum from Constants.

claim$alpha = 2 - 2 nu = 0$ with $nu = 1$, $eta = 1/4$, $beta = 1/8$, $gamma = 7/4$, $delta = 15$, satisfying Rushbrooke, Fisher and hyperscaling relations.

background

Recognition Science derives all constants from a single functional equation whose solutions produce the phi-ladder and the eight-tick octave. The upstream Constants module supplies the RS-native time quantum tau_0 = 1 tick. This module specializes those foundations to the two-dimensional Ising model by recording the exact Onsager exponents at criticality, with the supplied doc comment noting alpha = 2 - 2*1 = 0.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Onsager exponents that anchor Recognition Science predictions for critical phenomena in two dimensions. It directly feeds the sibling declarations nu_onsager, alpha_onsager, beta_onsager, gamma_onsager, delta_onsager, rushbrooke_onsager, fisher_onsager and hyperscaling_onsager. These values confirm the framework reproduces the known logarithmic singularity (alpha = 0) and the standard scaling relations for the 2D Ising universality class.

scope and limits

Does not derive the exponents from the J-cost functional equation.
Does not address the three-dimensional Ising model.
Does not compute correlation functions or the partition function.
Does not include finite-size or numerical corrections.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (19)

lemma phi_gt_1618 L27
def D2 L37
def nu_onsager L38
def eta_onsager L39
def beta_onsager L40
def gamma_onsager L41
def delta_onsager L42
def alpha_onsager L51
theorem alpha_onsager_eq L53
theorem rushbrooke_onsager L57
theorem fisher_onsager L61
theorem hyperscaling_onsager L65
theorem widom_onsager L69
theorem beta_from_scaling L73
theorem delta_from_scaling L77
theorem rs_leading_order_below_onsager L88
theorem onsager_rs_gap L97
structure Ising2DCert L107
def ising2DCert L115