Pith. sign in
module module moderate

IndisputableMonolith.Foundation.MaxwellDemon2DeepFromJCost

show as:
view Lean formalization →

Module formalizing a two-layer Maxwell-demon obstruction derived from the RS J-cost. It defines a domain cost, a canonical positive threshold, and an inhabited certificate that the demon cannot extract free work below that threshold. Physicists citing the RS second-law story use the certificate; the argument is algebraic nonnegativity of J plus a threshold comparison.

claimOn a recognition domain one has a nonnegative cost $C$ built from the J-cost $J(x)=(x+x^{-1})/2-1$, a canonical threshold $\theta>0$, and an inhabited certificate asserting that any Maxwell-demon protocol whose net recognition cost lies below $\theta$ cannot produce free work (two-deep obstruction).

background

Recognition Science measures mismatch by the unique cost $J(x)=(x+x^{-1})/2-1$ fixed by the Recognition Composition Law. The Cost import supplies that functional and its elementary inequalities (nonnegativity, minimum at $x=1$). Constants supplies the RS tick $\tau_0=1$ used to normalize discrete time.

Maxwell's demon is the classical attempt to convert information into work without a compensating entropy export. In the RS setting the relevant ledger is recognition cost, not Shannon entropy alone: every sorting or measurement step incurs a $J$-cost on the ratio of occupation or probability weights.

This module packages that obstruction at "two-deep" level: a domain-level cost functional, its evaluation identity and nonnegativity, a strictly positive canonical threshold, and a certificate type witnessing that protocols cheaper than the threshold cannot yield free work.

proof idea

Definition-and-certificate module rather than a single deep theorem. It introduces domainCost from the imported J-cost, records the pointwise evaluation identity and nonnegativity, defines a positive canonicalThreshold, and packages them into an inhabited MaxwellDemon2DeepCert. The logical content is: nonnegativity of $J$ plus threshold comparison imply the demon obstruction; no heavy tactic proof is required beyond assembling those facts into the certificate.

why it matters in Recognition Science

Closes a Foundation-layer gap between the pure J-cost calculus and thermodynamic irreversibility claims in RS. Downstream consumers (none yet wired in the graph) would cite the inhabited certificate when discharging second-law or demon-style side conditions in larger forcing or ledger arguments. It sits downstream of T5 J-uniqueness: once $J$ is forced, the demon threshold is a derived positive scale rather than an extra postulate. No open scaffold remains inside the module; the certificate is inhabited.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)