cert_inhabited
plain-language theorem explainer
The certificate packing diagonal vanishing of domain cost, its nonnegativity on positive arguments, and positivity of the canonical threshold is nonempty. Structural-module consumers cite this to obtain a single inhabited witness rather than three separate lemmas. The proof is a one-line term that supplies the packaged certificate as the inhabitant.
Claim. There exists a certificate asserting: (i) the domain cost of any nonzero real $r$ against itself vanishes, (ii) the domain cost of positive measure and expectation is nonnegative, and (iii) the canonical threshold is strictly positive.
background
Module RS_FDN_Structural_005 is a zero-sorry structural package for the Recognition Science eight-tick: the period $2^D=8$ complete traversal of the binary recognition lattice (forcing landmark T7). It sits in the Foundation layer and imports only Constants and Cost.
The certificate structure bundles three elementary facts about a real-valued domain cost and a canonical threshold: cost vanishes on the diagonal for nonzero reals, cost is nonnegative when both arguments are positive, and the threshold is positive. Those three properties are the only fields of the structure; the present theorem merely asserts that the structure type is inhabited.
proof idea
One-line term proof. The inhabitant is the already-constructed certificate term cert, introduced via the anonymous constructor for Nonempty. No tactics, no further lemmas, and no unfolding of the three field proofs.
why it matters
Gives a single Nonempty witness for the structural certificate of module 5, so downstream code can obtain the three cost/threshold facts by projection rather than by separate imports. The module itself is tagged STRUCTURAL THEOREM and records the eight-tick octave (period $2^3=8$), the T7 landmark of the forcing chain. No downstream users are recorded yet; the declaration closes the module's certificate interface rather than feeding a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.