cert_inhabited
plain-language theorem explainer
The structural certificate packing three elementary properties of the domain cost (diagonal vanishing, nonnegativity on positives, and a strictly positive canonical threshold) is inhabited. Anyone assembling the RS structural module 10 stack cites this to obtain a concrete witness. The proof is a one-line term that supplies the prebuilt certificate as the Nonempty inhabitant.
Claim. The type of certificates asserting that the domain cost vanishes on the diagonal ($C(r,r)=0$ for all nonzero $r\in\mathbb{R}$), is nonnegative for positive arguments ($C(m,e)\ge 0$ whenever $m>0$ and $e>0$), and that the canonical threshold is strictly positive, is nonempty.
background
Module 10 of the RS structural mathematics layer records calibration facts once the coherence energy is fixed by the electron mass; thereafter predictions are parameter-free. Status is structural theorem: zero sorry, zero axioms.
The certificate structure packages three elementary analytic properties of the domain cost function: it vanishes when both arguments coincide and are nonzero; it is nonnegative on the positive quadrant; and the associated canonical threshold is strictly positive. These are the minimal structural guarantees needed before any ladder or defect work that treats the domain cost as a nonnegative measure vanishing on matched pairs.
Upstream, the structure itself is the sole dependency: inhabitation is exactly the claim that some value of that structure type exists.
proof idea
One-line term proof. The already-constructed certificate value is fed to the Nonempty constructor, so the type is witnessed directly. No tactics, no further lemmas, and no unfolding of the three packed fields.
why it matters
Closes the inhabitation obligation for the structural certificate of module 10, confirming the module's zero-sorry, zero-axiom status. With no downstream edges yet recorded, the immediate role is local: any later consumer can project the three packed properties from an element of the nonempty type. The ambient setting is the RS calibration stance (coherence energy fixed once by the electron mass, predictions thereafter parameter-free). The lemma itself does not touch the forcing chain (T5 J-uniqueness, T6 phi, T7 eight-tick, T8 D=3), the Recognition Composition Law, or the alpha band; it only certifies that the local analytic package is inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.