RSCOSStructural003Cert
plain-language theorem explainer
Certificate structure bundling three structural properties used by the RS cosmology count-law module: diagonal domain cost vanishes, domain cost is nonnegative on positive arguments, and the canonical threshold is positive. Cosmology auditors cite it as the interface that the concrete certificate and its nonempty witness inhabit. Pure Prop bundle with no proof body.
Claim. A certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_COS_Structural_003 packages the RS Count Law in cosmology: with spatial dimension $D=3$ forced upstream, one has $2^D-1=7$ independent channels. Status is structural (zero sorry, zero axiom). The local cost object is a real bivariate domain cost imported from the Cost layer; the canonical threshold is a fixed positive scale against which domain costs are compared.
Nonnegativity of recognition cost is already standard in the foundation: any recognition event has nonnegative cost, via nonnegativity of the J-cost on positive states. The certificate rephrases the same positivity discipline at the cosmology domain-cost interface, plus a diagonal vanishing condition (matched measure and expectation give zero cost) and positivity of the threshold.
Sibling lemmas in the module discharge each field: diagonal identity, domain-cost nonnegativity for positive arguments, and strict positivity of the canonical threshold.
proof idea
No proof body: this is a structure declaration whose fields are propositions. Inhabitation is deferred to the sibling definition that fills the three fields with the corresponding lemmas (diagonal vanishing, domain-cost nonnegativity, threshold positivity), and to the one-line nonempty witness built from that inhabitant.
why it matters
Gives the typed interface for Structural Module 3 of RS cosmology. Downstream, the concrete certificate definition assembles the three sibling lemmas into one value of this structure, and the nonempty theorem records that the certificate type is inhabited. That closes the structural claim that the count-law module is fully certified with zero sorry.
In the broader framework this sits under the $D=3$ forcing (T8) and the eight-tick octave (T7): the count $2^D-1=7$ is exact once configuration dimension is three. The cost fields keep the cosmology layer aligned with the global J-cost nonnegativity and identity-minimum discipline from ObserverForcing, so channel counting does not float free of the recognition cost calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.