domainWallEnergy
plain-language theorem explainer
Domain wall energy density in mJ/m² is assigned by atomic number with fixed values 1.5 for iron (Z=26), 3.0 for cobalt (Z=27), and 0.5 for nickel (Z=28), returning zero for every other input. Materials modelers working inside the Recognition Science account of ferromagnetism would cite these numbers when computing wall contributions to total magnetic energy. The definition is a direct case match on the atomic number with no further reduction or lemma application.
Claim. Domain wall energy density $E(Z)$ (mJ/m²) equals 1.5 when $Z=26$, 3.0 when $Z=27$, 0.5 when $Z=28$, and 0 for all other natural numbers $Z$.
background
In the ferromagnetism module, spontaneous alignment of atomic moments arises from exchange interactions rooted in Pauli exclusion for d-electrons, with 8-tick orbital degeneracy enforcing Hund's rule maximum spin. Domain walls form to lower magnetostatic energy; their width and energy are stated to follow φ-ladder scaling. The upstream has class from AsteroidOreSpectroscopy supplies the precedent that characteristic frequencies obey ω_k = ω_0 · φ^k, supplying the same rung-based scaling used here for magnetic properties.
proof idea
The definition is a direct case distinction on the atomic-number argument that returns the three listed constants for Z = 26, 27, 28 and zero otherwise. No lemmas or tactics are invoked.
why it matters
The definition supplies the concrete numbers required by the downstream co_high_anisotropy theorem, which proves cobalt possesses both the narrowest walls and the highest wall energy. It occupies the domain-wall slot inside the CM-010 derivation, linking the eight-tick coherence of d-shells and φ-scaling of wall properties to the Stoner criterion and Curie-temperature predictions. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.