RSCOSStructural005Cert
plain-language theorem explainer
Certificate structure bundling three structural facts for cosmology module 5: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is positive. Cosmology and eight-tick auditors cite it as the typed interface for the RS structural claim. No proof body; it is a pure record whose inhabitant is assembled from sibling lemmas.
Claim. A structural certificate for RS cosmology module 5 is a triple of facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_COS_Structural_005 packages the eight-tick structural layer of Recognition cosmology: period $2^D = 8$, one full traversal of the binary recognition lattice (forcing-chain landmark T7). Status is structural theorem, zero sorry and zero axiom.
The certificate refers to a local domain cost on pairs of positive reals (sibling domainCost), built in the style of the RS J-cost $J(x) = (x+x^{-1})/2-1$. Upstream, ObserverForcing records that every recognition-event cost is nonnegative via Jcost_nonneg. The third field is positivity of a canonical threshold used as a comparison scale in the same module.
Together the three fields are the minimal algebraic hygiene needed before any cosmology claim that compares domain costs against a threshold on the eight-tick lattice.
proof idea
No proof: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Downstream, the concrete inhabitant cert fills them by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then wraps that witness as Nonempty.
why it matters
Gives the typed bundle that cert and cert_inhabited discharge, closing the structural interface for cosmology module 5. That module is the eight-tick layer (period $2^D=8$), so the certificate sits on forcing-chain T7 and on the nonnegativity of recognition cost from ObserverForcing. Without a single record of diagonal vanishing, cost positivity, and threshold positivity, later cosmology comparisons against the canonical scale would be ad hoc. No open scaffold remains here: the module claims 0 sorry and 0 axiom once the sibling lemmas inhabit the structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.