zero_above_curie
plain-language theorem explainer
The magnetization ratio in the mean-field model vanishes for all temperatures at or above the Curie point. Condensed-matter theorists would cite this when confirming the loss of spontaneous order due to thermal fluctuations. The proof reduces directly to the piecewise definition by unfolding the conditional and applying the temperature hypothesis.
Claim. For real numbers $T$ and $T_C$ with $T$ at least $T_C$, the mean-field magnetization ratio $M(T)/M(0)$ equals zero.
background
The magnetization ratio is defined as zero when temperature meets or exceeds the Curie temperature (or when the Curie temperature itself is zero); otherwise it returns the square root of one minus the square of the reduced temperature. This definition appears inside the ferromagnetism module, which derives spontaneous alignment from exchange interactions, Pauli exclusion, and the eight-tick coherence structure of d-orbitals. The module also states the Stoner criterion and lists predicted Curie temperatures for iron, cobalt, and nickel.
proof idea
The term proof first simplifies the magnetization ratio definition, then simplifies again using the hypothesis that temperature is at least the Curie temperature to select the zero branch of the conditional.
why it matters
The result supplies the high-temperature boundary condition for the magnetization curve inside the Recognition Science treatment of ferromagnetism. It directly implements the statement that thermal fluctuations overcome exchange coupling above the Curie point, consistent with the module's 8-tick coherence and phi-ladder scaling. No downstream theorems yet reference it, leaving the low-temperature branch and numerical predictions as the natural continuation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.