cert
plain-language theorem explainer
Packages three elementary facts about the solar-luminosity domain cost into a single certificate record: the cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Cited by anyone assembling the RS structural theorem for solar effective temperature. Construction is a pure structure literal wiring three already-proved lemmas.
Claim. There exists a certificate asserting: (i) the domain cost satisfies $C(r,r)=0$ for every $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module treats solar luminosity inside Recognition Science. Observationally $L_\odot=3.828\times 10^{26},\mathrm{W}$ and $T_\mathrm{eff}\approx 5778,\mathrm{K}$. RS identifies the effective temperature with a pure power of the golden ratio: $T_\odot=\varphi^{18},\mathrm{K}$, which matches 5778 K exactly. Luminosity itself is not forced as a single $\varphi^k$ wattage (the exponent is intractable), so the module works with a domain cost instead.
domainCost is the local cost functional on pairs of positive reals (mass-like and energy-like coordinates). The certificate structure SolarLumCert demands three properties of that cost: diagonal vanishing, non-negativity, and a positive canonical threshold. Upstream, the foundation lemma cost_nonneg already guarantees that every recognition-event cost is non-negative via the J-cost $J(x)=(x+x^{-1})/2-1$.
proof idea
Pure structure construction. The three fields of SolarLumCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg and canonicalThreshold_pos. No additional tactics or rewriting; the definition is the certificate.
why it matters
Supplies the inhabited certificate that the module status line calls a STRUCTURAL THEOREM (zero sorry, zero axiom). It sits inside the astrophysics layer that realises the $\varphi$-ladder for stellar temperatures, consistent with the forcing chain (T6 forces $\varphi$ as the self-similar fixed point). Downstream the sibling cert_inhabited simply exhibits this value, closing the existence claim for the solar-luminosity certificate. No further parent theorems appear in the dependency graph yet; the record is the terminal packaging step for the solar $T=\varphi^{18}$ identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.