cert
plain-language theorem explainer
Packages three elementary properties of the spin-torque domain cost into a single certificate: cost vanishes on equal nonzero arguments, is nonnegative for positive magnetization and excitation scales, and the canonical recognition threshold is strictly positive. Anyone citing the structural STT-from-J-cost story uses this bundle. The definition is a pure structure inhabitant wiring three already-proved sibling lemmas.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical recognition threshold $\tau$ obeys $\tau>0$.
background
The module treats spin-transfer torque (STT) as a recognition threshold phenomenon: switching occurs when the J-cost carried by the spin current exceeds the magnetization barrier. In RS-native language the critical current density scales as $J_c \sim J(\varphi), e, M_s, t/(\hbar P)$, with $J$ the unique cost forced by the Recognition Composition Law (T5: $J(x)=(x+x^{-1})/2-1$).
Domain cost is the local cost functional on magnetization and excitation scales; the certificate demands it vanish on the diagonal (equal arguments) and stay nonnegative off it. The canonical threshold is the positive scale at which recognition is allowed to flip the magnetic state. Upstream, nonnegativity of recognition cost is already forced globally: every recognition event has cost $\ge 0$ because $J$ itself is nonnegative on the positive reals.
proof idea
One-line structure inhabitant. The three fields of SpinTorqueCert 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 packages those three facts.
why it matters
Gives a single named witness that the cost-and-threshold hypotheses of the STT-from-J-cost structural theorem are inhabited. The module is marked structural (0 sorry, 0 axiom) and sits in the physics layer that connects the forced J-cost (T5) and the golden-ratio fixed point $\varphi$ (T6) to a concrete spintronic observable. Downstream consumers can assume the certificate rather than re-proving diagonal vanishing, nonnegativity, and threshold positivity separately. No parent theorems are yet recorded as users; the certificate is the export surface of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.