cert_inhabited
plain-language theorem explainer
The three-field certificate for the recognition Hilbert-space setup is inhabited: domain cost vanishes on the diagonal, is nonnegative on positive arguments, and the canonical threshold is positive. Anyone wiring structural hypotheses into H_RS = L^2(recognition manifold) would cite this. Proof is a one-line term witness packaging a prebuilt certificate value.
Claim. The certificate type for the three-dimensional recognition Hilbert-space setup is nonempty: there exist proofs that domain cost vanishes on the diagonal for every nonzero real, that domain cost is nonnegative for positive mass-energy pairs, and that the canonical threshold is strictly positive.
background
The module builds the recognition Hilbert space $H_{RS}$ as $L^2$ on the recognition manifold. Basis labels are rung, spin, charge, and phase; the Hamiltonian is assembled from the J-cost on powers of $\varphi$, in the sense of the Plan v7 structural session (0 sorry, 0 axiom).
Domain cost is the local cost on mass-energy pairs induced by the Recognition Science cost $J(x)=(x+x^{-1})/2-1$. The certificate structure packages three elementary analytic facts about that cost and a fixed positive cutoff: diagonal vanishing off zero, nonnegativity on the positive quadrant, and positivity of the canonical threshold.
Those three fields are the minimal Prop-level handle needed before treating $H_{RS}$ as a cost-weighted Hilbert space rather than a bare $L^2$ space.
proof idea
Term-mode one-liner. A concrete value of the certificate structure is already assembled from the three field lemmas (diagonal cost identity, nonnegativity, threshold positivity). Nonemptiness is obtained by packaging that value as the witness of Nonempty.
why it matters
Closes the structural certificate for the recognition Hilbert-space module under Foundation: a single inhabited bundle rather than three loose lemmas. Downstream developments that need one Prop-level assumption on cost and threshold can take this nonemptiness instead of reopening the field proofs. It sits under the layer that moves J-cost (forcing-chain T5) and the $\varphi$-ladder into an operator setting for $H_{RS}$. No used_by edges are recorded yet; the declaration is the terminal inhabitation check of the certificate structure itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.