cert_inhabited
plain-language theorem explainer
The module-10 forcing-chain certificate is inhabited: there is a packed witness that domain cost vanishes on the diagonal, is nonnegative for positive arguments, and that the canonical threshold is positive. Calibration and structural-forcing arguments cite this for existence of the bundle. The proof is a one-line term that feeds the prebuilt certificate into Nonempty.
Claim. The type of module-10 RS forcing certificates is nonempty: 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 10 of the RS forcing chain is a structural calibration layer: $E_{\mathrm{coh}}$ is treated as the single free parameter, fixed by the electron mass at rung 3. Status is a structural theorem (zero sorry, zero axioms).
The certificate structure bundles three elementary facts about the local cost geometry. Domain cost is the two-argument cost on the recognition domain (imported from the Cost layer). The first field asserts it vanishes on the diagonal for nonzero scale; the second that it is nonnegative for positive mass and energy arguments; the third that the module's canonical threshold is strictly positive.
Those three properties are already proved as sibling lemmas (domainCost_at_eq, domainCost_nonneg, canonicalThreshold_pos) and assembled into a concrete certificate value; this theorem only records that the certificate type is inhabited.
proof idea
One-line term proof. Nonempty is introduced by the anonymous constructor applied to the prebuilt certificate value cert, which already inhabits RSForcingChain010Cert. No tactics, no further lemmas.
why it matters
Gives a single inhabited certificate object for the module-10 structural facts, so downstream forcing or calibration code can depend on one Nonempty hypothesis rather than three separate lemmas. The module doc frames this as part of the RS calibration story in which $E_{\mathrm{coh}}$ is the sole free parameter set by the electron at rung 3, sitting under the broader T0–T8 forcing chain (J-uniqueness, $\varphi$, eight-tick octave, $D=3$).
No used_by edges are recorded yet; the declaration is an existence seal for the local certificate bundle rather than a step inside a larger proved theorem. It closes the structural side of module 10 with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.