Thermodynamics Forced Response Law

The forced response law

In thermodynamics, a system pushed away from equilibrium responds with a flux: heat flows, charge moves, or a reaction proceeds. The forced response law in Recognition Science starts from the cost, a measure of how far a state sits from its preferred one, and asks what the response looks like when the cost is the canonical one forced by the framework's axioms. The answer is exact. The canonical cost, written in a log-ratio coordinate, is cosh(s) - 1, and its derivative, the force conjugate to that coordinate, is sinh(s). This is a proved theorem, not a model choice.

The classical cousin of this result is the Butler-Volmer equation, the workhorse of electrochemistry that describes how current depends on overpotential. Its dimensionless shape is exp(alpha * affinity) - exp(-(1 - alpha) * affinity), where alpha is a symmetry factor. When alpha equals one half, this shape reduces to 2 * sinh(affinity / 2), a symmetric hyperbolic sine. The framework's theorem shows that this symmetric sinh profile is exactly what the canonical cost derivative produces when the bridge from physical affinity to log-ratio is a half-scale linear map. The framework thus recovers a known physical law as a consequence of its cost structure.

The module then proves a sharp boundary on what the cost alone can determine. A general coordinate bridge, a differentiable map from physical affinity to the log-ratio, contributes its own derivative as a free factor. The flux shape is therefore conditional on two inputs: the bridge and a mobility law. Even with the bridge fixed to half-affinity, every Butler-Volmer symmetry factor alpha can be realized by choosing a positive mobility that absorbs the asymmetry. The theorem every_butlerVolmer_alpha_is_gradientFlux shows this explicitly. A free mobility prevents the cost-gradient model from selecting alpha = 1/2; the canonical cost alone does not pin down the symmetry factor.

What the law does establish is a clean separation. The derivative of the canonical cost is a theorem: sinh(s). The bridge and mobility are model inputs, each contributing a factor. The flux shape is conditional on those inputs, and the module proves that ratio-level premises do not determine flux amplitude: two positive rate pairs can share the same ratio yet differ in net rate. In plain language, the framework tells you exactly what the cost forces and exactly where physics must step in with extra assumptions.

/-- The canonical log-ratio cost is exactly `cosh s - 1`. -/
theorem canonicalLogCost_eq_cosh_sub_one (s : ℝ) :
    canonicalLogCost s = cosh s - 1 := by
  simpa [canonicalLogCost, FunctionalEquation.G] using
    FunctionalEquation.Jcost_G_eq_cosh_sub_one s

/-- The force conjugate to the canonical log-ratio coordinate is `sinh s`. -/
theorem canonicalLogCost_deriv (s : ℝ) :
    deriv canonicalLogCost s = sinh s := by
  have hfun : canonicalLogCost = fun t : ℝ => cosh t - 1 := by
    funext t
    exact canonicalLogCost_eq_cosh_sub_one t
  rw [hfun]
  exact (Real.hasDerivAt_cosh s).sub_const 1 |>.deriv

/-- At symmetry factor one half, Butler-Volmer is the symmetric sinh law. -/
theorem butlerVolmer_half_eq_two_sinh (affinity : ℝ) :
    butlerVolmerShape (1 / 2) affinity = 2 * sinh (affinity / 2) := by
  rw [butlerVolmerShape, Real.sinh_eq]
  ring_nf

/-- Even after fixing the bridge to half-affinity, every Butler-Volmer symmetry
factor is realizable by choosing the displayed positive mobility. Therefore a
free mobility prevents the cost-gradient model from selecting `alpha = 1 / 2`.
-/
theorem every_butlerVolmer_alpha_is_gradientFlux (alpha affinity : ℝ) :
    gradientFlux (butlerVolmerMobility alpha) (linearBridge (1 / 2)) affinity =
      butlerVolmerShape alpha affinity := by
  rw [gradientFlux, linearBridge_cost_deriv, butlerVolmer_factorization]
  simp only [butlerVolmerMobility]
  ring_nf

/-- Positive forward and backward rate pairs can have the same ratio but
different net rates. Ratio-level premises therefore do not determine flux
amplitude. -/
theorem rate_ratio_does_not_determine_net_rate :
    ∃ q₁plus q₁minus q₂plus q₂minus : ℝ,
      0 < q₁plus ∧ 0 < q₁minus ∧ 0 < q₂plus ∧ 0 < q₂minus ∧
      q₁plus / q₁minus = q₂plus / q₂minus ∧
      q₁plus - q₁minus ≠ q₂plus - q₂minus := by
  refine ⟨2, 1, 4, 2, by norm_num, by norm_num, by norm_num, by norm_num, ?_, ?_⟩
  · norm_num
  · norm_num

What this page does not claim

The framework derives the Butler-Volmer equation from first principles; it recovers the symmetric alpha = 1/2 shape as a theorem and shows other symmetry factors require additional model inputs. The bridge and mobility are not derived; they remain free inputs. This page does not claim the framework selects a unique flux law for physical systems.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Thermodynamics/ForcedResponseLaw.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: