gd_highest_moment
plain-language theorem explainer
Gadolinium exhibits a higher saturation magnetic moment per atom than iron under the Recognition Science assignment of saturationMoment. Condensed-matter physicists comparing transition-metal and rare-earth ferromagnets would cite the inequality when discussing maximum spin alignment from f-electron shells. The proof is a one-line wrapper that substitutes the explicit numerical values from the saturationMoment definition and normalizes the resulting arithmetic comparison.
Claim. Let $m_s(Z)$ denote the saturation magnetic moment per atom in Bohr magnetons for atomic number $Z$. Then $m_s(64) > m_s(26)$, with the concrete values $m_s(64) = 7.63$ and $m_s(26) = 2.22$.
background
The saturationMoment function, defined in the same module, assigns explicit values to ferromagnetic elements: 2.22 for iron (Z=26), 1.72 for cobalt (Z=27), 0.61 for nickel (Z=28), and 7.63 for gadolinium (Z=64), with zero for all other atomic numbers. These numbers encode the RS-native saturation moments that arise from the exchange interaction and 8-tick orbital coherence described in the module documentation.
proof idea
The term-mode proof applies simp only [saturationMoment] to unfold the definition into the pair of literals 7.63 and 2.22, then invokes norm_num to discharge the numerical inequality.
why it matters
The result supplies the concrete numerical support for the module's prediction that gadolinium possesses the highest moment among the listed ferromagnetic species, consistent with the 8-tick coherence and f-electron alignment in the RS ferromagnetism derivation. It stands as an isolated fact with no downstream dependents, illustrating how the framework assigns concrete moments without further theorem chaining.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.