dimensional_crossover
plain-language theorem explainer
The theorem shows that the freezing-to-Curie ratio for three-dimensional Heisenberg spin glasses equals the two-dimensional Ising ratio multiplied by the golden ratio phi. Condensed-matter theorists working on spin-glass energy scales would cite it to quantify the extra frustration incurred by moving from two to three dimensions. The proof reduces to unfolding the two ratio definitions, invoking positivity of phi, and simplifying the resulting field expression.
Claim. Let $r_3$ denote the freezing-to-Curie ratio for canonical three-dimensional Heisenberg spin glasses and $r_2$ the corresponding ratio for two-dimensional Ising spin glasses. Then $r_3 = r_2 · ϕ$.
background
The module derives spin-glass freezing ratios from the Recognition Science phi-ladder. The definition freezingRatio3D sets the three-dimensional ratio to 1/phi, while freezingRatio2D sets the two-dimensional ratio to 1/phi squared. These expressions encode the gap-45 frustration prediction: the spin glass occupies the canonical frustrated sector and the ferromagnet the sigma-equals-zero sector, so their energy-scale ratio is the recognition dividend 1/phi. The module document states that canonical three-dimensional Heisenberg spin glasses satisfy T_g / T_c in (0.61, 0.62) and two-dimensional Ising spin glasses satisfy the deeper-frustration band (0.37, 0.40).
proof idea
The proof is a direct algebraic reduction. It unfolds the definitions of freezingRatio3D and freezingRatio2D, introduces the auxiliary fact that phi is nonzero from phi_pos, and finishes with field_simp to clear the common denominator.
why it matters
The result supplies the dimensional-crossover axiom required by the SpinGlassFreezingCert structure and is invoked verbatim inside spin_glass_one_statement to assemble the single-statement summary of the 3D and 2D bands together with their phi relation. It realises the structural claim that passage from two to three dimensions adds exactly one phi-step of frustration, consistent with the eight-tick octave and D=3 landmarks of the forcing chain. The module document lists the empirical falsifier as a median T_g / T_c ratio lying outside (0.61, 0.62) at the 2-sigma level across a corpus of at least ten calibrated spin glasses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.