cert_inhabited
plain-language theorem explainer
The eight-tick completeness certificate type is inhabited: there is a concrete package of the three structural facts (diagonal domain-cost vanishes, domain-cost is nonnegative, canonical threshold is positive). Foundation authors cite it to discharge Nonempty obligations without unpacking fields. The proof is a one-line term that wraps the existing concrete certificate.
Claim. The type of eight-tick completeness certificates is nonempty. Equivalently, there exists a package asserting: (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
The module treats the Recognition Science eight-tick cycle as a structural completeness statement: a period-8 lattice covers all $2^D=8$ binary states exactly once per cycle, and no shorter period does. Status is a structural theorem (zero sorry, zero axiom).
An eight-tick completeness certificate is a structure bundling three real-analytic facts about the local cost: domain cost vanishes on the diagonal for nonzero arguments, domain cost is nonnegative on the positive quadrant, and the canonical threshold is positive. Domain cost is the module's cost functional on pairs of reals; the canonical threshold is the positive cutoff used to mark completeness of the cycle.
This declaration only asserts that such a package exists as a type-theoretic inhabitant, not a new analytic identity.
proof idea
Term-mode one-liner. The module already builds a concrete value cert : EightTickCompleteCert. The proof is the standard Nonempty introduction ⟨cert⟩, i.e. package that value as a witness. No tactics, no further lemmas.
why it matters
Closes the inhabitance side of the eight-tick completeness certificate in Foundation, aligning with the T7 landmark (eight-tick octave, period $2^3$). Downstream code that only needs Nonempty EightTickCompleteCert (choice, instance search, or abstract completeness hypotheses) can cite this without opening the three fields.
No used_by edges are recorded yet; the declaration is the terminal inhabitance fact for the local cert structure. It does not itself prove minimality of period 8 beyond what the bundled fields encode; that content lives in the surrounding module narrative and sibling lemmas on domain cost and the threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.