onsager_rs_gap
plain-language theorem explainer
The declaration establishes that the Onsager correlation-length exponent in two dimensions exceeds the Recognition Science leading-order prediction by more than 38 percent. A physicist testing dimensional specificity of the phi-ladder formulas would cite this gap to confirm that the base formula applies only for D equals three. The tactic proof unfolds the constant definition of nu_onsager, bounds one over phi below 0.619 via the lower bound on phi, and closes the inequality with linear arithmetic.
Claim. $0.38 < 1 - phi^{-1}$ where the left-hand side uses the Onsager correlation-length exponent equal to 1 and phi denotes the golden ratio.
background
The module treats the two-dimensional Ising model whose exact Onsager solution supplies the critical exponents nu equals 1, eta equals 1/4, beta equals 1/8, gamma equals 7/4, alpha equals 0 (log divergence), and delta equals 15. Recognition Science supplies the leading-order formula nu zero equals phi inverse. The upstream lemma phi greater than 1.618 supplies the numerical lower bound on the golden ratio that quantifies the discrepancy.
proof idea
The proof unfolds the definition of nu_onsager to the constant 1. It then shows one over phi is less than 0.619 by applying the reciprocal inequality together with the bound phi greater than 1.618 and a numerical check. Linear arithmetic finishes the target inequality.
why it matters
This result records the mismatch between the Recognition Science phi-based formula and the exact two-dimensional solution, consistent with the framework derivation that D equals 3 is the unique physical dimension from the forcing chain. It sits with the other Onsager exponent checks in the module and supports the claim that the eight-tick octave and three spatial dimensions arise uniquely. No downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.