cert
plain-language theorem explainer
Packages three structural facts about the cosmology domain cost and its threshold into a single certificate for RS Cosmology Module 5. Anyone citing the module's r-tensor consistency (2/(44 φ²) ≈ 0.0174 below the Planck bound 0.036) can point here. The definition is a pure structure inhabitant: three already-proved lemmas are plugged into the certificate fields.
Claim. There is a 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 arguments; (iii) the canonical threshold is strictly positive.
background
RS Cosmology Module 5 records a structural consistency check on an r-tensor value $2/(44\varphi^2)\approx 0.0174$, which sits below the Planck bound $0.036$. The module is marked free of sorry and axioms.
The certificate type bundles three properties of a real-valued domain cost on pairs $(m,e)$ and of a fixed positive threshold. Diagonal vanishing says equal mass and energy arguments incur zero cost. Nonnegativity for positive inputs is the local form of the global recognition-cost law (upstream: cost of any recognition event is nonnegative, via $J$-cost nonnegativity). The threshold positivity field simply records that the module's cutoff is a genuine positive scale.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge those three fields; this definition only assembles them.
proof idea
One-line structure construction. The three fields of RSCosmo005Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra reasoning: the certificate is the tuple of those proofs.
why it matters
Gives a single named inhabitant that Module 5's structural theorem can hand to downstream cosmology checks. The module doc frames the content as an r-tensor consistency result against the Planck bound, inside the RS forcing chain where $\varphi$ is already fixed (T6) and the $J$-cost is unique (T5). With used_by empty in the graph, this is presently a leaf certificate: it closes the module's local obligations rather than feeding a larger named theorem. It touches no open scaffold; status is definitional packaging of proved facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.