idealGasMu
plain-language theorem explainer
The declaration defines the chemical potential of an ideal gas as μ = k_B T ln(n λ³) with thermal wavelength λ = h / sqrt(2 π m k_B T) for T > 0. Thermodynamicists working in the Recognition Science framework cite it when linking particle density to J-cost minimization in ledger models. The definition is a direct algebraic transcription of the standard formula using the exact SI Boltzmann constant.
Claim. The chemical potential of an ideal gas is μ(T, n, m) = k_B T ln(n λ³) where λ = h / sqrt(2 π m k_B T) for T > 0, n denotes number density, and m the particle mass.
background
In Recognition Science the chemical potential measures the J-cost gradient with respect to particle number, so that particles flow to minimize total J-cost and determine ledger occupation. The module sets the target of deriving μ from these gradients, with the explicit relation μ = (∂F/∂N){T,V} = (∂G/∂N){T,P}. Upstream the Boltzmann constant is anchored exactly as k_B = 1.380649 × 10^{-23} J/K.
proof idea
The definition first computes the thermal wavelength λ from Planck's constant h, mass m, and the SI Boltzmann constant, then returns k_B T times the logarithm of n λ³. It is a direct algebraic definition with no lemmas or tactics applied.
why it matters
This definition supplies the explicit formula required by the THERMO-007 target for expressing chemical potential as a J-cost gradient. It grounds thermodynamic quantities inside the Recognition framework's forcing chain and recognition composition law, supporting later derivations of equilibrium uniform μ and reaction equilibrium even though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.