cert
plain-language theorem explainer
Packages three elementary properties of the cosmology domain cost into a single certificate: diagonal vanishing, non-negativity on positive arguments, and positivity of the canonical threshold. Cosmologists citing the RS count law (seven independent channels from D=3) use this as the structural witness. The body is a pure structure assembly of three already-proved sibling lemmas.
Claim. There exists a certificate asserting: (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
This module records the RS Count Law for cosmology: with spatial dimension $D=3$ forced by the T8 step of the unified forcing chain, the number of independent channels is $2^D-1=7$. The status line marks the module as a structural theorem (zero sorry, zero axiom).
The certificate structure bundles three cost-side facts about a real-valued domain cost on pairs of positive reals. Domain cost is the local cost functional used to score recognition mismatch in this cosmology layer; it inherits non-negativity from the global J-cost (the unique cost solving the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). The upstream result cost_nonneg states that every recognition event has nonnegative cost, via non-negativity of $J$ on positive states.
The three fields are: diagonal vanishing (cost of a matched pair is zero), positivity of cost off the identity for positive arguments, and a strictly positive canonical threshold used as a comparison scale.
proof idea
One-line structure construction. The definition fills the three fields of the certificate structure by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional tactic work or algebraic reduction occurs; the proof obligation is discharged entirely by those prior results.
why it matters
Gives a single named witness that the cost side of the RS Count Law module is well-formed: matched configurations cost nothing, unmatched positive configurations cost at least zero, and the threshold used to gate channels is positive. That is the structural precondition for treating $2^D-1=7$ as an exact channel count forced by $D=3$ (T8), rather than a fitted parameter.
No downstream consumers are recorded yet in the dependency graph; the sibling cert_inhabited is the natural next step that turns this definition into an inhabited-type fact. Within the broader framework it sits under the cosmology structural layer that feeds observer and forcing arguments built on nonnegative J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.