cert_inhabited
plain-language theorem explainer
The structural certificate packing diagonal vanishing of domain cost, nonnegativity for positive mass/energy, and positivity of the canonical threshold is inhabited. Anyone assembling or discharging RS_MTH_Structural_005 obligations cites this existence fact. The proof is a one-constructor term that feeds the prebuilt certificate into Nonempty.
Claim. There exists a certificate packing three facts: the domain cost of any nonzero real against itself is zero; the domain cost of positive mass and energy is nonnegative; and the canonical threshold is strictly positive.
background
Module RS_MTH_Structural_005 records structural facts tied to the RS eight-tick: one full traversal of the binary recognition lattice has period $2^D = 8$ when $D = 3$. Status is a closed structural theorem (no sorry, no axiom).
The certificate structure bundles three elementary cost properties. Domain cost is the local cost functional on a mass/energy pair (imported from the Cost layer). Its diagonal vanishes for every nonzero real, and it is nonnegative whenever both arguments are positive. The canonical threshold is a fixed positive real used as a comparison scale in the same module.
Upstream, the structure itself only declares the three fields; the concrete witness cert is assembled from the sibling lemmas that prove each field.
proof idea
Term-mode one-liner. Nonempty is witnessed by the anonymous constructor applied to the already-built certificate value cert, which packages the three proved fields (diagonal vanishing, nonnegativity, threshold positivity). No tactics and no further lemmas are invoked at this site.
why it matters
Gives a single inhabited bundle for the three cost/threshold facts that define Structural Module 5. Downstream consumers can pattern-match on one Nonempty rather than re-proving or re-importing the three fields. In the Recognition framework this sits under the eight-tick octave (forcing chain T7: period $2^3 = 8$) and the $D = 3$ spatial step (T8), as the module doc states. No parent theorems currently list this declaration as a dependency, so its role is local packaging and export of the closed structural status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.