freezingRatio2D_pos
plain-language theorem explainer
The theorem shows that the 2D Ising spin-glass freezing ratio is strictly positive. Condensed-matter researchers using Recognition Science would cite it to confirm the 2D case before applying band bounds in spin-glass certification. The proof is a one-line term that invokes div_pos on numerator 1 and denominator phi squared, with norm_num and pow_pos supplying the positivity facts.
Claim. $0 < 1/phi^2$ where $phi$ is the golden-ratio fixed point.
background
The CondensedMatter.SpinGlassFreezingRatio module defines freezingRatio2D explicitly as 1/phi^2 for the 2D Ising case. This replaces the 3D gap-45 frustration with deeper 2D frustration, predicting T_g/T_c in (0.38,0.39). The upstream freezingRatio2D supplies the closed-form expression while phi_pos (from Constants) guarantees the base is positive. The module derives all ratios from the recognition lattice, with the 3D counterpart at 1/phi.
proof idea
Term-mode proof applies div_pos to the constant 1 (via norm_num) and the positive power phi^2 (via pow_pos on phi_pos). No further tactics or lemmas are required.
why it matters
The result supplies the ratio_2D_pos field inside spinGlassFreezingCert, which bundles positivity and band statements for both 2D and 3D cases. It completes the 2D prediction in Track E3 of the module, linking to the phi-ladder and eight-tick octave of the forcing chain. The parent spinGlassFreezingCert uses it to certify the full set of ratios for downstream spin-glass analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.