RelationalQM3Cert
plain-language theorem explainer
Packages three structural axioms for relational quantum mechanics read off the J-cost: diagonal vanishing, non-negativity on positive pairs, and a strictly positive canonical threshold. Anyone building observer-frame agreement from Recognition Science cites this certificate type. It is a pure structure definition; inhabitance is discharged separately by the module's cert.
Claim. A relational-QM certificate is a triple of properties of the domain cost $C$ and canonical threshold $\tau$: (i) $C(r,r)=0$ for every $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
The module develops relational quantum mechanics (Rovelli) inside Recognition Science: each observer carries a recognition frame whose comparisons are scored by the J-cost $J(x)=(x+x^{-1})/2-1$. Observers need not share absolute scales, but they agree on $J$ of observable-to-reference ratios.
Here the domain cost is the concrete comparison functional on real pairs (measure vs energy, or analogous positive quantities) used as that frame score. The canonical threshold is the positive cutoff that separates negligible from reportable recognition events in the same units.
Upstream, ObserverForcing already records that every recognition-event cost is non-negative via $J\ge 0$ on positive states. The present structure lifts that positivity, plus diagonal vanishing and threshold positivity, into an explicit certificate interface for the relational-QM story.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements on domainCost and canonicalThreshold. Inhabitation is not claimed here; the sibling definition cert fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and cert_inhabited packages that witness as Nonempty.
why it matters
Gives the typed interface that the module's structural theorem (status: 0 sorry, 0 axiom) must inhabit before relational QM can be read as forced by J-cost frames. Downstream, cert is the concrete witness and cert_inhabited asserts non-emptiness, closing the certificate layer of Plan v7's relational-QM pass.
In the broader forcing chain this sits under the J-uniqueness landmark (T5): once $J$ is the unique cost, diagonal zeros and non-negativity are the minimal frame axioms that let distinct observers share ratio scores without sharing absolute units. It does not itself derive $D=3$ or the eight-tick octave; it only certifies the cost-frame side of relational agreement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.