alternativeDefinitions
plain-language theorem explainer
alternativeDefinitions enumerates three equivalent thermodynamic expressions for chemical potential μ. A researcher deriving thermodynamics from J-cost gradients would cite this list to anchor the RS derivation to classical relations. The definition is a direct static enumeration of the partial-derivative forms with no computation or lemmas applied.
Claim. The chemical potential admits the equivalent expressions $μ = (∂G/∂N)_{T,P}$, $μ = (∂U/∂N)_{S,V}$, and $μ = -T(∂S/∂N)_{U,V}$, all valid at equilibrium.
background
In the Recognition Science setting of THERMO-007, chemical potential measures the energy cost of adding one particle and drives flow from high to low μ. The module interprets μ as the J-cost gradient with respect to particle number, where particles minimize total J-cost on the recognition manifold. Upstream results include the J-cost functional from Cost.FunctionalEquation and RS-native units from Constants.RSNativeUnits.U.
proof idea
The declaration is a definition that directly constructs a List String containing the three listed expressions. No lemmas or tactics are invoked; it is a static enumeration.
why it matters
This definition supplies the classical target expressions that the J-cost gradient derivation must recover. It anchors the RS-native chemical potential to standard thermodynamics within the forcing chain from J-uniqueness to thermodynamic relations. No downstream uses are recorded, but the list supports sibling definitions such as idealGasMu.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.