cert_inhabited
plain-language theorem explainer
The RS cosmology structural certificate for module 5 is nonempty: there is a packed witness that domain cost vanishes on equal positive arguments, stays nonnegative off the diagonal, and the canonical threshold is strictly positive. Cosmology and eight-tick lattice arguments cite it to discharge the structural interface in one step. The proof is a one-line term that exhibits the prebuilt certificate record.
Claim. The type of structural certificates is inhabited: there exists a record 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) the canonical threshold is strictly positive.
background
Module RS_COS_Structural_005 is a zero-sorry structural layer for Recognition Science cosmology. Its setting is the eight-tick octave: one full traversal of the binary recognition lattice has period $2^D=8$, matching the T7 forcing step that locks the discrete clock to three spatial bits.
The certificate structure bundles three elementary facts about a domain cost (imported from the Cost layer) and a positive canonical threshold. Domain cost is the local mismatch functional on mass/energy-like pairs; the diagonal identity says equal nonzero arguments incur zero cost, nonnegativity keeps the functional a genuine cost, and threshold positivity supplies a strict cutoff used by later selection or stability arguments.
Upstream, the structure itself only declares the three propositions; the sibling certificate value assembles the proved instances of those propositions into one record.
proof idea
Term-mode one-liner. The goal is Nonempty of the certificate structure; the proof supplies the already-constructed sibling certificate as the witness via the standard angle-bracket introduction. No further rewriting or case analysis is required.
why it matters
This inhabitation lemma closes the structural interface for Cosmology module 5 so downstream developments can assume a single packed certificate rather than three separate lemmas. It sits inside the eight-tick story (T7: period $2^3=8$), the discrete recognition lattice that underwrites RS cosmology timing and octave structure. With zero sorry and zero axioms in the module, it is a clean structural theorem rather than a hypothesis stub. No used-by edges are recorded yet; the natural consumers are any cosmology theorems that need the domain-cost diagonal, nonnegativity, and positive threshold in one hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.