Ising2DCert
plain-language theorem explainer
Ising2DCert packages the exact Onsager critical exponents for the two-dimensional Ising model into a certificate verifying that they obey the Rushbrooke, Fisher, Widom and hyperscaling relations, with alpha equal to zero and nu strictly larger than phi inverse. Researchers comparing renormalization-group scaling predictions to exact solutions in statistical mechanics would cite this structure. It is introduced as a plain record definition that assembles the verified equalities and the RS discrepancy without additional computation.
Claim. A structure asserting that the Onsager exponents for the two-dimensional Ising model satisfy the Rushbrooke relation $alpha + 2 beta + gamma = 2$, the Fisher relation $gamma = nu (2 - eta)$, the Widom relation $gamma = beta (delta - 1)$, the hyperscaling relation $2 nu = 2 - alpha$, the equality $alpha = 0$, and the inequality $nu > phi^{-1}$, where the exponents are the known exact values $nu=1$, $eta=1/4$, $beta=1/8$, $gamma=7/4$, $alpha=0$, $delta=15$.
background
The module examines the two-dimensional Ising model whose critical exponents are known exactly from Onsager's 1944 solution. D2 is defined as the real number 2. The Onsager exponents are given by the sibling definitions: beta_onsager = 1/8, eta_onsager = 1/4, gamma_onsager = 7/4, delta_onsager = 15, nu_onsager = 1, and alpha_onsager = 2 - D2 * nu_onsager which evaluates to zero. The module documentation states: 'The RS leading-order formula ν₀ = φ⁻¹ does NOT reproduce ν = 1 for D = 2. This is expected since RS derives D = 3 as the unique physical dimension.'
proof idea
The declaration is a structure definition that directly assembles the four scaling relations together with the alpha-zero equality and the rs_fails inequality. Each field references the corresponding sibling definition or theorem that establishes the numerical identity for the Onsager values. No tactics or lemmas are applied inside the structure itself; the verification occurs in the referenced upstream results such as rushbrooke_onsager and alpha_onsager_eq.
why it matters
This structure serves as the central certificate for the D = 2 diagnostic. It is instantiated by the downstream definition ising2DCert which supplies concrete proofs for each field. The declaration highlights the failure of the leading RS formula nu_0 = phi^{-1} to match the exact Onsager nu = 1, reinforcing the T8 step that forces D = 3 as the unique physical dimension. It touches the open question of how the phi-ladder extends beyond three dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.