cert
plain-language theorem explainer
Packages the three structural facts needed for the solar-radius RS certificate: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is positive. Anyone citing the Module-8 solar match (φ⁴³ m ≈ R_☉) uses this inhabitant. The body is a pure structure assembly of three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 8 records the solar-radius match in Recognition Science units: $\varphi^{43},\mathrm{m} \approx 7.0\times 10^8,\mathrm{m}$ against $R_\odot = 6.96\times 10^8,\mathrm{m}$ (about $0.6%$ relative error), marked as a structural theorem with no sorry and no axioms.
The certificate structure bundles three cost-side obligations. Domain cost is the local cost functional on pairs of positive reals (mass/energy style arguments); it is required to vanish when the two arguments coincide and to stay nonnegative off the diagonal. The canonical threshold is the positive cutoff against which that cost is compared in the module's matching criterion.
Upstream, nonnegativity of recognition cost is the standard J-cost fact: every recognition event has cost $J(x)\ge 0$ for $x>0$, with minimum at the identity $x=1$. The module imports that foundation and specializes it to the astrophysical domain cost.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra is performed at this site.
why it matters
Gives a single named witness that Module 8's cost interface is fully discharged, so the solar-radius $\varphi$-ladder claim can be treated as a closed structural theorem. In the broader RS chain this sits downstream of T5 J-uniqueness and the nonnegative J-cost calculus, and on the astrophysics side it is the packaging step for the $\varphi^{43}$ yardstick match to $R_\odot$. No further used-by edges are recorded yet; the immediate consumer is the module's own inhabitedness fact for the certificate type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.