cert
plain-language theorem explainer
Packages three elementary facts about the cosmology domain cost and its threshold into a single structural certificate for RS Cosmology module 10. Anyone citing the module's parameter-free calibration after fixing E_coh from the electron mass would point here. The definition is a pure structure assembly: it wires three already-proved sibling lemmas into the certificate fields.
Claim. There is a structural certificate asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and energy arguments; (iii) the canonical threshold is strictly positive.
background
Module 10 of the RS cosmology structural series fixes the coherence energy $E_{\mathrm{coh}}$ once from the electron mass and then treats all further predictions as parameter-free. The local certificate type records three minimal analytic properties that any admissible domain cost must satisfy before those predictions are trusted.
The domain cost is the recognition cost specialized to cosmology mass/energy pairs. It inherits nonnegativity from the underlying $J$-cost on recognition events: the upstream result states that "the cost of any recognition event is non-negative," via $J$-cost nonnegativity at positive state. The diagonal vanishing condition encodes that matched mass and energy incur zero excess cost. The canonical threshold is the positive cutoff used to separate structural regimes in the same module.
Sibling lemmas already establish each of the three fields separately (domainCost at equal arguments is zero, domain cost is nonnegative on the positive orthant, and the canonical threshold is positive).
proof idea
One-line structure construction. The three certificate fields are filled by direct assignment to the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional rewriting or case analysis occurs; the definition is pure packaging of those three results into RSCOSStructural010Cert.
why it matters
Gives the inhabited structural certificate that module 10 advertises as a zero-sorry, zero-axiom theorem package. Downstream consumers (none yet wired in the graph) can assume a single object rather than three separate lemmas when arguing that cosmology predictions remain parameter-free after $E_{\mathrm{coh}}$ is fixed by the electron mass.
In the broader Recognition framework this sits on the cost side of the forcing chain: nonnegativity traces to $J$-cost uniqueness (T5) and the recognition composition law, while the positive threshold is the local gate that keeps structural comparisons well-defined. It does not itself derive masses, the eight-tick octave, or $D=3$; it only certifies the cost infrastructure those later cosmology claims need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.