module module moderate

`IndisputableMonolith.Chemistry.Ferromagnetism`

The Ferromagnetism module catalogs elements that exhibit ferromagnetism at room temperature inside the Recognition Science chemistry scaffold. Materials physicists would cite it for zero-parameter lists of room-temperature magnets such as iron, cobalt and nickel. The module supplies definitions and basic predicates with no proofs, inheriting its structure directly from the PeriodicTable engine.

claimThe set of elements $E$ satisfying the room-temperature ferromagnetism predicate, constructed from the eight-tick octave mapping on the $\phi$-ladder with fixed $s/p/d/f$ block offsets.

background

The module imports the Periodic Table Engine, whose doc-comment states it supplies an 'Octave ↔ eight-tick mapping for chemistry: φ-tier rails with a fixed set of block offsets (s/p/d/f) and an eight-window neutrality predicate used to detect rests (noble-gas closures)'. It also imports Constants, which fixes the RS time quantum $ au_0 = 1$ tick. These supply the only upstream structure; the module itself adds no new axioms.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the concrete ferromagnetic predicates that later chemistry results would invoke. It sits downstream of the PeriodicTable engine and therefore inherits the T7 eight-tick octave and the zero-parameter neutrality predicate. No parent theorems are listed in the used-by graph.

scope and limits

Does not derive Curie temperatures from the mass formula or $ au_0$.
Does not prove the Stoner criterion; only states it for listed elements.
Does not extend beyond the three classical ferromagnets and rare-earth cases.
Does not connect to Berry creation threshold or dream fraction.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Chemistry.PeriodicTable module_import
IndisputableMonolith.Constants module_import

declarations in this module (27)

def ferromagneticElements L55
def rareEarthFerromagnets L58
def isFerromagnetic L61
theorem iron_ferromagnetic L65
theorem cobalt_ferromagnetic L68
theorem nickel_ferromagnetic L71
def curieTemperature L76
theorem fe_curie_temp L84
theorem co_highest_curie L87
def stonerCriterion L97
def stonerI_Fe L100
def dos_Fe L103
theorem fe_stoner_satisfied L106
def saturationMoment L113
theorem fe_higher_moment_than_ni L121
theorem gd_highest_moment L127
def exchangeJ L135
theorem ferromagnet_positive_J L142
def domainWallWidth L150
def domainWallEnergy L157
theorem co_high_anisotropy L164
def magnetizationRatio L173
theorem zero_above_curie L178
theorem nonzero_below_curie L185
theorem ferromagnets_are_3d_metals L204
def curie_ratio_Co_Fe L210
theorem curie_ratio_bounds L216