RSAstro008Cert
plain-language theorem explainer
Certificate bundle for Astrophysics Module 8 (solar radius on the phi ladder). It packages three structural facts: the domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is strictly positive. Downstream code cites the inhabited instance to discharge the module's structural obligations. The structure itself is pure data; witnesses are filled by sibling lemmas.
Claim. A certificate for RS Astrophysics Module 8 consists of three properties of the module's domain cost $C$ and canonical threshold $\tau$: (i) $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
Module 8 records the solar-radius match: $\phi^{43},\mathrm{m}\approx 7.0\times 10^8,\mathrm{m}$ versus $R_\odot\approx 6.96\times 10^8,\mathrm{m}$ (about $0.6%$). Status is structural theorem (no sorry, no axiom).
The domain cost is the local J-style cost used inside this astrophysics slice; on equal nonzero arguments it is zero, and it stays nonnegative for positive mass and energy inputs. The canonical threshold is the positive cutoff against which the module's recognition or match criterion is judged.
Upstream, nonnegativity of recognition cost is already forced in the foundation: any recognition event has cost $\ge 0$ via $J$-cost nonnegativity on positive states. The certificate reuses that pattern at the astrophysics layer.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued obligations. The concrete inhabitant cert assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. Inhabitation is then immediate: cert_inhabited is ⟨cert⟩.
why it matters
Gives Module 8 a single named certificate type so the solar-radius structural claim can be discharged uniformly. Downstream, cert builds an instance and cert_inhabited proves Nonempty RSAstro008Cert, closing the module's structural obligation.
In the broader RS ladder, solar radius sits at rung-scale $\phi^{43}$ meters; the certificate does not re-derive the rung, it only packages the cost and threshold hygiene needed for the match to count as structural. Ties to the phi-ladder mass/length yardstick and to foundation cost nonnegativity (J-cost minimum at identity).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.