module module moderate

`IndisputableMonolith.Chemistry.Ferromagnetism`

This module enumerates the elements that exhibit ferromagnetism at room temperature inside the Recognition Science chemistry scaffold. Condensed-matter physicists would cite it when mapping magnetic behavior onto the phi-tier rails without per-element tuning. The module consists entirely of definitions that apply the eight-tick octave structure imported from PeriodicTable to identify Fe, Co, Ni and selected rare-earth cases.

claimThe set of room-temperature ferromagnetic elements is the collection $F$ of transition metals and rare earths whose positions on the eight-tick phi-ladder satisfy the Stoner criterion and the neutrality predicate for d-block occupancy.

background

The module imports the Periodic Table Engine, which supplies an octave-to-eight-tick mapping for chemistry via phi-tier rails, fixed s/p/d/f block offsets, and an eight-window neutrality predicate that detects noble-gas closures. It also imports the RS time quantum tau_0 = 1 tick from Constants. These primitives are used to classify ferromagnetism by rung and gap without introducing free parameters or dataset fits.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete chemical realizations needed for magnetic phenomena inside the Recognition Science framework. It feeds the overall chemistry layer that connects to the J-uniqueness and phi-ladder constructions upstream, placing room-temperature ferromagnets on the T0-T8 forcing chain. No downstream theorems are recorded yet.

scope and limits

Does not derive the microscopic exchange interaction from the Recognition Composition Law.
Does not compute numerical Curie temperatures or temperature dependence.
Does not include external-field or domain-structure effects.
Does not bind to or validate against experimental datasets.

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