co_highest_curie
plain-language theorem explainer
Cobalt exhibits the highest Curie temperature among the elemental ferromagnets iron, cobalt and nickel. Condensed matter physicists working in Recognition Science cite the result when checking that the assigned exchange energies respect the observed ordering of magnetic transition temperatures. The proof is a one-line wrapper that unfolds the curieTemperature definition and reduces the resulting numerical inequalities.
Claim. The Curie temperature of cobalt exceeds that of iron and that of nickel: $T_C(27) > T_C(26) ∧ T_C(27) > T_C(28)$, where $T_C(Z)$ is the Curie temperature (in kelvin) assigned to the element of atomic number $Z$.
background
The Ferromagnetism module (CM-010) derives spontaneous magnetization from the Recognition Science ledger via exchange interaction (Pauli exclusion for d-electrons), 8-tick orbital coherence, and the Stoner criterion $U × D(E_F) > 1$. Curie temperature is introduced as the scale at which thermal fluctuations destroy this order, with $T_C$ scaling directly with exchange energy. The supporting definition curieTemperature : ℕ → ℝ maps Z = 26 to 1043 K (Fe), Z = 27 to 1394 K (Co), Z = 28 to 631 K (Ni) and Z = 64 to 293 K (Gd), returning zero otherwise. Upstream structures such as PhiForcingDerived.of supply the J-cost and phi-ladder scaling that justify these discrete assignments in RS-native units.
proof idea
The term proof applies simp only [curieTemperature] to replace each occurrence with the explicit numeric value from the definition, then invokes norm_num to discharge the two strict inequalities by direct arithmetic comparison.
why it matters
The declaration anchors the predicted Curie-temperature ordering (Fe < Co > Ni) stated in the module predictions and thereby confirms consistency with the 8-tick coherence and Stoner criterion inside the Recognition framework. It supplies an empirical checkpoint for phi-scaled magnetic energies without deriving the temperatures from the ledger equations themselves. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.