dos_Fe
plain-language theorem explainer
dos_Fe supplies the numerical value 1.5 for the density of states at the Fermi level in iron, in states per eV per atom. Condensed-matter researchers applying the Recognition Science Stoner criterion cite this constant to confirm ferromagnetism in transition metals such as Fe. The definition is a direct real-number assignment with no computation or derivation steps.
Claim. The density of states for iron at the Fermi level is $D(E_F) = 1.5$ states/eV/atom.
background
The Ferromagnetism module (CM-010) derives permanent magnetism from spontaneous alignment of atomic moments, arising from the exchange interaction rooted in Pauli exclusion and the ledger's fermion statistics. The Stoner criterion states that ferromagnetism occurs when the product of exchange strength U and density of states at the Fermi level D(E_F) exceeds 1; this constant supplies D(E_F) for iron (Z=26). The module links the criterion to 8-tick coherence in d-orbitals and phi-ladder scaling for Curie temperatures and domain walls.
proof idea
Direct definition that assigns the real number 1.5. No lemmas or tactics are invoked; the value is referenced by name in the simplification step of the downstream Stoner-criterion theorem.
why it matters
This definition supplies the D(E_F) input required by fe_stoner_satisfied, which confirms iron satisfies the Stoner criterion U × D(E_F) > 1. It fills the numerical slot in the module's RS Mechanism section on exchange interaction and 8-tick coherence. The value supports the framework prediction of ferromagnetism in Fe, Co, Ni and connects to the eight-tick octave (T7) structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.