RSCosmo005Cert
plain-language theorem explainer
A certificate bundle for Cosmology Module 5: the domain cost vanishes on the diagonal, stays non-negative for positive mass/energy arguments, and the canonical threshold is strictly positive. Cosmology auditors cite it as the structural interface that Module 5 must inhabit. It is a plain structure definition; inhabitation is discharged separately by the concrete `cert` witness.
Claim. A certificate for Cosmology Module 5 consists of three facts: (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
Cosmology RS Module 5 records a structural consistency check on the tensor ratio $r = 2/(44\phi^2) \approx 0.0174$, which sits below the Planck bound $0.036$. The module is marked as a structural theorem with no sorry and no axioms.
The certificate packages three elementary cost properties used in that check. The domain cost is the local cost functional on pairs of positive reals (mass/energy-like arguments). Its diagonal vanishing and nonnegativity mirror the global recognition cost: upstream, cost_nonneg states that "the cost of any recognition event is non-negative," via nonnegativity of the J-cost. The canonical threshold is the positive cutoff against which the module's numerical bound is compared.
Together these fields form the Prop-level interface that a concrete witness must satisfy before the module is treated as inhabited.
proof idea
No proof body: this is a structure definition. It declares three fields (diagonal vanishing of domain cost, nonnegativity of domain cost on positive arguments, positivity of the canonical threshold) and nothing more. Inhabitation is supplied downstream by the noncomputable definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Module 5's claim is that the RS tensor ratio $2/(44\phi^2)\approx 0.0174$ is consistent with the Planck upper bound $<0.036$. The certificate is the structural gate for that claim: without diagonal vanishing, nonnegativity, and a positive threshold, the numerical comparison has no certified cost semantics.
Downstream, cert builds an explicit inhabitant by wiring the three sibling lemmas into the fields, and cert_inhabited records Nonempty of the structure. That inhabitation is what lets the module advertise status "STRUCTURAL THEOREM (0 sorry, 0 axiom)."
In the broader RS stack the cost fields sit on the same J-cost foundation used in the forcing chain (T5 J-uniqueness and the Recognition Composition Law). The threshold positivity is the local positivity hinge for the cosmology bound, not a new physical constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.