cert_inhabited
plain-language theorem explainer
The D = 3 configuration-dimension certificate is inhabited: a packed record of diagonal vanishing, nonnegativity of the domain cost, and a positive canonical threshold exists. Anyone citing the eight-tick forcing of three spatial dimensions can point here for the live certificate object. The proof is a one-line term that supplies the prebuilt witness.
Claim. The type of D = 3 configuration certificates is nonempty: there exists a record packing (i) $\mathrm{domainCost}(r,r)=0$ for every $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) positivity of the canonical threshold.
background
The module treats spatial dimension as forced by eight-tick closure. The recognition clock has period $8=2^3$, so the cycle closes after exactly three binary recursions; the module narrative identifies this with $D=3$, the unique value for which the recognition lattice is minimal and self-similar (forcing-chain landmark T8).
The certificate structure packages three elementary side conditions on the domain cost: it vanishes on the diagonal $m=e$, it is nonnegative on the positive quadrant, and the canonical threshold used by the configuration is strictly positive. These are the structural hypotheses later code expects when it treats the D = 3 package as a single inhabited object rather than three separate lemmas.
proof idea
Term-mode one-liner. The anonymous constructor supplies the already-built value cert as a witness for Nonempty of the certificate structure; no tactics and no further lemmas are invoked.
why it matters
Gives the Foundation layer a standard inhabited-certificate handle for the D = 3 structural package tied to eight-tick closure (period $2^3$, forcing-chain T8). The module is marked structural with zero sorry and zero axioms; this theorem is the final inhabitation step that exposes the packed certificate. The dependency graph currently lists no downstream users, so the declaration is the export surface rather than an intermediate lemma inside a longer proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.