isFerromagnetic
plain-language theorem explainer
The definition returns true for an atomic number Z precisely when Z matches one of the transition metals 26-28 or rare-earth ferromagnets 64-66. Condensed-matter physicists applying the Recognition Science ledger to magnetic materials would cite it to classify spontaneous magnetization. It is realized as a direct Boolean disjunction over two fixed finite lists of atomic numbers.
Claim. The predicate holds for atomic number $Z$ if and only if $Z$ belongs to the set of ferromagnetic transition metals or to the set of rare-earth ferromagnets.
background
The Ferromagnetism Derivation module (CM-010) treats ferromagnetism as spontaneous alignment of atomic moments arising from Pauli-derived exchange interactions and 8-tick orbital coherence in d-shells. Two supporting lists encode the empirical cases: ferromagneticElements supplies the atomic numbers 26 (Fe), 27 (Co), 28 (Ni); rareEarthFerromagnets supplies 64 (Gd), 65 (Tb), 66 (Dy). These lists instantiate the module's predictions that only these elements satisfy the Stoner criterion at room temperature under phi-ladder scaling.
proof idea
The definition is a one-line wrapper that returns the disjunction of membership tests against the two element lists; no auxiliary lemmas or tactics are invoked.
why it matters
It supplies the classification predicate used by the three downstream theorems that certify ferromagnetism for iron, cobalt, and nickel. Those theorems directly realize the CM-010 predictions and connect to the eight-tick coherence (T7) and fermion statistics of the forcing chain. The predicate therefore closes the empirical interface between the ledger and observed permanent magnets without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.