Thermodynamics Forced Response Large Deviation Bridge

The bridge

In thermodynamics, a system driven away from equilibrium responds with a flux. The response is often nonlinear, and a standard way to describe it is through a dissipation potential, a function whose derivative gives the flux. For a chemical reaction network that satisfies detailed balance, the large deviation principle of the underlying Markov jump process yields a specific dual dissipation potential. Per reaction, stripped of its state-dependent prefactor, that potential is C*(z) = 4 cosh(z/2) - 4, normalized so that C*(z) = z^2/2 + O(z^4) near zero. The prefactor is affinity-independent, a property called tilt invariance, and it is exactly what selects this structure from infinitely many gradient structures generating the same evolution equation. This result is due to Mielke, Peletier and Renger (Potential Analysis 41, 2014), Maas and Mielke (J. Stat. Phys., 2020), and Mielke, Patterson, Peletier and Renger (SIAM, 2016).

The same function appears in Recognition Science, where the framework models a ledger, a discrete record of recognition events, and derives a cost of recognition from five plain conditions. The derived cost is J(x) = (x + 1/x)/2 - 1. The bridge is the observation that the large-deviation potential C* is exactly four times the recognition cost read through a linear bridge with scale one half. The factor four and the half are not adjusted; they are the external normalization and the bridge scale. The flux conjugate to the drive, the derivative of C*, is 2 sinh(z/2), which is precisely the symmetric Butler-Volmer flux at mobility four and bridge scale one half. This is the drive-free response law: a mobility that does not depend on its own drive absorbs the Butler-Volmer symmetry factor.

In Recognition Science, the module records this identification as a theorem. The key content is that the constants are not fitted. If a drive-free flux with positive mobility and positive bridge scale reproduces the symmetric Butler-Volmer response for all drives, then the mobility is four and the bridge scale is one half. Two drives suffice, and the hyperbolic double-angle identity does the rest. In addition, the external normalization condition M*k^2 = 1, which in the large deviation literature fixes the prefactor by matching the quadratic fluctuation regime, comes out satisfied rather than imposed. The electrochemical premise had no access to the fluctuation requirement, and it satisfies it anyway. Two derivations from disjoint premises, one function, one normalization.

This is a theorem in pure real analysis, machine-checked in the framework's library of formal theorems. What is not claimed is that the recognition derivation of J and the large-deviation derivation of C* are the same argument. They are two arguments reaching the same function, which is evidence and not proof. The empirical domain of validity is a separate matter: published outer-sphere kinetics exclude a drive-free mobility above roughly 0.3 of the reorganization energy, consistent with C* being a small-fluctuation normalization to begin with.

/-- **The large-deviation potential is the recognition cost.** `C*` is four times the canonical
J-cost read through the half-affinity bridge. The factor four is the external normalization and
the half is the bridge scale; neither is adjusted here. -/
theorem ldpPotential_eq_four_bridgedCost (z : ℝ) :
    ldpPotential z = 4 * bridgedCost (linearBridge (1 / 2)) z := by
  rw [ldpPotential, bridgedCost, canonicalLogCost_eq_cosh_sub_one, linearBridge]
  ring_nf

/-- And therefore the large-deviation flux is symmetric Butler-Volmer exactly. -/
theorem ldpFlux_eq_butlerVolmer_half (z : ℝ) :
    deriv ldpPotential z = butlerVolmerShape (1 / 2) z := by
  rw [ldpFlux, butlerVolmer_half_eq_two_sinh]

/-- **The mobility and the bridge scale are forced.**

If a drive-free flux with positive mobility and positive bridge scale reproduces the symmetric
Butler-Volmer response, then the mobility is four and the bridge scale is one half. Nothing is
fitted: two drives suffice, and the hyperbolic double-angle identity does the rest.

