MaxwellDemon2DeepCert
plain-language theorem explainer
Certificate record packaging three properties of the Maxwell-demon domain cost: it vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical recognition threshold is positive. Anyone citing the inhabited demon-cost certificate or the J-cost floor on information erasure uses this bundle. Pure structure definition with no proof body.
Claim. A Maxwell-demon deep certificate is a record of three assertions: (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: a demon cannot drive the J-cost of a recognition event below $J(\varphi)$ per bit processed. Information gain equals $J(\varphi)$ times bits erased, i.e. one recognition quantum per bit. Status is structural (zero sorry, zero axiom).
The underlying cost is the standard RS J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the Recognition Composition Law and the T5 step of the forcing chain. Upstream, every recognition event has nonnegative cost via cost_nonneg from ObserverForcing ("The cost of any recognition event is non-negative"), which itself reduces to nonnegativity of $J$ on positive reals.
Locally, domainCost is the two-argument cost used for the demon's mass/energy bookkeeping, and canonicalThreshold is the positive floor (tied to $J(\varphi)$) that the demon cannot undercut.
proof idea
No proof: this is a structure definition whose three fields are propositions. Inhabitation is deferred to the sibling cert, which fills the fields by the already-proved lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The structure itself only names the interface.
why it matters
Gives a single named certificate type for the structural Maxwell-demon claim in this module: diagonal vanishing (identity events cost nothing), cost nonnegativity, and a strictly positive canonical threshold. Downstream, cert assembles a concrete inhabitant and cert_inhabited records Nonempty MaxwellDemon2DeepCert, closing the module's structural theorem.
In the broader framework this is the Lean packaging of the RS restatement that a demon cannot reduce recognition cost below the $J(\varphi)$ quantum per bit. It sits on the J-uniqueness / RCL side of the forcing chain (T5) and on the nonnegative cost calculus used throughout ObserverForcing and the primitive recognition calculus. It does not itself derive the physical second-law corollary; it freezes the three algebraic facts the rest of the argument quotes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.