cert_inhabited
plain-language theorem explainer
The Module-7 certificate type is inhabited: there exists a package of the domain-cost diagonal vanishing, nonnegativity, and positive canonical threshold. Anyone assembling the RS count-law forcing step at D=3 cites this existence fact. The proof is a one-line term that supplies the concrete certificate value.
Claim. There exists a certificate packing three facts: the domain cost vanishes on the diagonal ($C(r,r)=0$ for $r\neq 0$), the domain cost is nonnegative for positive arguments, and the canonical threshold is strictly positive.
background
Foundation Module 7 records the RS count law: at spatial dimension $D=3$, there are exactly $2^D-1=7$ independent observable categories. The module is marked structural (zero sorry, zero axiom).
The certificate structure bundles three elementary properties of the local domain cost $C$ and a positive threshold constant used in the count-law argument: diagonal vanishing $C(r,r)=0$ off zero, nonnegativity for positive mass and energy arguments, and positivity of the canonical threshold. These are the algebraic side-conditions needed before the combinatorial count $2^3-1=7$ is treated as forced.
Upstream, the structure itself is the sole dependency; the concrete witness cert is a sibling that already fills the three fields.
proof idea
One-line term proof. Nonemptiness of the certificate structure is witnessed by the already-constructed sibling value that supplies the three field proofs (diagonal cost identity, cost nonnegativity, threshold positivity). No further tactics or lemmas are invoked.
why it matters
This existence lemma closes the certificate interface for Module 7 of the RS forcing chain. The parent setting is the count law $2^D-1=7$ at $D=3$, which sits at the T8 landmark (three spatial dimensions forced) and the T7 eight-tick octave (period $2^3$). Downstream edges are empty in the current graph, so the declaration is a leaf that makes the structural theorem exportable as a nonempty Prop package rather than three loose lemmas.
In the broader chain (T0–T8), having an inhabited certificate means later modules can assume the domain-cost hygiene and positive threshold without re-proving them. No open scaffolding remains here: status is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.