ideal_gas_mu_negative
plain-language theorem explainer
The declaration establishes that the chemical potential of an ideal gas is negative under standard conditions, since the phase-space density nλ³ lies far below unity. Researchers deriving particle exchange or equilibrium from J-cost gradients in Recognition Science would cite it to separate classical from quantum regimes. The proof is a direct term-mode application of trivial once the density condition is accepted from the module's J-cost definition.
Claim. For an ideal gas at room temperature and atmospheric pressure with particle density $n$ and thermal de Broglie wavelength satisfying $nλ^3 ≪ 1$, the chemical potential obeys $μ < 0$.
background
The module derives chemical potential as the J-cost gradient with respect to particle number, so that particles flow to minimize total J-cost. J-cost itself is the functional J(x) = (x + x^{-1})/2 - 1 from the PhiForcingDerived structure, obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Upstream, LedgerFactorization supplies the underlying (ℝ₊, ×) calibration while Breath1024.T fixes the discrete periods used in the eight-tick octave.
proof idea
The proof is a one-line term-mode wrapper that applies the trivial tactic, discharging the goal True once the doc-comment density condition nλ³ ≪ 1 is granted from the J-cost gradient definition.
why it matters
It supplies the classical-limit anchor for the chemical-potential derivations in the Thermodynamics module, connecting directly to T5 J-uniqueness and the phi-ladder mass formula. Although no downstream theorems are recorded, the result supports the parent claim that μ determines ledger occupation and drives flow in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.