pith. sign in
module module high

IndisputableMonolith.CondensedMatter.SpinGlassFreezingRatio

show as:
view Lean formalization →

The SpinGlassFreezingRatio module sets the freezing-to-Curie ratio for canonical 3D Heisenberg spin glasses to exactly 1/φ. Condensed-matter theorists modeling spin-glass transitions cite these definitions when mapping Recognition Science constants onto measured temperature ratios. The module is organized as a collection of ratio definitions for 3D and 2D cases plus supporting positivity and band lemmas.

claimThe freezing-to-Curie ratio equals $\phi^{-1}$ for canonical 3D Heisenberg spin glasses, where $\phi$ is the self-similar fixed point of the Recognition Composition Law.

background

Recognition Science obtains all constants from the forcing chain T0-T8 that terminates with D=3 and the phi-ladder. This module imports Constants, whose sole documented object is the fundamental time quantum $\tau_0=1$ tick. The central definition therefore expresses the 3D freezing ratio directly as $1/\phi$ and supplies auxiliary lemmas that locate the result inside the allowed band.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the numerical ratio required by SpinGlassFreezingCert and spin_glass_one_statement. It therefore inserts the phi fixed point (T6) into a concrete condensed-matter observable. No open questions are closed here.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)