cert
plain-language theorem explainer
Bundled certificate that the astrophysical domain cost vanishes on the diagonal, is nonnegative for positive arguments, and that the canonical threshold is strictly positive. Structural-layer authors cite it whenever a single witness of cost well-formedness is required. The definition only assembles three already-proved sibling lemmas into the certificate structure.
Claim. A structural certificate asserting: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
Astrophysics Structural Module 9 sits on the RS forcing chain T5 (J-uniqueness) through T8 ($D=3$), and is marked as a structural theorem with zero sorry and zero axioms. The local object of study is a domain-level cost, the natural specialization of the Recognition Science J-cost $J(x)=(x+x^{-1})/2-1$, which measures departure from the identity recognition event at $x=1$.
The certificate structure packages three elementary properties any such cost must satisfy before it can underwrite structural claims: diagonal vanishing (a perfect match costs nothing), nonnegativity on the positive orthant, and a strictly positive decision threshold. Upstream, the foundation result that every recognition-event cost is nonnegative (via nonnegativity of $J$) supplies the conceptual precedent for the domain-level nonnegativity field.
proof idea
Definitional packing of a structure instance. The three fields are filled directly by the sibling lemmas establishing diagonal vanishing of the domain cost, its nonnegativity for positive mass and energy arguments, and strict positivity of the canonical threshold. No further algebraic work occurs; the declaration is a pure witness assembly.
why it matters
This is the packaged witness for Structural Module 9 in the astrophysics layer. The module rides the forcing chain from T5 J-uniqueness and T6 phi-forcing through the eight-tick octave (T7) and $D=3$ (T8), and is recorded as a structural theorem with no sorry and no axioms. No downstream consumers appear in the current graph, yet the certificate is the natural single-hypothesis handle for any later result that needs domain-cost well-formedness. It closes the local interface by exhibiting an inhabited certificate rather than leaving the three properties unbundled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.