cert
plain-language theorem explainer
Packages three structural facts about the domain cost and canonical threshold into a single CMB-temperature certificate. Cosmologists citing the phi-ladder derivation of T_CMB ≈ 2.73 K use this witness. The definition is a pure record assembly: it wires three already-proved sibling lemmas into the certificate fields.
Claim. There exists a certificate asserting: (i) the domain cost vanishes on the diagonal, $\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
The module derives the CMB temperature from the Recognition Science phi-ladder. In RS-native units one has $T_{\mathrm{CMB}}/T_{\mathrm{vac}}=\varphi^{-k}$; with $T_{\mathrm{vac}}=kT_{\mathrm{Planck}}\approx 1.4\times 10^{32},\mathrm{K}$ and rung $k=196$ this yields $T_{\mathrm{CMB}}\approx 2.73,\mathrm{K}$, matching the observed $2.725,\mathrm{K}$. The status is structural: zero sorry, zero axioms.
The certificate structure bundles three properties of a domain cost built from the J-cost $J(x)=(x+x^{-1})/2-1$ (the unique cost forced by the Recognition Composition Law). Upstream, nonnegativity of recognition-event cost is already known: any recognition event has cost $\ge 0$ because $J$ is nonnegative on the positive reals. The siblings domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos specialize that fact to the cosmology domain cost and assert positivity of the threshold used in the temperature matching.
proof idea
One-line record construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive measure and expectation), and canonicalThreshold_pos (strict positivity of the canonical threshold). No additional reasoning occurs at this site.
why it matters
This certificate is the structural witness that the domain-cost side conditions needed for the phi-ladder CMB temperature argument hold. The module frames the result as a structural theorem linking $T_{\mathrm{CMB}}$ to $\varphi^{-196}$ against the Planck vacuum temperature. It sits downstream of the J-cost nonnegativity fact from ObserverForcing and of the T5 uniqueness of $J$ in the forcing chain. No further used-by edges are recorded yet; the certificate is the local packaging step that later cosmology lemmas can consume when they invoke the temperature identity. It does not itself compute the numerical Kelvin value; it only certifies the cost-theoretic hypotheses of that derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.