curieTemperature
plain-language theorem explainer
This definition supplies numerical Curie temperatures in kelvin for the primary ferromagnetic elements by atomic number. Researchers deriving magnetic properties from the Recognition Science ledger would reference these values when computing ratios or bounds. The implementation is a direct pattern match on atomic number with no computational steps.
Claim. The Curie temperature $T_C(Z)$ (in kelvin) for atomic number $Z$ equals 1043 for $Z=26$ (iron), 1394 for $Z=27$ (cobalt), 631 for $Z=28$ (nickel), 293 for $Z=64$ (gadolinium), and 0 for all other $Z$.
background
In the ferromagnetism module the Curie temperature marks the point above which thermal fluctuations destroy spontaneous magnetization. It is tied to the exchange interaction derived from Pauli exclusion and the 8-tick coherence in d-orbitals. Upstream, temperature is defined as the inverse of the Lagrange multiplier beta in the Boltzmann distribution, while $K$ denotes the dimensionless bridge ratio phi to the power one half.
proof idea
This is a definition by pattern matching on the atomic number input, returning hardcoded experimental values for the four relevant elements and zero otherwise. No lemmas are applied.
why it matters
This definition provides the numerical inputs for theorems establishing that cobalt has the highest Curie temperature among elements and for bounding the Co/Fe ratio near 1.337. It fills the prediction slot in the ferromagnetism derivation where $T_C$ scales with exchange energy from the 8-tick structure. The module notes that the observed ratio is close to phi to the 0.6 but within uncertainty, leaving open a tighter phi-ladder derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.