cert
plain-language theorem explainer
Packages the three structural facts of the magnetar-field module into one certificate: the domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the module's STRUCTURAL status for the phi^{72} Gauss magnetar scale uses this bundle. The definition is a pure field-wise assembly of three sibling lemmas.
Claim. There is a 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. Together these witness the structural claims of the magnetar-field module.
background
Module 11 is the Recognition Science structural account of the magnetar surface field scale $\phi^{72},\mathrm{G}\sim 10^{14},\mathrm{G}$. Status is STRUCTURAL THEOREM: zero sorry, zero axiom.
The local cost is a domain-level specialization of the Recognition J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). Sibling facts record that this cost is zero when model and evidence coincide off zero, and nonnegative on the positive orthant. The canonical threshold is the positive cutoff against which that cost is compared.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: every recognition event has $0\le e.\mathrm{cost}$, via $J$-cost nonnegativity on positive states. The certificate structure simply names the three Prop fields a consumer must discharge.
proof idea
One-line structure instance. The three fields of RSAstro011Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra algebra or case analysis occurs at this site; the work lives in those three lemmas (the middle one ultimately resting on foundation-level $J$-cost nonnegativity).
why it matters
Gives a single named inhabitant of the module certificate so downstream astrophysics code can assume the magnetar structural package without re-proving diagonal vanishing, nonnegativity, and threshold positivity. The module doc pins the physical claim: magnetar field $\phi^{72}$ Gauss, of order $10^{14}$ Gauss, as a STRUCTURAL THEOREM in the RS ladder. That scale sits on the same $\phi$-ladder used for mass rungs and the eight-tick octave (T6--T7). No used-by edges are recorded yet; the immediate sibling cert_inhabited is the natural consumer. Does not itself compute the numerical Gauss value; it certifies the cost/threshold scaffolding around that claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.