exchangeJ
plain-language theorem explainer
exchangeJ assigns exchange energies of 10 meV to iron (Z=26), 14 meV to cobalt (Z=27), and 8 meV to nickel (Z=28), returning zero for every other atomic number. Condensed-matter modelers cite these numbers when computing the spin-coupling strength that stabilizes permanent magnetism in the d-block. The definition is a direct pattern match on the input natural number with no further computation.
Claim. The exchange energy function $J : ℕ → ℝ$ satisfies $J(26) = 10$, $J(27) = 14$, $J(28) = 8$, and $J(Z) = 0$ for all other $Z$.
background
In the Recognition Science account of ferromagnetism the exchange interaction originates in the Pauli exclusion principle applied to d-electrons, which itself follows from the ledger's fermion statistics. The module links this interaction to eight-tick coherence in the d-orbitals, where orbital degeneracy permits Hund's-rule maximum spin alignment. The Stoner criterion then requires that the product of exchange strength and density of states at the Fermi level exceed unity; the tabulated values supply the concrete exchange strengths for Fe, Co and Ni.
proof idea
The definition is a direct case distinction on the atomic number Z that returns the listed positive constants only for the three ferromagnetic elements and zero otherwise.
why it matters
exchangeJ supplies the numerical inputs required by the downstream theorem ferromagnet_positive_J, which proves that every element in ferromagneticElements has positive exchange energy. It therefore anchors the RS mechanism for spontaneous moment alignment inside the eight-tick octave (T7) and supplies the concrete scale for Curie-temperature and domain-wall predictions that follow from phi-ladder scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.