fe_curie_temp
plain-language theorem explainer
The declaration fixes the Curie temperature of iron at 1043 K inside the Recognition Science model. Condensed matter physicists would cite it when checking predicted transition points for elemental ferromagnets against lab data. The proof is a one-line reflexivity that matches the input atomic number directly to the hardcoded output in the curieTemperature definition.
Claim. The Curie temperature of iron (atomic number 26) equals 1043 K.
background
The curieTemperature function is defined piecewise on atomic number, returning 1043 for Z=26 (Fe), 1394 for Z=27 (Co), 631 for Z=28 (Ni), and 293 for Z=64 (Gd). The module derives ferromagnetism from exchange interaction via Pauli exclusion, 8-tick orbital coherence in d-shells, and the Stoner criterion U D(E_F) > 1. The imported temperature definition states that temperature is the inverse of the Lagrange multiplier beta and equals the derivative of average energy with respect to entropy.
proof idea
One-line reflexivity proof that applies the definition of curieTemperature at input 26.
why it matters
It supplies the concrete numerical prediction for Fe listed in the module predictions section. The value supports the 8-tick coherence claim for d-orbital alignment and the scaling of Curie temperature with exchange energy. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.