cert
plain-language theorem explainer
Packages the three structural axioms for the astrophysics domain at recognition rung 71 into a single certificate: the domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the mod-71 structural prediction uses this bundle. The construction is a pure record assembly from three already-proved sibling lemmas.
Claim. There exists a structural certificate for the astrophysics domain at rung 71 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.
background
Module status is a structural theorem (zero sorry, zero axiom) giving the Recognition Science prediction for the astrophysics domain at recognition rung 71. The certificate type is a three-field structure: diagonal vanishing of the domain cost, nonnegativity of that cost on the positive quadrant, and positivity of a canonical threshold.
Domain cost is the local cost functional on mass-energy pairs in this module; its diagonal vanishing and nonnegativity are sibling facts assembled here. Nonnegativity of recognition cost is the standard J-cost property from ObserverForcing: the cost of any recognition event is nonnegative, since $J$ is nonnegative on the positive reals. The canonical threshold is the positive cutoff against which domain cost is compared in the structural prediction.
proof idea
One-line record construction. The three fields of the certificate structure are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional reasoning occurs at this site.
why it matters
This is the inhabited certificate object for Structural Certificate 71 in the astrophysics lane of the Plan v7 structural pass. Downstream consumers that need a single term of type StructAstrophysicsM71Cert (for example the companion inhabitedness fact in the same module) point here rather than re-proving the three field obligations. It sits in the astrophysics domain layer, not in the T0-T8 forcing chain itself; it records that the J-cost-style domain functional at rung 71 meets the structural checklist (zero on match, nonnegative, positive threshold) required for RS structural predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.