cert
plain-language theorem explainer
Packages three elementary properties of the magnetic domain cost into a single coercivity certificate: diagonal vanishing, nonnegativity, and a positive canonical threshold. Materials theorists working the φ-ladder soft/hard magnet split would cite it as the structural witness. The body is a pure structure instance wiring three already-proved field lemmas.
Claim. There exists a coercivity certificate: the domain cost vanishes on the diagonal ($C(r,r)=0$ for $r\neq 0$), is nonnegative for positive magnetisation and field arguments, and the canonical threshold is strictly positive.
background
The module treats magnetic coercivity as a Recognition-Science materials claim. Soft magnets sit below ~1 Oe and hard magnets above ~1000 Oe; the empirical hard/soft ratio ~1000 is identified with a 14-rung φ-ladder gap ($\varphi^{14}\approx 843$). Domain cost is the local cost functional on magnetisation and external-field coordinates; the certificate demands it vanish when the two arguments coincide and stay nonnegative off the diagonal.
The structure CoercivityCert is the interface: three propositions (diagonal zero, nonnegativity, positive threshold). Upstream, nonnegativity of recognition cost is already forced by the J-cost minimum (cost_nonneg: cost of any recognition event is nonnegative). The canonical threshold is the positive cutoff separating soft from hard classes on the ladder.
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No new algebra is performed; the definition only assembles those three facts into a single CoercivityCert value.
why it matters
Gives the module a single named witness that the domain-cost side of the coercivity story is in place. The parent narrative is the structural theorem that soft/hard magnetic classes sit a 14-rung φ separation apart (module status: 0 sorry, 0 axiom). That separation is the materials-side echo of the φ-ladder mass formula and of T6 (φ forced as the self-similar fixed point). No downstream consumers are wired yet (used_by empty), so this certificate is presently the terminal packaging step rather than an intermediate lemma. It closes the local interface that any later coercivity-range theorem would inhabit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.