cert
plain-language theorem explainer
Packages three elementary facts about the Maxwell-demon domain cost into a single certificate: the cost vanishes on the diagonal, is nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Anyone citing the structural Maxwell-demon bound from J-cost will pull this bundle rather than the three lemmas separately. The body is a pure structure instance, wiring named sibling proofs into the certificate fields.
Claim. There is a 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 recognition threshold is strictly positive.
background
The module reformulates Maxwell's demon in Recognition Science language: a demon cannot drive the J-cost of a recognition event below $J(\varphi)$ per bit processed, so information gain equals one recognition quantum per erased bit. Domain cost is the local cost functional on pairs of positive reals that the demon would have to pay; the canonical threshold is the positive lower bound against which that cost is compared.
The certificate structure collects exactly the three algebraic properties needed downstream: diagonal vanishing (identity events cost nothing), nonnegativity on the positive orthant, and positivity of the threshold. Nonnegativity of recognition cost is already known upstream from the J-cost lemma: any recognition event has cost $J(x)\ge 0$ for $x>0$. The present module specializes that fact to the demon's domain-cost functional.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (threshold positivity). No extra tactics or rewriting; the definition is pure packaging.
why it matters
Gives a single named inhabitant of the Maxwell-demon deep certificate so later arguments can assume the three cost axioms by one hypothesis rather than three. Fits the module's structural theorem (zero sorry, zero axiom) that the demon cannot undercut $J(\varphi)$ per bit. Sits on the J-cost foundation (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$) and the recognition-composition law, which force nonnegativity and the self-similar scale $\varphi$. No downstream users are wired yet; the sibling inhabitedness lemma is the immediate consumer. Closes the certificate interface for the Plan v7 Maxwell-demon session.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.