cert_inhabited
plain-language theorem explainer
The module-12 forcing certificate is inhabited: there exists a bundle asserting diagonal vanishing of domain cost, its nonnegativity on positive arguments, and positivity of the canonical threshold. Anyone assembling the RS structural certificate stack cites this existence fact. The proof is a one-line term that packages the already-built witness.
Claim. The type of certificates whose fields assert (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, is nonempty.
background
Module 12 of the RS foundation forcing chain records the dimensionless identity $J(\varphi)=\varphi-3/2$ (numerically $\approx 0.11803$), treated as a structural theorem with no sorry and no axioms. The local certificate structure packages three elementary cost facts used throughout that module.
Domain cost is the two-argument cost functional on the module (imported from the Cost layer). The certificate demands it vanish on the diagonal for nonzero $r$, stay nonnegative for positive mass and energy arguments, and that the module's canonical threshold be strictly positive. Those three propositions are exactly the fields of the certificate structure.
Upstream, the structure itself is the only dependency: inhabitation is existence of some value of that structure type.
proof idea
One-line term proof. The module already constructs a concrete value cert of type RSForcingChain012Cert. The proof is the standard Nonempty introduction ⟨cert⟩, i.e. package that witness. No tactics, no further lemmas.
why it matters
Closes the existence side of Foundation RS Module 12: once the three cost/threshold facts are proved and bundled into cert, this theorem records that the certificate type is inhabited. Downstream consumers of the forcing-chain certificate stack can therefore assume a module-12 cert without reconstructing the fields. The module sits in the structural layer that supports the broader T0–T8 forcing narrative (J-uniqueness, $\varphi$ fixed point, eight-tick octave, $D=3$), though this particular declaration only certifies the local cost package tied to $J(\varphi)=\varphi-3/2$. No used-by edges are recorded yet; the value is as a stack leaf for later chain assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.