cert
plain-language theorem explainer
Packages three elementary facts about the domain cost and the canonical threshold into a single certificate for the Recognition Hilbert space setup. Anyone assembling H_RS from J-cost data cites this bundle. The body is a pure structure instance: each field is filled by an already-proved sibling lemma.
Claim. There is a certificate recording that the domain cost vanishes on the diagonal ($C(r,r)=0$ for $r\neq 0$), is nonnegative for positive mass and energy arguments, and that the canonical threshold is strictly positive.
background
The module builds the Recognition Hilbert space $H_{RS}=L^2$ on the recognition manifold, with basis states labeled by rung, spin, charge, and a canonical phase, and with Hamiltonian weighted by the J-cost on the $\phi$-ladder. Status is structural: zero sorry, zero axiom.
The domain cost is the local cost functional used to score recognition events on that manifold; it is built from the RS J-cost $J(x)=(x+x^{-1})/2-1$. The certificate structure RecogHilbert3Cert packages the three elementary properties needed before one can treat the cost as a legitimate energy scale: diagonal vanishing, nonnegativity on the positive orthant, and a strictly positive threshold.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing (cost_nonneg: "The cost of any recognition event is non-negative"), via $J\ge 0$.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No new algebra is performed.
why it matters
This is the gatekeeping certificate for the Plan-v7 Recognition Hilbert space construction: before $H_{RS}$ and its J-weighted Hamiltonian can be treated as a well-posed quantum object, the cost scale must be certified nonnegative, zero on matched states, and bounded below by a positive threshold. It sits at the foundation layer that feeds the forcing chain's cost uniqueness (T5 J-uniqueness) into the Hilbert-space geometry. No downstream consumers are wired yet in the graph; the immediate role is to discharge the structural hypotheses of the $H_{RS}$ module itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.