cert
plain-language theorem explainer
Packages the three local lemmas on domain cost vanishing on the diagonal, nonnegativity, and positive canonical threshold into a single magnon-dispersion certificate. Anyone citing the Fe magnon stiffness structural claim would use this inhabitant. The construction is a pure structure instance: each field is filled by the matching sibling lemma.
Claim. There exists a certificate for the second magnon-dispersion package: the domain cost vanishes whenever the two arguments are equal and nonzero, the domain cost is nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive.
background
The module treats ferromagnetic magnon dispersion on the Recognition Science phi-ladder. The target physical scale is the magnon stiffness $D$ in iron ($\sim 370,\mathrm{meV},\mathrm{\AA}^2$), written schematically as $D = J(\phi), k_B T_{\mathrm{Curie}} a^2/\hbar^2$ with $T_{\mathrm{Curie}}=1043,\mathrm{K}$ and $a=2.87,\mathrm{\AA}$, claimed only at order-of-magnitude consistency.
domainCost is the local cost functional on mass/energy pairs; the certificate demands it be zero on the equal-argument diagonal (nonzero $r$) and nonnegative for positive arguments. canonicalThreshold is the positive cutoff used to separate the dispersion regime. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity; the local nonnegativity field is the domain-level analogue of that fact.
proof idea
One-line structure instance. The three fields of MagnonDisp2Cert are filled by the three sibling lemmas already proved in the same module: diagonal vanishing (domainCost_at_eq), domain-cost nonnegativity (domainCost_nonneg), and positivity of the canonical threshold (canonicalThreshold_pos). No further rewriting or case analysis occurs.
why it matters
Gives a single named inhabitant of the magnon-dispersion certificate so downstream physics lemmas can assume the three structural properties as a bundle rather than re-importing each lemma. The module is marked structural (zero sorry, zero axiom) and sits in the physics layer that connects the $J$-cost / phi-ladder apparatus to condensed-matter scales. No parent theorems currently depend on this certificate in the graph; it is the ready-to-cite package for the Fe stiffness claim in Plan v7. Framework landmarks in play are the $J$-cost (T5) and the phi fixed point (T6) that enter the stiffness formula, not the eight-tick or $D=3$ forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.