CMBTemp3v2Cert
plain-language theorem explainer
Certificate packing three structural hypotheses used in the phi-ladder CMB temperature argument: diagonal domain cost vanishes, domain cost is nonnegative on positive mass/energy, and the canonical threshold is positive. Cosmology code cites it via the concrete inhabitant `cert` and the nonemptiness lemma. Pure structure definition; no proof body.
Claim. A CMB-temperature certificate is a triple of facts: (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 treats CMB temperature as a structural consequence of the Recognition Science phi-ladder: $T_{\mathrm{CMB}}/T_{\mathrm{vac}}=\varphi^{-k}$ with $T_{\mathrm{vac}}$ at the Planck thermal scale and $k=196$, giving $T_{\mathrm{CMB}}\approx 2.73,\mathrm{K}$ against the observed $2.725,\mathrm{K}$. Status is structural (zero sorry, zero axiom).
Domain cost is the local cost functional on mass/energy pairs that the certificate constrains; the sibling lemmas assert it vanishes on the diagonal and is nonnegative off it. The canonical threshold is the positive scale cut used when matching the ladder rung to temperature. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative because $J$-cost is nonnegative on positive states.
proof idea
No proof: this is a structure whose three fields are propositions. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The nonemptiness theorem is then the trivial constructor application ⟨cert⟩.
why it matters
Gives a named interface for the three cost/threshold facts the CMB-from-J-cost story needs, so downstream code can depend on a single certificate type rather than three free-floating lemmas. Immediate consumers are the concrete certificate and the theorem that the type is inhabited. In the broader RS chain this sits under the cosmology layer that reads temperatures off the phi-ladder (T5–T6 force $J$ and $\varphi$; the eight-tick and $D=3$ steps are upstream geometry). It does not itself compute $2.725,\mathrm{K}$; it only packages the structural side conditions the numerical claim relies on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.