cert
plain-language theorem explainer
Packages three structural properties of the astrophysics domain cost into one certificate: it vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is positive. Astrophysicists citing the RS eight-tick structural layer point here. The construction is a direct field-by-field assembly of three already-proved lemmas.
Claim. There is a certificate asserting that the domain cost $C$ satisfies $C(r,r)=0$ for every $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
This module is the fifth structural block in the RS astrophysics layer. Its stated setting is the eight-tick octave: one full traversal of the binary recognition lattice with period $2^D=8$ (forcing step T7, with $D=3$ from T8). Status is a structural theorem package with no sorry and no axioms.
The domain cost $C(m,e)$ is the local cost functional on mass-like and energy-like coordinates used in this astrophysics certificate. It is built from the RS J-cost $J(x)=(x+x^{-1})/2-1$, whose non-negativity is the upstream fact cost_nonneg: every recognition event has non-negative cost, since $J$ is non-negative on the positive reals.
The certificate structure bundles three properties: diagonal vanishing ($C(r,r)=0$ for $r\neq 0$), off-diagonal non-negativity for positive arguments, and positivity of a fixed canonical threshold used as a comparison scale in later structural claims.
proof idea
One-line structure construction. Each field of the certificate is filled by a named sibling lemma already proved in the module: diagonal vanishing by the equality lemma for domain cost on equal arguments, non-negativity by the domain-cost non-negativity lemma (itself resting on J-cost non-negativity from ObserverForcing), and threshold positivity by the canonical-threshold positivity lemma. No extra algebra is performed at this site.
why it matters
Gives a single inhabited certificate object for RS astrophysics structural module 5, so downstream code can assume the three cost axioms as a package rather than re-importing them separately. The module doc frames this as part of the eight-tick structural theorem layer (period $2^D=8$), tying the local cost geometry to forcing landmarks T7 and T8.
No downstream dependents are recorded yet (used_by is empty), so the immediate role is packaging and inhabitance: the sibling cert_inhabited and any later astrophysics theorems that need a named witness of diagonal vanishing, cost non-negativity, and a positive threshold can cite this record. It does not itself derive masses, rotation curves, or the alpha band; it only certifies the cost side-conditions those arguments rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.