curie_ratio_bounds
plain-language theorem explainer
The declaration establishes that the ratio of Curie temperatures for cobalt to iron lies strictly between 1.33 and 1.34. Researchers modeling ferromagnetic materials or verifying Recognition Science predictions for transition metals would reference this bound. The proof proceeds as a one-line wrapper that unfolds the ratio definition and applies numerical normalization to confirm the inequality.
Claim. $1.33 < T_C(27)/T_C(26) < 1.34$, where $T_C(Z)$ is the Curie temperature in kelvin assigned to the element with atomic number $Z$.
background
In the Ferromagnetism module the Curie temperature is introduced as a function that returns fixed values for the ferromagnetic transition metals: 1043 K for iron (Z=26) and 1394 K for cobalt (Z=27). The ratio is formed directly as the quotient of these two values. The module situates ferromagnetism inside Recognition Science through exchange interactions derived from the ledger's fermion statistics, 8-tick orbital coherence in d-shells, and the Stoner criterion that links exchange strength to density of states at the Fermi level.
proof idea
The term proof first applies simp to unfold the definitions of the ratio and the Curie-temperature function, reducing the claim to concrete numerical inequalities on 1394 and 1043. Constructor splits the conjunction into two separate bounds; norm_num then discharges both sides by direct arithmetic comparison.
why it matters
The theorem supplies a verified numerical check on the Curie-temperature predictions listed in the module (Fe 1043 K, Co 1394 K). It therefore anchors the ferromagnetism section of the chemistry derivations, even though the accompanying doc-comment records that the observed ratio 1.337 lies nearer phi^0.6 than the earlier phi^(2/5) conjecture. Within the larger framework it supports the 8-tick coherence account of spontaneous spin alignment without asserting an exact phi-power identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.