pith. sign in
theorem

spin_glass_one_statement

proved
show as:
module
IndisputableMonolith.CondensedMatter.SpinGlassFreezingRatio
domain
CondensedMatter
line
127 · github
papers citing
none yet

plain-language theorem explainer

Canonical 3D Heisenberg spin glasses exhibit a freezing-to-Curie ratio inside (0.617, 0.622) while 2D Ising versions lie inside (0.37, 0.40), with the three-dimensional ratio exactly equal to the two-dimensional ratio multiplied by phi. Condensed-matter theorists comparing spin-glass data to the recognition lattice would cite the statement. The proof is a one-line term that assembles the three upstream band and crossover results.

Claim. Let $r_3 = 1/phi$ be the freezing-to-Curie ratio for canonical 3D Heisenberg spin glasses and $r_2 = 1/phi^2$ the ratio for canonical 2D Ising spin glasses. Then $0.617 < r_3 < 0.622$, $0.37 < r_2 < 0.40$, and $r_3 = r_2 · phi$.

background

The module defines the three-dimensional freezing ratio as $1/phi$ and the two-dimensional ratio as $1/phi^2$, where phi is the golden-ratio fixed point forced by the recognition composition law. The dimensional-crossover result states that the three-dimensional ratio equals the two-dimensional ratio multiplied by phi, which encodes the claim that passage from two to three dimensions removes one step of frustration. The local setting is Track E3 of Plan v6, which treats the spin-glass freezing temperature as the canonical gap-45 frustration sector of the recognition lattice while the ferromagnet occupies the sigma = 0 sector.

proof idea

The proof is the term that packages the three upstream results: the numerical band theorem for the three-dimensional ratio, the numerical band theorem for the two-dimensional ratio, and the algebraic equality that relates them by multiplication by phi. No additional tactics are applied once those component statements are supplied.

why it matters

The declaration consolidates the concrete numerical predictions that follow from the phi-ladder structure for spin-glass systems. It supplies the gap-frustrated sector claim for three-dimensional Heisenberg glasses and the deeper-frustration claim for two-dimensional Ising glasses, directly implementing the module's stated link to the recognition dividend $1/phi$. No downstream uses are recorded, yet the statement supplies the testable interval that would be checked against a corpus of at least ten calibrated spin-glass systems.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.