summary
plain-language theorem explainer
Chemical potential equals the J-cost gradient with respect to particle number, with particles flowing from high to low values and equilibrium requiring uniformity. Researchers deriving thermodynamics from recognition costs cite these five points when connecting J-cost to standard free-energy derivatives. The declaration is a direct list definition encoding the interpretive statements.
Claim. The chemical potential satisfies $μ = (∂F/∂N)_{T,V} = (∂J_{total}/∂N)$, particles flow from high $μ$ to low $μ$, equilibrium holds when $μ$ is uniform throughout the system, and reactions proceed to minimize $∑ μN$.
background
Module THERMO-007 targets derivation of chemical potential from J-cost gradients. J-cost is the cost of a recognition event, given by Cost.Jcost e.state (ObserverForcing.cost) and equivalently the derivedCost of a multiplicative recognizer comparator (MultiplicativeRecognizerL4.cost). The chemical potential measures the energy cost to add one particle and drives flow to minimize total J-cost, determining ledger occupation.
proof idea
Direct definition that returns a fixed list of five strings. No lemmas or tactics are applied; the body simply enumerates the key interpretive statements listed in the module documentation.
why it matters
This supplies the interpretive bridge between J-cost gradients and thermodynamic chemical potential as stated in the THERMO-007 target. It anchors particle flow and equilibrium statements inside the Recognition framework, consistent with J-cost non-negativity and the multiplicative structure from upstream cost definitions. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.