cert
plain-language theorem explainer
Packages the three structural obligations of the first RS astrophysics certificate: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is strictly positive. Anyone citing the solar-surface module (phi^18 K = 5778 K) uses this bundle as the inhabited witness. The definition is a pure structure assembly of three sibling lemmas.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module RS_Astro_Module_001 is the first astrophysics structural theorem in the Recognition Science mirror. Its headline claim is that the solar surface temperature equals $\phi^{18}$ kelvin, matching the PDG value 5778 K exactly, with zero sorry and zero axiom.
The certificate structure collects three cost-side obligations used throughout the module. Domain cost is the local cost functional on mass/energy pairs; the diagonal vanishing condition says a matched pair carries zero cost, and nonnegativity says the cost never goes negative for positive arguments. The canonical threshold is the positive cutoff against which domain comparisons are judged.
Upstream, nonnegativity of recognition cost is already forced in ObserverForcing: every recognition event has cost $\ge 0$ via the J-cost minimum. The present certificate specialises that discipline to the astrophysics domain cost and adds the diagonal and threshold facts.
proof idea
One-line structure inhabitant. Each field is filled by the corresponding sibling lemma already proved in the same module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and positivity of the threshold by canonicalThreshold_pos. No extra tactics or algebraic work.
why it matters
This is the inhabited witness that the solar-surface module meets its structural cost interface. Downstream consumers (none yet linked in the graph) can assume the three fields without re-proving them. In the broader RS chain it sits under the J-cost uniqueness (T5) and the phi-ladder mass/temperature bookkeeping: temperatures are read as rung powers of $\phi$, here rung 18 for the solar photosphere. It closes the certificate side of a zero-sorry structural theorem rather than deriving the temperature formula from first principles in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.