cert
plain-language theorem explainer
Packages three elementary properties of the RS domain entanglement cost into one certificate record: the cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone working in the entanglement-cost layer cites this as the inhabited witness. The body is a pure structure assembly wiring three already-proved sibling lemmas.
Claim. There is a canonical entanglement-cost certificate asserting: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats entanglement entropy $S=-\sum p_k\log p_k$ in Recognition Science units, where the maximum is fixed by the Count Law as $S_{\max}=D\log 2=3\log 2\approx 2.079$ bits (using the forced spatial dimension $D=3$ from the T8 step of the forcing chain).
The certificate structure bundles three elementary facts about the domain cost functional used to score recognition mismatch between two positive scales. The first field requires the cost to vanish when the two arguments coincide (off zero). The second requires nonnegativity for positive arguments, in the same spirit as the upstream observer-forcing result that every recognition-event cost is nonnegative via $J$-cost nonnegativity. The third requires the module's canonical threshold constant to be strictly positive.
Local status is structural: zero sorry, zero axiom. Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields.
proof idea
Pure structure construction, not a tactic proof. The three fields of EntanglementCostCert are filled by direct assignment to the sibling lemmas already proved in-module: diagonal vanishing, nonnegativity on the positive quadrant, and positivity of the canonical threshold. No further rewriting or case analysis occurs.
why it matters
Gives a single named witness that the domain entanglement cost satisfies the minimal analytic hygiene expected of an RS cost (zero on matched scales, nonnegative, positive threshold). That matches the module's claim to be a structural theorem with no sorry and no axiom, and aligns with the broader RS cost philosophy (J-cost nonnegative, minimum at the identity scale).
No downstream consumers are recorded yet in the graph, so the certificate presently anchors the module rather than feeding a named parent theorem. It sits next to cert_inhabited and the domain-cost API, ready for any later bound that needs a packaged proof that the cost and threshold are well-behaved. Framework landmarks in view: $D=3$ (T8) fixing $S_{\max}=3\log 2$, and the nonnegativity lineage through observer-forcing cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.