stonerI_Fe
plain-language theorem explainer
The declaration assigns the constant value 0.9 to the Stoner exchange parameter for iron. Condensed matter physicists using the Recognition Science model would cite this value when verifying whether iron meets the threshold for spontaneous magnetization via the Stoner criterion. The definition is a direct real-number assignment with no lemmas or computation required.
Claim. The Stoner exchange parameter for iron, denoted $I$, is the real number 0.9 (in eV).
background
The Ferromagnetism module derives permanent magnetism from exchange interactions that arise from Pauli exclusion and ledger fermion statistics. The Stoner criterion requires the product of exchange strength $U$ and density of states at the Fermi level $D(E_F)$ to exceed 1; the parameter here supplies the $U$ value specific to iron. Upstream structures from NucleosynthesisTiers, LedgerFactorization, PhiForcingDerived, SpectralEmergence, UniversalForcingSelfReference, and PhysicsComplexityStructure supply the discrete φ-tier scaling, J-cost convexity, and 8-tick coherence that justify assigning material-specific constants in this setting.
proof idea
The definition is a direct numerical assignment of 0.9. No lemmas are invoked and no tactics are applied; the body is simply the literal real constant.
why it matters
This supplies the exchange parameter required by the downstream theorem fe_stoner_satisfied, which proves iron satisfies the Stoner criterion. It fills the Stoner-criterion step in the CM-010 ferromagnetism derivation, linking to the module's account of 8-tick coherence in d-orbitals and φ-ladder scaling of exchange energy. The assignment is chosen so the product with dos_Fe exceeds 1, matching observed ferromagnetism in Fe.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.