nonzero_below_curie
plain-language theorem explainer
The theorem shows that the mean-field magnetization ratio remains strictly positive for nonnegative temperatures below the Curie point. Condensed-matter physicists modeling ferromagnetic phase transitions would cite it to confirm the order parameter vanishes only at and above T_C. The proof unfolds the piecewise definition of the ratio and reduces the inequality to the positivity of the square root via case analysis and elementary real bounds.
Claim. Let $T, T_C$ be real numbers satisfying $T ≥ 0$, $T_C > 0$, and $T < T_C$. Then the mean-field magnetization ratio $M(T)/M(0)$ satisfies $M(T)/M(0) > 0$, where the ratio equals $√(1 - (T/T_C)^2)$ when $T < T_C$ and $T_C ≠ 0$.
background
The module derives ferromagnetism from the Recognition Science ledger via exchange interaction (from Pauli exclusion on d-electrons), 8-tick coherence in orbital degeneracy, and the Stoner criterion $U × D(E_F) > 1$. Curie temperature marks the point where thermal fluctuations destroy spontaneous alignment, with $T_C$ scaling to exchange energy. Magnetization ratio is defined as the mean-field (Brillouin) form: zero above $T_C$ or when $T_C = 0$, otherwise $√(1 - (T/T_C)^2)$ near the transition.
proof idea
The tactic proof first simplifies with the magnetizationRatio definition, then uses linarith to obtain the negation of the if-condition and $T_C ≠ 0$. It applies Real.sqrt_pos_of_pos and reduces the radicand positivity to $(T/T_C)^2 < 1$ via div_nonneg, div_lt_one, abs_of_nonneg, and sq_lt_one_iff_abs_lt_one, closing with linarith.
why it matters
The result verifies that the ferromagnetic order parameter is nonzero in the ordered phase, consistent with the module's 8-tick coherence for 3d metals (Z = 26, 27, 28) and the RS prediction of ferromagnetism in Fe, Co, Ni. It fills the local verification step for the Curie transition within the broader chemistry derivations; no direct downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.