cert
plain-language theorem explainer
Packages three elementary facts about the domain J-cost into a single Relational QM certificate: cost vanishes on the diagonal, cost is nonnegative off the diagonal for positive arguments, and the canonical recognition threshold is positive. Anyone citing the structural RQM-from-J-cost theorem uses this bundle. The definition is a pure structure inhabitant wiring three sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical recognition threshold is strictly positive.
background
The module develops Relational Quantum Mechanics (Rovelli) inside Recognition Science: each observer carries a J-cost frame, so absolute scale is observer-dependent while ratios of the form $J(\mathrm{observable}/\mathrm{reference})$ are shared. The cost functional is the unique RS cost $J(x)=(x+x^{-1})/2-1$ (T5), extended here as a domain cost on pairs of positive reals (measure vs expectation).
RelationalQM3Cert is the structure that packages the three minimal positivity and normalization facts needed before any observer-comparison argument. Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing (cost_nonneg: every recognition event has nonnegative cost, via Jcost_nonneg). The sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields of the certificate.
proof idea
One-line structure inhabitant. The three fields are filled by direct assignment to the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive measure and expectation), and canonicalThreshold_pos (strict positivity of the canonical threshold). No additional tactics or algebraic work.
why it matters
This is the concrete certificate object for the module's structural theorem that Relational QM arises from J-cost frames (Plan v7, 122nd pass; 0 sorry, 0 axiom). It sits at the foundation layer: once the certificate exists, downstream arguments can treat domain cost as a genuine nonnegative cost with a unique zero on the identity ray and a positive detection threshold, matching the RS forcing chain (T5 J-uniqueness) and the observer-forcing nonnegativity result. No used_by edges are recorded yet; the immediate consumer is the inhabitedness lemma cert_inhabited and any later observer-agreement theorems that quantify over a RelationalQM3Cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.