saturationMoment
plain-language theorem explainer
Saturation magnetic moment per atom in Bohr magnetons is supplied as a piecewise function on atomic number for iron, cobalt, nickel and gadolinium. Researchers comparing magnetic properties in the Recognition Science model cite this definition when proving inequalities between moments. The definition proceeds by direct pattern matching on the atomic number with default zero.
Claim. The saturation magnetic moment per atom (in Bohr magnetons) is the function $m : ℕ → ℝ$ such that $m(26) = 2.22$, $m(27) = 1.72$, $m(28) = 0.61$, $m(64) = 7.63$, and $m(Z) = 0$ otherwise.
background
In the Recognition Science treatment of ferromagnetism the saturation moment arises from exchange interactions derived from Pauli exclusion and the 8-tick coherence of d-orbitals. The module sets out the Stoner criterion relating exchange strength to density of states at the Fermi level, with scaling tied to the phi-ladder. Upstream, the has class defines characteristic spectral peaks at frequencies scaled by powers of phi, providing a ranking mechanism that parallels the rung assignments here.
proof idea
The definition is supplied directly by case analysis on the input atomic number, returning the listed numerical values for the four ferromagnetic species and zero elsewhere. No lemmas are invoked; it is a pure data definition.
why it matters
This definition supplies the numerical inputs for the comparison theorems establishing that iron exceeds nickel and gadolinium exceeds iron. It fills the CM-010 slot in the ferromagnetism derivation by providing concrete values consistent with the 8-tick structure and phi-scaling of moments. The framework predicts these moments via the phi-ladder mass formula adapted to magnetic moments, leaving open the first-principles derivation of the exact coefficients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.