RSAstro004Cert
plain-language theorem explainer
Certificate bundle for Astrophysics Module 4 (Jupiter period as a structural phi^5 match). It packages three props: diagonal vanishing of the domain cost, non-negativity of that cost on positive arguments, and positivity of the canonical threshold. Downstream code builds a concrete inhabitant and a Nonempty proof from sibling lemmas. Pure structure definition; no proof body.
Claim. A Module-4 certificate is a record of three statements: (1) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (2) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (3) the canonical threshold is strictly positive.
background
Module 4 is the structural astrophysics claim that Jupiter's orbital period sits near $\varphi^5$ years ($\approx 11.09$ yr versus the observed $\approx 11.86$ yr, about 6.5%). In RS units the same scale appears as $Z_{\mathrm{cf}}=\varphi^5\in(11,12)$. The module imports the global cost layer and Constants.
The certificate talks about a local domainCost on pairs of reals (mass/energy-style arguments in the module's convention) and a positive canonicalThreshold used as the acceptance cutoff for the structural match. Upstream, the foundation lemma cost_nonneg states that every recognition event has nonnegative cost, via nonnegativity of the J-cost $J(x)=(x+x^{-1})/2-1$ for $x>0$. The certificate's nonnegativity field is the domain-level echo of that fact.
proof idea
No proof: this is a structure whose fields are propositions. Inhabitation is deferred to the sibling definition that fills the three fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to the one-line Nonempty theorem that wraps that instance.
why it matters
Gives a single named type for the structural side-conditions of the Jupiter/$\varphi^5$ module so downstream code can demand a complete certificate rather than three loose lemmas. Used by the concrete cert instance and by cert_inhabited, which close the module as a sorry-free structural theorem. Ties the local cost axioms to the global J-cost nonnegativity story and to the RS landmark $Z_{\mathrm{cf}}=\varphi^5$ in $(11,12)$. Does not itself compute the 6.5% period residual; it only standardizes the cost/threshold interface the residual argument sits on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.