Chemistry Ferromagnetism Nonzero Below Curie

The magnetization ratio

Ferromagnetism is the mechanism by which materials such as iron, cobalt, and nickel form permanent magnets. It arises from the spontaneous alignment of atomic magnetic moments. Each ferromagnet has a characteristic Curie temperature, the temperature above which thermal fluctuations overwhelm the exchange coupling and destroy the magnetic order. Iron's Curie temperature is 1043 K, cobalt's is 1394 K, and nickel's is 631 K. The framework's library of machine-checked formal theorems captures this behavior in a simple model: a magnetization ratio that is positive whenever the temperature is below the Curie point, and zero at or above it.

The declaration nonzero_below_curie states this in precise terms. For any temperature T and Curie temperature T_C, if T is nonnegative, T is strictly less than T_C, and T_C is positive, then the magnetization ratio is strictly greater than zero. The companion theorem zero_above_curie states the complementary fact: if T is at least T_C, the ratio is exactly zero. Together they define a sharp transition: the ratio is positive on one side of the Curie point and zero on the other, with no intermediate state.

The ratio itself is defined by a formula: for T below T_C, it equals the square root of 1 minus (T/T_C) squared, a form the library labels as approximate near the transition. This is a definitional choice, not a derived physical law. The library also records measured values for the elements: the Curie temperatures above, saturation moments per atom (iron 2.22 Bohr magnetons, cobalt 1.72, nickel 0.61, gadolinium 7.63), and domain wall widths in nanometers. Theorems check that cobalt has the highest Curie temperature among the three 3d metals, that iron's moment exceeds nickel's, and that gadolinium's moment exceeds iron's.

What the declaration does not claim is as important as what it proves. It does not establish that any real material actually exhibits ferromagnetism; that is a separate empirical fact. It does not derive the Curie temperature values from first principles; those are entered as definitions, not proved. And it does not assert that the magnetization ratio formula is the true physical law; the library itself calls it approximate. The theorem's force is conditional: within the model, given the definitions, the ratio behaves as stated. The physical bridge from the framework's recognition ledger to these material properties is not part of this declaration.

What a reader can take away is a clean logical skeleton for the familiar fact that magnets stop working when heated enough. The framework models the transition as a binary switch in a ratio, positive below the Curie point and zero above. The real physics is richer, with domains, hysteresis, and critical exponents, but the declaration pins down the simplest structural claim: below the threshold, the magnetization ratio is nonzero.

/-- Magnetization is non-zero below Curie temperature.
    Requires T ≥ 0 (physical temperature). -/
theorem nonzero_below_curie (T T_C : ℝ) (hT_nonneg : T ≥ 0) (hT : T < T_C) (hT_C : T_C > 0) :
    magnetizationRatio T T_C > 0 := by
  simp only [magnetizationRatio]
  have h1 : ¬(T ≥ T_C) := by linarith
  have h2 : T_C ≠ 0 := by linarith
  simp only [h1, h2, or_self, ite_false]
  -- √(1 - (T/T_C)²) > 0 when 0 ≤ T < T_C
  apply Real.sqrt_pos_of_pos
  -- Need: 1 - (T/T_C)² > 0, i.e., (T/T_C)² < 1
  have h_ratio_nonneg : T / T_C ≥ 0 := div_nonneg hT_nonneg (le_of_lt hT_C)
  have h_ratio_lt_one : T / T_C < 1 := by rw [div_lt_one hT_C]; exact hT
  have h_abs_lt : |T / T_C| < 1 := by rw [abs_of_nonneg h_ratio_nonneg]; exact h_ratio_lt_one
  have h_sq_lt_one : (T / T_C) ^ 2 < 1 := (sq_lt_one_iff_abs_lt_one _).mpr h_abs_lt
  linarith

/-- Magnetization is zero above Curie temperature. -/
theorem zero_above_curie (T T_C : ℝ) (hT : T ≥ T_C) :
    magnetizationRatio T T_C = 0 := by
  simp only [magnetizationRatio]
  simp only [hT, true_or, ite_true]

/-- Magnetization ratio M(T)/M(0) for mean-field (Brillouin). -/
def magnetizationRatio (T T_C : ℝ) : ℝ :=
  if T ≥ T_C ∨ T_C = 0 then 0
  else Real.sqrt (1 - (T / T_C) ^ 2)  -- Approximate near T_C

/-- Curie temperature for ferromagnetic elements (K). -/
def curieTemperature : ℕ → ℝ
| 26 => 1043  -- Fe
| 27 => 1394  -- Co
| 28 => 631   -- Ni
| 64 => 293   -- Gd (just below room temperature)
| _ => 0

What this page does not claim

The theorem does not prove that iron, cobalt, or nickel are ferromagnetic; that is a separate empirical fact entered as data. The theorem does not derive the Curie temperature values from the framework's axioms; they are definitions, not conclusions. The magnetization ratio formula is labeled approximate near T_C and is not claimed to be the exact physical law.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Chemistry/Ferromagnetism.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: