StructAstrophysicsM81Cert
plain-language theorem explainer
Packages three structural axioms for the astrophysics domain at recognition rung 81: diagonal domain-cost vanishes, cost is nonnegative off the axes, and the canonical threshold is positive. Downstream code cites the inhabited instance as the RS structural certificate for this domain. Pure structure definition; no proof body.
Claim. A structural astrophysics certificate at rung 81 is a record of three facts: for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; for all positive $m,e$, one has $C(m,e)\ge 0$; and the canonical threshold $T$ obeys $T>0$.
background
Recognition Science assigns each physical domain a rung on the $\varphi$-ladder and a domain cost built from the universal $J$-cost $J(x)=(x+x^{-1})/2-1$. The module states a structural RS prediction for the astrophysics domain at recognition rung 81, with status structural theorem (zero sorry, zero axiom).
Here domainCost is the real bivariate cost used for that domain; the diagonal identity $C(r,r)=0$ encodes perfect self-match, while nonnegativity for positive arguments mirrors the global fact that every recognition event has nonnegative cost (ObserverForcing cost_nonneg, via $J\ge 0$). The canonical threshold is the positive cutoff against which domain residuals are compared.
The structure simply names the three Prop fields that any valid certificate must supply.
proof idea
No proof: this is a structure declaration. The three fields are pure propositions (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Inhabitation is deferred to the sibling definition cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the typed interface for the rung-81 astrophysics structural certificate in the Plan v7 structural-pass series. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty StructAstrophysicsM81Cert, so later modules can assume the package without re-proving the three axioms.
In the broader RS forcing chain the nonnegativity field is the domain-level echo of $J$-cost nonnegativity (T5 uniqueness of $J$), while the positive threshold is the gate used when comparing residuals to the Berry-scale and $\varphi$-ladder mass formula. The certificate does not itself compute masses or rotation curves; it only locks the structural hypotheses those predictions rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.