fe_stoner_satisfied
plain-language theorem explainer
The declaration verifies that iron satisfies the Stoner criterion for spontaneous ferromagnetism. Condensed matter physicists modeling transition-metal magnetism cite it when checking stability of ferromagnetic order in Fe. The proof is a one-line term reduction that unfolds the two constant definitions and confirms the numerical product exceeds unity.
Claim. $I_{Stoner,Fe} D(E_F,Fe) > 1$, where $I_{Stoner,Fe}$ is the Stoner exchange parameter (0.9 eV) and $D(E_F,Fe)$ is the density of states at the Fermi level (1.5 states/eV/atom).
background
The module derives ferromagnetism from Recognition Science by linking Pauli exclusion to exchange interaction, 8-tick orbital coherence in d-shells, and the Stoner criterion that ferromagnetism occurs when the product of exchange strength U and density of states at the Fermi level exceeds 1. The upstream definitions supply the concrete values: stonerI_Fe := 0.9 (Stoner parameter for Fe in eV) and dos_Fe := 1.5 (density of states for Fe at Fermi level in states/eV/atom). These constants are treated as inputs that already incorporate φ-ladder scaling for the relevant transition-metal rung.
proof idea
The term proof applies simp only to unfold the two constant definitions, then norm_num to evaluate the resulting arithmetic inequality 0.9 * 1.5 > 1.
why it matters
The result places iron inside the set of elements predicted to be ferromagnetic by the RS mechanism (exchange from fermion statistics plus 8-tick coherence). It directly supports the module's listed predictions for Fe, Co, Ni and the relation of Curie temperature to exchange energy. No downstream theorems yet consume it; the declaration closes the numerical check for the Stoner step in the ferromagnetism derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.