Pith. sign in
module module moderate

IndisputableMonolith.Physics.MaxwellDemon_FromJCost

show as:
view Lean formalization →

Formalizes Maxwell's demon as a recognition-cost obstruction: any attempt to sort microstates without paying the J-cost hits a strictly positive canonical threshold. Physicists citing RS thermodynamics or Landauer-type bounds use this module. The development is mostly definitions plus nonnegativity and positivity lemmas, capped by an inhabited certificate structure.

claimA domain cost $C$ built from the recognition cost $J$ is nonnegative, and there is a canonical threshold $\theta>0$ such that any Maxwell-demon sorting operation that would reduce disorder without external work must pay at least $\theta$. The module packages this as a certificate record asserting the obstruction.

background

Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced uniquely by the Recognition Composition Law. In RS-native units the fundamental tick is $\tau_0=1$. The Cost import supplies the analytic properties of $J$ used here.

Maxwell's demon is the classical thought experiment in which a gatekeeper sorts hot and cold molecules and appears to lower entropy without work. In this module the "work" is recognition cost on the configuration ratio: a domain cost functional is defined so that equality cases and nonnegativity are immediate from $J$, and a canonical positive threshold marks the minimal cost of a successful sort.

The local setting is pure physics scaffolding inside IndisputableMonolith: no continuum statistical mechanics, only the discrete J-ladder cost that already underlies mass and coupling derivations elsewhere in the monolith.

proof idea

Definition-heavy module. domainCost is introduced from J; domainCost_at_eq and domainCost_nonneg are short algebraic consequences of J's minimum at 1 and J>=0. canonicalThreshold is a positive constant (canonicalThreshold_pos). MaxwellDemonCert is a structure bundling the cost obstruction; cert and cert_inhabited supply a concrete inhabited instance. No deep tactic proof: the argument is "J-cost is nonnegative and vanishes only at balance, hence any demon gate that creates imbalance pays a fixed positive floor."

why it matters in Recognition Science

Places Maxwell's demon inside the same J-cost ledger that forces T5 (J-uniqueness) and the RS constants, rather than as a separate information-theoretic parable. Downstream graph is currently empty, so this module is a leaf certificate: it records that the demon cannot operate below the canonical threshold once recognition cost is the only allowed ledger. It aligns with Landauer-style "information is physical" claims, but the currency is J, not kT ln 2. Useful as a physics-facing sanity check that the cost functional used for masses and alpha also blocks free sorting.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)