cert_inhabited
plain-language theorem explainer
The D=3 configuration-space certificate bundle is inhabited: there exists a record packing diagonal vanishing of domain cost, nonnegativity on the positive orthant, and positivity of the canonical threshold. Anyone assembling the Riemannian recognition metric on C_3 = R^3 cites this existence fact. The proof is a one-line term that feeds the concrete witness cert into Nonempty.
Claim. The type of D=3 configuration-space certificates is nonempty: there exists a record asserting (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) the canonical threshold is strictly positive.
background
The module fixes the Recognition Science configuration space at spatial dimension three: $C_3=\mathbb{R}^3$ equipped with the recognition metric $ds^2=J(dx/x)$ on the positive orthant, where $J$ is the unique cost forced by the Recognition Composition Law (T5). The metric is claimed positive definite for all $x>0$.
A certificate is a structure packing three elementary facts about the domain cost and the canonical threshold: diagonal vanishing away from zero, nonnegativity when both arguments are positive, and strict positivity of the threshold. These are the minimal algebraic hooks needed before one treats the J-cost as a Riemannian metric on the positive orthant.
The module status is structural (zero sorry, zero axiom). The present theorem only asserts that such a certificate object exists.
proof idea
Term-mode one-liner. The sibling definition cert already assembles a concrete ConfigSpaceD3Cert value. The proof is the introduction rule for Nonempty, written ⟨cert⟩, so the witness is exactly that pre-built certificate. No tactics, no further lemmas.
why it matters
T8 of the forcing chain fixes spatial dimension $D=3$. This module supplies the configuration-space side of that claim: $C_3$ with the J-cost Riemannian metric. Inhabiting the certificate is the existence half of the structural package (cost identities plus positive threshold) that later metric and measure constructions on the positive orthant can assume without re-proving the elementary cost facts.
No downstream dependents are recorded yet; the theorem is a leaf existence fact inside Foundation.Configuration_Space_D3. It closes the "is the certificate type empty?" question for any development that wants a single Nonempty hypothesis rather than three separate lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.