SpinGlassFreezingCert
plain-language theorem explainer
The SpinGlassFreezingCert structure bundles positivity, numerical bands, and the exact phi scaling for the 3D Heisenberg and 2D Ising spin-glass freezing ratios. Condensed-matter researchers comparing T_g/T_c data on CuMn or AuFe would cite it to anchor frustration predictions. It is a pure structure definition that assembles the already-proved ratio definitions and their crossover equality.
Claim. A structure certifying that the 3D Heisenberg spin-glass freezing ratio $r_{3D}$ satisfies $0 < r_{3D}$ and $0.617 < r_{3D} < 0.622$, the 2D Ising spin-glass freezing ratio $r_{2D}$ satisfies $0 < r_{2D}$ and $0.37 < r_{2D} < 0.40$, and $r_{3D} = r_{2D} phi$, where $phi$ denotes the golden ratio.
background
In this module the 3D Heisenberg freezing ratio is defined as $1/phi$ and the 2D Ising ratio as $1/phi^2$. These arise from the gap-45 frustration sector of the recognition lattice, with the ferromagnet supplying the zero-frustration reference scale. The module states that canonical 3D spin glasses realize $T_g/T_c$ inside (0.61, 0.62) while 2D versions sit deeper at (0.38, 0.39).
proof idea
This is a structure definition that packages the four positivity and band statements together with the dimensional_crossover equality. It serves as a one-line wrapper collecting the already-established facts about freezingRatio3D and freezingRatio2D.
why it matters
The certificate supplies the master structural claim for Track E3, feeding directly into the spinGlassFreezingCert instance. It encodes the phi-step frustration increase from 3D to 2D, consistent with the T5 J-uniqueness and T6 phi fixed-point landmarks of the forcing chain. It touches the open falsifiability question of whether a cross-system median of $T_g/T_c$ lies outside the predicted band at 2 sigma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.