freezingRatio2D_band
plain-language theorem explainer
The declaration proves that the 2D Ising spin-glass freezing ratio lies strictly inside (0.37, 0.40). Condensed-matter theorists testing Recognition Science predictions against 2D Ising data would cite this interval. The argument unfolds the definition 1/phi squared, pulls the bounds 2.5 < phi squared < 2.7, and closes the inequalities with linear arithmetic after rewriting the divisions.
Claim. $0.37 < 1/phi^2 < 0.40$, where the ratio equals the reciprocal of the square of the golden-ratio fixed point.
background
The module derives spin-glass freezing ratios from the Recognition lattice. The 3D Heisenberg case yields the ratio 1/phi; the 2D Ising case replaces this by the deeper-frustration value 1/phi squared. The definition freezingRatio2D is exactly that reciprocal. The lemma phi_squared_bounds supplies the numerical enclosure 2.5 < phi squared < 2.7 that converts the exact algebraic expression into the stated open interval.
proof idea
Unfold freezingRatio2D to obtain 1/phi^2. Obtain the pair of bounds on phi squared from phi_squared_bounds. Establish positivity of phi squared. Rewrite the target inequalities via lt_div_iff and div_lt_iff, then close both sides with nlinarith.
why it matters
The band is packaged inside SpinGlassFreezingCert and appears verbatim in the one-statement theorem spin_glass_one_statement that collects the 3D band, the 2D band, and the exact phi crossover. It supplies the 2D prediction required by the spin-glass track of the Recognition framework, where gap-45 frustration is replaced by the 2D version 1/phi squared.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.