cert
plain-language theorem explainer
Packages three elementary facts about domain J-cost into the monogamy certificate: diagonal vanishing, nonnegativity, and a positive canonical threshold. Anyone invoking three-party entanglement monogamy from J-cost cites this inhabited record. Construction is a pure structure fill-in from three already-proved sibling lemmas.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
The module derives three-party entanglement monogamy from the Recognition Science J-cost. Classical monogamy reads $S(A:B)+S(A:C)\le S(A:BC)$; the RS translation is the cost inequality $J(A,BC)\le J(A,B)+J(A,C)$, obtained from J-cost additivity plus the triangle inequality.
Domain cost is the two-argument specialization of the J-cost used to compare recognition events on a pair of positive reals. The structure EntMonogamy3Cert is the interface that packages the three elementary properties needed before monogamy can be stated: the cost vanishes when both arguments agree and are nonzero, the cost is nonnegative on the positive quadrant, and a fixed positive threshold (the canonical cutoff) is available.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: every recognition event has cost $\ge 0$ because $J$ itself is nonnegative on positive reals.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity on positives), and canonicalThreshold_pos (strict positivity of the threshold). No new algebra is performed; the definition only assembles those three facts into the certificate record.
why it matters
This is the inhabited certificate that makes the module's structural monogamy theorem usable as a single object rather than three loose lemmas. The module is marked STRUCTURAL THEOREM (0 sorry, 0 axiom) and sits in the Foundation layer: monogamy of mutual information is recovered from J-cost geometry rather than from Hilbert-space postulates.
It feeds the local monogamy development (siblings such as cert_inhabited and the domain-cost lemmas). In the broader RS chain it supports the claim that entanglement inequalities are forced by the same J-cost that appears in T5 (J-uniqueness) and the Recognition Composition Law, rather than being independent quantum axioms. No external used-by edges are recorded yet; the certificate is the local packaging step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.