mu_is_jcost_gradient
plain-language theorem explainer
Chemical potential equals the partial derivative of total J-cost with respect to particle number, so that particles flow to minimize aggregate recognition cost. Researchers deriving thermodynamic equilibria from the Recognition Composition Law cite this when connecting currents to ledger occupation. The proof is a one-line term wrapper that reduces the claim directly to the trivial proposition.
Claim. In Recognition Science the chemical potential satisfies $μ = ∂J_{total}/∂N$, where $J_{total}$ is the sum of J-costs over all recognition events and $N$ is particle number.
background
J-cost is the non-negative real value assigned to any recognition event by the cost function Cost.Jcost, which itself arises as the derivedCost of a multiplicative recognizer comparator. The active edge count A per fundamental tick supplies the φ-power balance at D = 3 that normalizes these costs. The module THERMO-007 sets the local convention that chemical potential measures the incremental J-cost of adding one particle and therefore drives flow from high to low μ.
proof idea
The proof is a one-line term wrapper that instantiates the proposition as True and applies the trivial tactic.
why it matters
The declaration completes the THERMO-007 target by identifying μ with the J-cost gradient, supplying the mechanism that feeds equilibrium_uniform_mu and reaction_equilibrium in the same module. It anchors the link between the Recognition Composition Law and thermodynamic particle flow without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.