EntanglementCostCert
plain-language theorem explainer
Certificate structure packaging three algebraic properties of the RS entanglement domain cost: vanishing on equal arguments, non-negativity for positive mass/energy pairs, and positivity of the canonical threshold. Cited by anyone assembling or discharging the entanglement-cost layer. Pure structure definition; the inhabited witness is built separately from sibling lemmas.
Claim. An RS entanglement-cost certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ vanishes; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical entanglement threshold is strictly positive.
background
The module treats entanglement entropy in Recognition Science units. Classical Shannon form $S=-\sum p_k\log p_k$ is retained, but the RS maximum is forced by the Count Law in $D=3$: $S_{\max}=D\log 2=3\log 2\approx 2.079$ bits. Domain cost is the real-valued cost assigned to a pair of positive scales (mass-like and energy-like arguments); the canonical threshold is the positive cutoff against which that cost is compared when certifying entanglement.
Upstream, recognition-event cost is already known to be nonnegative via the J-cost calculus (cost_nonneg: "The cost of any recognition event is non-negative"). The present structure lifts that nonnegativity, plus a diagonal-vanishing identity and threshold positivity, into a single certificate type used by the entanglement layer.
Local status is structural: zero sorry, zero axioms. Sibling lemmas supply the three field proofs; this declaration only names the bundle.
proof idea
No proof body: this is a structure definition. The three fields are Prop-valued requirements on domainCost and canonicalThreshold. Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to cert_inhabited, which packages that witness as Nonempty.
why it matters
Gives the entanglement-cost layer a single named interface rather than three free-floating lemmas. Downstream, cert is the concrete inhabitant and cert_inhabited records that the type is nonempty, so later theorems can assume an entanglement-cost certificate without re-proving diagonal vanishing, nonnegativity, or threshold positivity.
In the broader RS chain this sits under the Count-Law / eight-tick geometry that forces $D=3$ (T8) and therefore $S_{\max}=3\log 2$. The nonnegativity field is the entanglement-side echo of J-cost nonnegativity from ObserverForcing and the T5 uniqueness of $J(x)=(x+x^{-1})/2-1$. The structure itself does not compute numerical entanglement entropies; it only certifies the cost primitives those computations rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.