cert_inhabited
plain-language theorem explainer
The structural certificate packing diagonal vanishing of domain cost, nonnegativity of domain cost, and positivity of the canonical threshold is nonempty. Foundation and calibration work cite it to discharge the module-10 packing obligation in one step. The proof is a one-line term that exhibits the already-built witness.
Claim. There exists a certificate whose three fields assert: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_FDN_Structural_010 is a foundation structural theorem: zero sorry, zero axiom. Its stated role is RS calibration in which the coherence energy $E_{\mathrm{coh}}$ is fixed once by the electron mass, after which predictions are parameter-free.
The certificate structure bundles three elementary cost facts. Domain cost is the local cost functional on pairs of positive (or nonzero) reals used in this module; the diagonal identity says matched arguments incur zero cost, and the second field is ordinary nonnegativity on the positive quadrant. The canonical threshold is the positive real cutoff carried by the same module (sibling positivity lemma).
Upstream, the structure itself is only a Prop-packing record; inhabitation is the theorem that turns the three sibling lemmas into a single inhabited certificate type.
proof idea
One-line term proof: the anonymous constructor of Nonempty is applied to the pre-built witness cert, which already fills the three structure fields. No tactics, no further lemmas beyond that witness.
why it matters
In the Recognition foundation layer this closes the module-10 structural packing: once the certificate is inhabited, downstream calibration and parameter-free prediction arguments can assume diagonal vanishing, cost nonnegativity, and a positive threshold as a single hypothesis. The module framing ties the pack to the electron-mass fixation of $E_{\mathrm{coh}}$. No used-by edges are recorded yet, so the immediate consumer is the structural export surface of the foundation chain rather than a named parent theorem. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it only certifies the cost/threshold side conditions those later steps rely on when calibration is in force.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.