SolarConstantCert
plain-language theorem explainer
A certificate packing three structural facts used to place the solar constant on the φ-ladder: the domain cost vanishes on the diagonal, stays non-negative off it for positive arguments, and the canonical threshold is strictly positive. Anyone citing the solar-constant rung placement or the inhabited certificate will use this bundle. It is a pure structure definition; inhabitants are assembled from sibling lemmas.
Claim. A solar-constant certificate is a record of three properties: (i) for every nonzero real $r$, the domain cost of the pair $(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 treats the solar constant $S_0 \approx 1361,\mathrm{W/m^2}$ as a φ-ladder quantity. In RS units one has $\varphi^{14}\approx 843$ and $\varphi^{15}\approx 1364\approx S_0$, so $S_0$ sits at rung 15 when measured in $\mathrm{W/m^2}$. The classical expression $S_0=\sigma_{\mathrm{SB}}T_{\mathrm{sun}}^4(R_{\mathrm{sun}}/\mathrm{AU})^2$ is the physical anchor; the ladder supplies the dimensionless rung.
Domain cost is the local cost functional on pairs of positive reals used in this physics layer (built from the Recognition J-cost). The upstream fact that every recognition-event cost is nonnegative ($0\le e.\mathrm{cost}$ via $J$-cost nonnegativity) is the foundation for the nonnegativity field here. The canonical threshold is the positive cutoff against which the ladder placement is judged.
This structure does not compute $S_0$; it packages the cost and threshold hypotheses that any certificate of the ladder claim must discharge.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. The concrete inhabitant cert fills them by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. Nonemptiness is then immediate from that inhabitant.
why it matters
In the Recognition framework the solar constant is not an independent empirical input; it is identified with rung 15 on the φ-ladder ($\varphi^{15}\approx 1364$). This certificate is the typed interface that makes that identification checkable: diagonal cost zero, off-diagonal cost nonnegative, and a positive threshold.
Downstream, cert assembles a concrete value and cert_inhabited records Nonempty SolarConstantCert, closing the structural theorem status of the module (0 sorry, 0 axiom). Parent consumers are exactly those two declarations in SolarConstantFromPhiLadder.
The construction sits in the physics layer that exports RS-native constants and ladder placements; it does not itself invoke the T0–T8 forcing chain, but it inherits cost nonnegativity from the observer/recognition calculus that those foundations supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.