cert_inhabited
plain-language theorem explainer
The structural certificate for RS cosmology module 3 is inhabited: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Cosmology auditors cite this to discharge Nonempty obligations on the RS count-law package (2^D-1=7 from D=3). Proof is a one-line term witness packing the concrete cert.
Claim. The type of certificates packing (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) positivity of the canonical threshold, is nonempty.
background
Module RS_COS_Structural_003 packages the RS Count Law: $2^D-1=7$ independent channels, exact once configuration dimension is $D=3$. Status is structural (zero sorry, zero axiom). The local cost is the domain cost on positive reals; the certificate structure bundles three elementary facts about it and about a fixed positive threshold.
RSCOSStructural003Cert requires: domain cost vanishes when the two arguments agree and are nonzero; domain cost is nonnegative for positive arguments; and the canonical threshold is strictly positive. Those three fields are the only content of the certificate. Upstream, the structure itself is the sole dependency of this theorem.
proof idea
One-line term proof. The module already defines a concrete value cert : RSCOSStructural003Cert. The theorem is ⟨cert⟩, i.e. the standard introduction rule for Nonempty, witnessing inhabitance by that value. No tactics, no further lemmas.
why it matters
Closes the inhabitance obligation for the structural certificate of cosmology module 3. The module doc ties the package to the RS Count Law $2^D-1=7$, which is exact once $D=3$ is forced (forcing-chain landmark T8). Downstream use list is empty in the graph, so this is a terminal inhabitance lemma for the cert bundle rather than a stepping stone into a larger named theorem. It does not itself derive the channel count; it only certifies that the cost/threshold side conditions are realized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.