freezingRatio3D_pos
plain-language theorem explainer
The declaration proves that the 3D Heisenberg spin-glass freezing ratio equals one over the golden ratio and is strictly positive. Condensed-matter researchers modeling canonical spin glasses would cite the bound when comparing freezing and Curie temperatures across CuMn and AuFe systems. The proof is a one-line wrapper that applies the division-positivity lemma with a numerical check on the numerator and the established positivity of the golden ratio.
Claim. $0 < 1/φ$, where $φ$ is the golden ratio fixed point of the recognition composition law.
background
The module derives the freezing-to-Curie ratio for canonical 3D Heisenberg spin glasses under the gap-45-frustration prediction. The upstream definition sets the ratio explicitly to one over phi. The band operation supplies arithmetic conjunction on stable states via bit multiplication, though it is not required for the positivity argument. The local setting is the Recognition Science claim that the spin-glass energy scale realizes the frustrated sector while the ferromagnet realizes the zero-sigma sector, with their ratio fixed at one over phi.
proof idea
The proof is a one-line wrapper that invokes the div_pos lemma. It supplies a numerical normalization for the positivity of the numerator and the known positivity of phi for the denominator.
why it matters
This positivity result is required by the spinGlassFreezingCert structure that assembles the full set of 3D and 2D ratio bounds. It fills the gap-45-frustration prediction in the Recognition framework and connects to the forcing chain in which phi emerges as the self-similar fixed point. The result supports the predicted band (0.61, 0.62) that sits inside the empirical CuMn and AuFe window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.