cert
plain-language theorem explainer
Packages three local lemmas into a single SolarConstantCert record: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the φ-ladder placement of the solar constant (rung 15, ≈1364 W/m²) uses this certificate as the structural witness. The body is a pure field assembly, no new reasoning.
Claim. There exists 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
The module places the solar constant $S_0 \approx 1361,\mathrm{W/m^2}$ on the Recognition Science $\varphi$-ladder. In SI units one has $\varphi^{15}\approx 1364$, so $S_0$ sits at rung 15; the classical expression $S_0=\sigma_{\mathrm{SB}}T_{\mathrm{sun}}^4(R_{\mathrm{sun}}/\mathrm{AU})^2$ is treated as the physical reading of that rung.
Domain cost is the local cost functional on pairs of positive reals used to score how far a measured quantity sits from a ladder identity. The certificate structure demands three properties of that cost and of a fixed positive threshold: vanishing on the diagonal (exact match costs nothing), nonnegativity off-diagonal, and a strictly positive acceptance threshold.
Upstream, nonnegativity of recognition cost is already forced in ObserverForcing via $J$-cost nonnegativity for any recognition event with positive state.
proof idea
One-line structure inhabitant. Each of the three fields is filled by a preexisting in-module lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No tactics or algebraic work occur in the body.
why it matters
Gives the module its structural certificate that the solar-constant claim is well-formed under the RS cost axioms. The parent module is marked STRUCTURAL THEOREM (0 sorry, 0 axiom) and ties $S_0$ to rung 15 of the $\varphi$-ladder, consistent with the forcing chain that fixes $\varphi$ as the self-similar scale (T6) and the mass/yardstick ladder used elsewhere in RS. No downstream consumers are recorded yet; the immediate sibling cert_inhabited is the natural next witness that the type is nonempty. Closes the local packaging step so later physics pages can cite a single named certificate rather than three scattered lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.