cert
plain-language theorem explainer
Certificate packing three structural properties of the domain cost used in the Jupiter-period astrophysics module: diagonal vanishing, non-negativity on positive arguments, and a strictly positive canonical threshold. Cited by anyone assembling the RS structural claim that the phi^5 year scale sits near Jupiter's orbital period. Pure structure inhabitant that wires three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) the domain cost of any nonzero real against itself is zero; (ii) for positive mass and energy arguments the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
RS Astrophysics Module 4 treats the Jupiter orbital period as a structural match to $\varphi^5$ years ($\approx 11.09,\mathrm{yr}$ versus the observed $11.86,\mathrm{yr}$, about $6.5%$ relative error). In the broader framework $\varphi^5$ is the same scale that appears as $Z_{\mathrm{cf}}$ in the band $(11,12)$ and as the RS-native gravitational constant factor.
The certificate is built on a domain cost (a two-argument real cost specialized to this module) together with a positive canonical threshold. The three fields demand: the cost vanishes on the diagonal away from zero, stays nonnegative for positive inputs, and the threshold is positive. Upstream, the foundation result cost_nonneg records that every recognition-event cost is nonnegative via nonnegativity of the $J$-cost on positive states; the module-local nonnegativity lemma is the analogous statement for domainCost.
proof idea
Definitional structure construction, not a tactic proof. The three fields of RSAstro004Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive mass and energy), and canonicalThreshold_pos (strict positivity of the threshold). No further rewriting or case analysis occurs.
why it matters
Gives a single named inhabitant of the module-4 certificate type so downstream astrophysics developments can assume the cost and threshold axioms in one hypothesis rather than three. The module is marked STRUCTURAL (zero sorry, zero axiom) and sits on the $\varphi^5$ year scale that the primer identifies with $Z_{\mathrm{cf}}\in(11,12)$ and with the RS-native $G\sim\varphi^5/\pi$. No used_by edges are recorded yet; the immediate consumer is the sibling inhabitance lemma that exposes this certificate as a plain existence fact. It does not itself close the numerical Jupiter comparison; it only packages the cost-theoretic side conditions that any such comparison must rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.