co_high_anisotropy
plain-language theorem explainer
Cobalt shows the highest magnetic anisotropy among the primary 3d ferromagnets, producing the narrowest Bloch domain walls and the largest wall energy density. Condensed-matter physicists comparing anisotropy parameters across Fe, Co, and Ni would cite the inequality when modeling domain structures. The proof is a direct numerical evaluation of the two tabulated functions at atomic numbers 26 and 27.
Claim. Let $w(Z)$ be the Bloch domain-wall width in nm and $E(Z)$ the wall energy density in mJ/m², both defined piecewise on atomic number $Z$. Then $w(27) < w(26) $ and $ E(27) > E(26) $, with concrete assignments $w(26)=40$, $w(27)=15$, $E(26)=1.5$, $E(27)=3.0$.
background
The Ferromagnetism module derives spontaneous spin alignment from the Recognition ledger via Pauli exclusion, 8-tick orbital coherence, and the Stoner criterion $U D(E_F)>1$. Domain walls arise to minimize magnetostatic energy; their width scales as the square root of exchange stiffness over anisotropy constant, while energy density scales with the square root of their product. The two functions domainWallWidth and domainWallEnergy are defined directly on atomic number with hardcoded values for Fe (Z=26), Co (Z=27), and Ni (Z=28). Upstream results supply the Recognition structure M and the triangular-number abbreviation T, but the present theorem uses only the two wall definitions.
proof idea
The term proof unfolds the two piecewise definitions by simplification, then applies numerical normalization to compare the literal constants 15 < 40 and 3.0 > 1.5.
why it matters
The result verifies the module prediction that Co possesses the highest anisotropy, consistent with the 8-tick coherence and Stoner scaling described in the module documentation. It supplies a concrete comparison that can be referenced when domain-wall energetics are later linked to phi-ladder rung assignments, although the numerical inputs themselves remain external to the Recognition functional equation. No downstream theorems yet consume the statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.