This is why the agreement with the large-deviation normalization in
`pinned_constants_satisfy_ldp_normalization` is a real coincidence of two derivations rather
than a choice of units. -/
theorem drive_free_match_forces_constants
    {M k : ℝ} (hk : 0 < k)
    (h : ∀ A : ℝ, constantMobilityFlux M k A = butlerVolmerShape (1 / 2) A) :
    k = 1 / 2 ∧ M = 4 := by
  have hsinh1 : 0 < sinh (1 : ℝ) := by
    have hzero : sinh (0 : ℝ) = 0 := Real.sinh_zero
    have hmono : sinh (0 : ℝ) < sinh 1 := Real.sinh_lt_sinh.mpr (by norm_num)
    linarith [hzero, hmono]
  -- Rewrite the hypothesis at the two drives we need.
  have h2 : M * (k * sinh (k * 2)) = 2 * sinh (2 / 2 : ℝ) := by
    have := h 2
    rwa [constantMobilityFlux, butlerVolmer_half_eq_two_sinh] at this
  have h4 : M * (k * sinh (k * 4)) = 2 * sinh (4 / 2 : ℝ) := by
    have := h 4
    rwa [constantMobilityFlux, butlerVolmer_half_eq_two_sinh] at this
  norm_num at h2 h4
  -- Double-angle on both sides: sinh (4k) = 2 sinh (2k) cosh (2k) and sinh 2 = 2 sinh 1 cosh 1.
  have hk4 : sinh (k * 4) = 2 * sinh (k * 2) * cosh (k * 2) := by
    have : k * 4 = 2 * (k * 2) := by ring
    rw [this, Real.sinh_two_mul]
  have hs2 : sinh (2 : ℝ) = 2 * sinh 1 * cosh 1 := by
    have hd := Real.sinh_two_mul (1 : ℝ)
    norm_num at hd
    exact hd
  rw [hk4] at h4
  rw [hs2] at h4
  -- Substituting the first equation collapses h4 to a statement about cosh alone.
  have hcosh : cosh (k * 2) = cosh 1 := by
    have hexpand : (M * (k * sinh (k * 2))) * (2 * cosh (k * 2))
        = 2 * (2 * sinh 1 * cosh 1) := by
      calc (M * (k * sinh (k * 2))) * (2 * cosh (k * 2))
          = M * (k * (2 * sinh (k * 2) * cosh (k * 2))) := by ring
        _ = 2 * (2 * sinh 1 * cosh 1) := h4
    rw [h2] at hexpand
    have hz : sinh 1 * (cosh (k * 2) - cosh 1) = 0 := by linear_combination hexpand / 4
    rcases mul_eq_zero.mp hz with h | h
    · linarith
    · linarith
  -- Positivity turns |2k| = 1 into k = 1/2, and the first equation then gives M.
  have habs : |k * 2| = |(1 : ℝ)| := abs_eq_of_cosh_eq hcosh
  have hkval : k = 1 / 2 := by
    rw [abs_of_pos (by linarith : (0:ℝ) < k * 2), abs_one] at habs
    linarith
  refine ⟨hkval, ?_⟩
  rw [hkval] at h2
  norm_num at h2
  have hkey : (M - 4) * sinh 1 = 0 := by linear_combination 2 * h2
  rcases mul_eq_zero.mp hkey with h | h
  · linarith
  · linarith

/-- **The two normalizations agree.** Matching symmetric Butler-Volmer with a drive-free
mobility implies the large deviation normalization condition `M * k^2 = 1`, which is what fixes
the prefactor externally from the quadratic fluctuation regime `C*(z) = z^2/2 + O(z^4)`. The
electrochemical premise had no access to the fluctuation requirement, and satisfies it. -/
theorem butlerVolmer_match_implies_ldp_normalization
    {M k : ℝ} (hk : 0 < k)
    (h : ∀ A : ℝ, constantMobilityFlux M k A = butlerVolmerShape (1 / 2) A) :
    M * k ^ 2 = 1 := by
  obtain ⟨hkval, hMval⟩ := drive_free_match_forces_constants hk h
  rw [hkval, hMval]
  norm_num

What this page does not claim

The recognition derivation of J and the large-deviation derivation of C* are the same argument. The empirical domain of validity of the drive-free mobility is established by this theorem. The factor four and the bridge scale one half are fitted to match the large-deviation normalization.

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/ForcedResponseLargeDeviationBridge.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: