cert
plain-language theorem explainer
Packages the three structural properties of the astrophysics domain cost at recognition rung 61: diagonal vanishing, non-negativity on positive arguments, and a strictly positive canonical threshold. Cited by anyone invoking the structural astrophysics certificate for rung 61. Proof is a structure instance that wires three already-established lemmas.
Claim. There exists a structural certificate for the astrophysics domain at recognition rung 61: the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, $C(m,e)\geq 0$ whenever $m>0$ and $e>0$, and the canonical threshold $T$ obeys $T>0$.
background
This module records the structural Recognition Science prediction for the astrophysics domain at recognition rung 61. Status is a structural theorem with zero sorry and zero axioms.
The certificate structure demands three properties of the domain cost $C$: (i) it vanishes on the diagonal away from zero, (ii) it is non-negative for positive mass and energy arguments, and (iii) the associated canonical threshold is strictly positive. Non-negativity of recognition cost is the standard J-cost fact from ObserverForcing: every recognition event has cost at least zero, since $J$ is minimized at the identity.
Domain cost here is the local cost functional for the astrophysics sector; the canonical threshold is the positive cutoff used to separate structural regimes on the phi-ladder at this rung.
proof idea
One-line structure instance. The three fields of StructAstrophysicsM61Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No additional reasoning is performed at this site.
why it matters
This is the inhabited structural certificate for astrophysics at rung 61 in the Plan v7 structural series. It closes the packaging step so downstream work can treat the three cost axioms as a single named object rather than three free-floating lemmas.
In the broader RS framework it sits in the astrophysics domain layer above the J-cost and forcing chain (T5 J-uniqueness, T6 phi fixed point). The certificate itself does not yet feed a named parent theorem in the dependency graph (used_by is empty), but it is the natural handle for any later mass-ladder or structural-prediction statement that needs the rung-61 astrophysics cost axioms in one place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.