cobalt_ferromagnetic
plain-language theorem explainer
Cobalt with atomic number 27 satisfies the ferromagnetic predicate under the Recognition Science ledger definition. Chemists deriving magnetic properties from exchange interactions and 8-tick orbital coherence would cite this when verifying transition-metal predictions. The proof reduces to a single native decision step on set membership.
Claim. The element with atomic number 27 is ferromagnetic: $27$ belongs to the ferromagnetic elements or the rare-earth ferromagnets.
background
The Ferromagnetism module derives permanent magnetism from spontaneous alignment of atomic moments. Exchange interaction follows from Pauli exclusion on d-electrons, while 8-tick coherence appears in Hund's-rule spin alignment for d-orbitals. The predicate isFerromagnetic(Z) returns true precisely when Z lies in ferromagneticElements or rareEarthFerromagnets, with Stoner criterion U × D(E_F) > 1 and phi-ladder scaling for Curie temperatures supplied by the module context.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the boolean membership test for Z = 27 against the two source sets.
why it matters
This result confirms the RS prediction of ferromagnetism for cobalt (Z = 27) alongside iron and nickel, filling the explicit list in the module's derivation of exchange-driven order and 8-tick coherence. It directly supports the listed predictions for Fe, Co, Ni and rare-earth cases without introducing new hypotheses. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.