ChemicalPotentialFalsifier
plain-language theorem explainer
The ChemicalPotentialFalsifier structure encodes the three conditions that would refute the derivation of chemical potential as a J-cost gradient. Researchers auditing Recognition Science thermodynamics would cite it to state the empirical tests for the claim that particles flow to minimize total J-cost. The declaration is a direct structure definition that packages the failure modes and requires two of them to be jointly impossible.
Claim. A structure $F$ whose fields are the propositions $P_1$ (particles flow against the chemical-potential gradient), $P_2$ (equilibrium exhibits non-uniform chemical potential), $P_3$ (the J-cost interpretation fails), together with the assertion that $P_1$ and $P_2$ cannot hold simultaneously.
background
The module derives chemical potential from the Recognition Science cost function: particles flow from high to low J-cost, so the chemical potential equals the partial derivative of the free energy with respect to particle number at fixed temperature and volume. The local setting treats equilibrium as the configuration that minimizes total J-cost and therefore requires uniform chemical potential across the system. The module imports the Cost and Constants libraries to supply the J-cost definition and the RS-native units.
proof idea
The declaration is a direct structure definition that introduces the three propositions and the single implication without invoking any lemmas or tactics.
why it matters
The structure supplies the concrete falsifiability criteria for the chemical-potential derivation that sits inside the broader Recognition Science thermodynamics program. It thereby anchors the claim that chemical potential is the J-cost gradient to observable particle flows and equilibrium uniformity. No downstream theorems yet reference it, leaving open the question of how these criteria will be confronted with data on ideal gases or Bose-Einstein condensates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.