domainWallWidth
plain-language theorem explainer
Domain wall width assigns measured Bloch widths in nanometers to atomic numbers of the ferromagnetic transition metals. Condensed matter researchers in the Recognition Science program cite it when evaluating domain energetics or comparing anisotropy strengths. The definition is realized as a direct case distinction on the input atomic number that returns tabulated values for Z=26,27,28 and zero otherwise.
Claim. The Bloch domain wall width function $w : ℕ → ℝ$ (nm) is defined by the cases $w(26)=40$, $w(27)=15$, $w(28)=100$, and $w(Z)=0$ for every other natural number $Z$.
background
In the Recognition Science account of ferromagnetism, spontaneous alignment of atomic moments follows from the exchange interaction derived from Pauli exclusion and the 8-tick coherence of d-orbitals. Domain walls form to reduce magnetostatic energy; their width scales as the square root of exchange stiffness over anisotropy constant and is therefore sensitive to phi-ladder scaling of material parameters. The upstream density definition supplies this scaling via density(k) := phi^k.
proof idea
Direct definition by pattern matching on the atomic-number argument. It returns the three tabulated widths for iron, cobalt and nickel and zero for every other input, without calling any lemmas.
why it matters
The definition supplies the concrete numerical inputs required by the co_high_anisotropy theorem, which proves cobalt possesses the narrowest walls and therefore the highest anisotropy energy. It thereby connects the abstract Stoner criterion and 8-tick orbital degeneracy to observable domain structure inside the phi-ladder framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.