cert
plain-language theorem explainer
Packages the three witnesses that form the magnon-dispersion certificate on the φ-recognition lattice: diagonal vanishing of domain cost, nonnegativity of domain cost, and positivity of the canonical threshold. Anyone citing the structural magnon result (zone-boundary gap = φ) needs this inhabited certificate. The body is a pure structure assembly from three already-proved sibling lemmas.
Claim. There is a magnon-dispersion certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module treats magnon dispersion for the canonical Heisenberg ferromagnet on the φ-recognition lattice. Classically the zone-boundary energy is $E_{ZB}=2JS(1-\cos\pi)=4JS$; Recognition Science identifies the zone-boundary / spin-wave gap with $\varphi$.
The certificate structure demands three properties of the local domain cost (the J-cost pulled back to mass/energy coordinates on the φ-ladder): it vanishes on the diagonal away from zero, it is nonnegative for positive arguments, and the canonical threshold used to mark the gap is positive. Upstream, nonnegativity of recognition cost is already forced by $J$-cost nonnegativity on positive states.
Sibling lemmas supply exactly those three facts; this definition only names the resulting package.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive mass and energy), and canonicalThreshold_pos (strict positivity of the threshold). No further rewriting or case analysis occurs.
why it matters
Gives an inhabited certificate object for the structural magnon theorem of the module: zone-boundary spin-wave gap equals $\varphi$ on the φ-recognition lattice. That identification sits on the φ-ladder mass/energy bookkeeping (primer: T6 φ fixed point, mass formula on the φ-ladder) and on the nonnegativity of J-cost (T5 uniqueness of $J$). With zero sorry and zero axioms in the module, this definition closes the certificate side of the structural claim. No downstream users are recorded yet; the natural consumer is any theorem that assumes an inhabited magnon-dispersion certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.