Pith. sign in
module module moderate

IndisputableMonolith.Foundation.EntanglementMonogamy3FromJCost

show as:
view Lean formalization →

Module packages a three-party entanglement monogamy certificate built from the RS J-cost. It defines a domain cost, a positive canonical threshold, and an inhabited certificate structure asserting that three-way sharing cannot exceed the J-derived bound. Foundation and quantum-information readers cite it when linking monogamy inequalities to the cost functional rather than to Hilbert-space axioms. The development is definitional plus elementary nonnegativity and positivity facts.

claimFrom the RS cost $J(x)=(x+x^{-1})/2-1$, the module defines a domain cost $C$, a canonical threshold $\tau>0$, and a three-party monogamy certificate asserting that the sum of pairwise entanglement measures is bounded by a $J$-derived constant, with an inhabited instance of that certificate.

background

Recognition Science takes the unique cost $J(x)=\cosh(\log x)-1$ (equivalently $(x+x^{-1})/2-1$) forced by the Recognition Composition Law as the primitive of distinguishability. The Cost import supplies that functional; Constants supplies the RS tick scale used when costs are normalized to native units.

Entanglement monogamy is the statement that strong pairwise entanglement cannot be freely shared among three or more parties. In the usual QI setting one proves CKW-type inequalities from the Hilbert-space inner product. Here the same qualitative bound is read off from nonnegativity and threshold properties of a domain cost built from $J$, so the monogamy statement becomes a consequence of the cost calculus rather than of state-space geometry.

The module therefore introduces domainCost (a $J$-based cost on a discrete domain), records that it is nonnegative and agrees with evaluation at equality cases, fixes a positive canonicalThreshold, and packages these into an EntMonogamy3Cert structure with an inhabited witness.

proof idea

Definition module with short supporting lemmas, not a deep derivation. Domain cost is defined from $J$; equality-at-evaluation and nonnegativity are immediate from the corresponding properties of $J$. The canonical threshold is a positive constant cut from the same cost scale. The certificate structure bundles the cost, the threshold, and the three-party inequality shape; inhabitation is by exhibiting those concrete pieces. No multi-step tactic proof is required beyond positivity and nonnegativity of $J$-expressions.

why it matters in Recognition Science

Places three-party monogamy inside the Foundation layer as a $J$-cost corollary, aligning quantum sharing limits with the same functional that forces $\phi$, the eight-tick octave, and $D=3$ in the T5–T8 chain. Downstream consumers (none linked yet in the graph) would import the inhabited certificate when deriving multipartite bounds or when comparing RS cost inequalities to CKW/Coffman–Kundu–Wootters forms. The module does not itself close a named paper proposition; it supplies the certificate interface those arguments need.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)