freezingRatio3D_band
plain-language theorem explainer
freezingRatio3D_band establishes that the 3D Heisenberg spin-glass freezing-to-Curie ratio lies in the open interval (0.617, 0.622). Condensed-matter physicists validating gap-45 frustration models against CuMn and AuFe data would cite the bound. The argument unfolds the definition 1/phi, invokes the tight numerical bounds on phi, and closes the two inequalities with division lemmas plus nlinarith.
Claim. $0.617 < 1/φ < 0.622$, where φ denotes the golden ratio.
background
In the Spin-Glass Freezing Temperature Ratio module the freezing ratio for canonical 3D Heisenberg spin glasses is introduced by the definition freezingRatio3D := 1/phi. This encodes the gap-45 frustration prediction that the spin-glass energy scale equals the recognition dividend 1/φ relative to the ferromagnetic Curie scale. The module draws the required numerical bounds on phi from the Constants file and arithmetic structures from the Foundation layer.
proof idea
The proof unfolds freezingRatio3D to obtain the expression 1/phi. It obtains the lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo. The left-hand inequality is rewritten via lt_div_iff₀ and discharged by nlinarith; the right-hand inequality follows by the symmetric application of div_lt_iff₀ and nlinarith.
why it matters
The band supplies the numerical component required by the parent theorem spin_glass_one_statement, which packages the 3D interval, the 2D interval 1/φ², and the crossover relation freezingRatio3D = freezingRatio2D * phi. It realizes the Recognition Science gap-45 prediction for spin-glass freezing, placing the ratio inside the empirical CuMn/AuFe window (0.60–0.65) and feeding the SpinGlassFreezingCert structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.