module module high

`IndisputableMonolith.Physics.Ising2D`

The Physics.Ising2D module assembles the Onsager critical exponents for the two-dimensional Ising model inside the Recognition Science framework. Researchers comparing exact lattice solutions to RS constants would cite these results. The module consists of a collection of definitions and theorems, one per exponent, anchored by the specific-heat relation alpha equals zero.

claimOnsager critical exponents for the 2D Ising model satisfy $\alpha=0$, $\beta=1/8$, $\gamma=7/4$, $\delta=15$, $\nu=1$, $\eta=1/4$, with the hyperscaling relation giving $\alpha=2-2\cdot1=0$.

background

The module imports IndisputableMonolith.Constants, whose doc-comment states that the fundamental RS time quantum is $\tau_0=1$ tick. It supplies the 2D Ising setting, where the J-uniqueness function, phi-ladder, and eight-tick octave from the upstream forcing chain (T0-T8) are specialized to spatial dimension two. The module doc-comment records the direct statement Onsager $\alpha=2-2\cdot1=0$.

proof idea

This is a definition module, no proofs. The overall structure declares one result per Onsager exponent (nu_onsager, eta_onsager, alpha_onsager, etc.) together with the auxiliary D2 and phi_gt_1618 facts needed to fix the values.

why it matters in Recognition Science

The module supplies the exact Onsager benchmark values that later Recognition Science results use when testing the alpha band and hyperscaling relations. It fills the lattice-model slot in the forcing chain and connects the D=3 spatial-dimension result to the two-dimensional specialization via the D2 sibling.

scope and limits

Does not derive the exponents from the Recognition Composition Law.
Does not treat the three-dimensional Ising model.
Does not incorporate the mass formula or Berry creation threshold.
Does not address finite-size scaling or numerical verification.

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