RecogHilbert3Cert
plain-language theorem explainer
Certificate structure packaging three analytic conditions needed to build the Recognition Hilbert space from J-cost: diagonal vanishing of domain cost, nonnegativity of domain cost on positive reals, and positivity of the canonical threshold. Anyone assembling H_RS = L^2 on the recognition manifold cites this bundle. Pure structure definition with no proof body; the sibling construction supplies the unique inhabitant used downstream.
Claim. A Recognition Hilbert certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module constructs the Recognition Hilbert space $H_{RS}$ as $L^2$ on the recognition manifold, with basis states labeled by rung, spin, charge, and angle coordinates, and with Hamiltonian built from the J-cost weights $J(\varphi^k)$. Domain cost is the real-valued cost functional on pairs of positive scale parameters that descends from the Recognition Composition Law cost $J$; it is required to vanish on the diagonal (matched measure and expectation) and to stay nonnegative off-diagonal. The canonical threshold is the positive cutoff used to separate admissible recognition events from the vacuum floor.
Upstream, nonnegativity of event cost is already known from ObserverForcing: every recognition event has cost $0 \le e.\mathrm{cost}$, via $J$-cost nonnegativity on positive states. The present certificate lifts that fact (and the diagonal identity) into the exact interface shape demanded by the $H_{RS}$ assembly.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold). Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
This certificate is the typed gate for the structural $H_{RS}$ construction (module status: 0 sorry, 0 axiom). Downstream, cert builds the canonical inhabitant by wiring the three sibling lemmas into the fields, and cert_inhabited records Nonempty RecogHilbert3Cert. Without the bundle, the $L^2$ recognition space and the J-weighted Hamiltonian $H_{RS} = -\hbar_R \sum_k J(\varphi^k), n_k$ have no certified cost interface. It sits on the foundation side of the forcing chain: J-uniqueness (T5) and the RCL supply the cost shape whose nonnegativity and diagonal minimum are re-exported here for Hilbert-space use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.