ferromagneticElements
plain-language theorem explainer
The definition enumerates the atomic numbers of the three primary room-temperature ferromagnetic elements as 26, 27 and 28. Condensed-matter physicists working within the Recognition Science derivation of magnetism cite this list when checking exchange positivity or 3d-metal classification. It is realized as a direct constant list that downstream simplifications reduce against to obtain the required inequalities.
Claim. The atomic numbers of the elements that exhibit ferromagnetism at room temperature are the list $Z = 26, 27, 28$ (Fe, Co, Ni).
background
The module derives ferromagnetism from the exchange interaction that follows from Pauli exclusion applied to d-electrons, the 8-tick coherence visible in d-orbital degeneracy and Hund's rule, and the Stoner criterion $U D(E_F) > 1$ whose scaling is tied to the phi-ladder. Curie temperature and domain formation are stated to follow from the same exchange energy. The supplied definition supplies the concrete atomic numbers that instantiate these mechanisms for the three 3d metals.
proof idea
The declaration is a direct definition that assigns the constant list [26, 27, 28] with no lemmas or tactics applied.
why it matters
It supplies the base data for the theorem ferromagnet_positive_J, which concludes exchangeJ Z > 0, and for ferromagnets_are_3d_metals, which records the [Ar] 3d^n 4s^2 configurations. The list therefore closes the link between the eight-tick octave (T7) and the observed ferromagnetic elements, while feeding the Stoner-criterion and Curie-temperature statements in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.