Thermodynamics Forced Response Detailed Balance Normal Form

The normal form

In electrochemistry and chemical kinetics, the flux through a reaction is the net rate at which reactants become products. When a voltage or chemical drive A is applied, the forward and reverse reactions no longer proceed at equal rates. The standard assumption, called detailed balance, says that at equilibrium the forward and reverse rates are equal, and that a drive A changes the logarithms of these rates so that their sum equals A. This is a statement about the thermodynamics of the system, not about any particular model of how molecules move.

Under this assumption, the flux can be rewritten exactly. Let F A be the logarithm of the forward rate at drive A, and G A the logarithm of the reverse rate. Detailed balance forces F A + G A = A. The deviation P A = F A - A/2 measures how far the forward rate is from splitting the drive evenly. The flux then factors into two parts: a hyperbolic sine of half the drive, times an exponential of the deviation. The sinh(A/2) factor is forced by detailed balance alone; it requires no additional physical input. The same algebraic identity appears in the large-deviation theory of random walks, where it is written as x - y = 2*sqrt(xy)*sinh((ln x - ln y)/2).

The ledger, a discrete record of recognition events, enters here as a bookkeeping device that tracks forward and reverse transitions. The framework models the response of such a ledger to an external drive, and the normal form is the exact expression for the net flux in terms of the deviation. The module proves that this expression is an identity under detailed balance, and that the deviation is the only free function in the problem. Everything else in the flux is fixed by the thermodynamic constraint.

The substantive result is a symmetry between opposite drives. If the flux is odd, meaning that reversing the drive exactly reverses the net rate, then the deviation must be even: P(-A) = P(A). This is proved as an equivalence. The consequence for measurements is that the transfer coefficient alpha, defined as the derivative of F with respect to A, must satisfy alpha(A) + alpha(-A) = 1. This relation is distinct from the detailed balance constraint alpha(A) + beta(A) = 1, which relates the two directions at a single drive. The new relation connects one direction at two opposite drives, and it is a testable prediction.

The Marcus theory of electron transfer satisfies this symmetry because its deviation is quadratic in A, hence even. Asymmetric Marcus-Hush theory violates it, and the asymmetry parameter in that theory is precisely a measure of how far the deviation is from being even. The module proves these facts as theorems about the algebraic structure, not as empirical claims. The empirical status of the symmetry relation remains open pending reanalysis of published asymmetric Marcus-Hush fits.

What this establishes in plain language is that a large class of rate models, once detailed balance is assumed, reduce to a single free function: the deviation from equal splitting. The half in the sinh factor is not a coincidence or a separate assumption; it is a consequence of the thermodynamic constraint. The measurable symmetry between opposite drives is the surviving prediction that distinguishes symmetric theories like Marcus from asymmetric ones.

/-- **Detailed balance alone forces the half-affinity `sinh` normal form.** No recognition input
is used, and no reciprocity: this is an algebraic identity about any pair of rates whose ratio is
the exponential of the drive. Consequently the half in `sinh (A/2)` is not evidence for anything,
and the draft's claim that its agreement with the large-deviation argument scale was a
coincidence of independent derivations is withdrawn. -/
theorem flux_eq_two_exp_deviation_mul_sinh_half
    {F G : ℝ → ℝ} (hDB : DetailedBalance F G) (A : ℝ) :
    responseOfLogRates F G A = 2 * exp (deviation F A) * sinh (A / 2) := by
  have hG : G A = A - F A := by have := hDB A; linarith
  have key : exp (F A - A / 2) * (exp (A / 2) - exp (-(A / 2)))
      = exp (F A) - exp (-(A - F A)) := by
    rw [mul_sub, ← Real.exp_add, ← Real.exp_add,
      show F A - A / 2 + A / 2 = F A by ring,
      show F A - A / 2 + -(A / 2) = -(A - F A) by ring]
  simp only [responseOfLogRates, deviation, hG, Real.sinh_eq]
  rw [← key]
  ring

/-- **Given detailed balance, the flux is odd if and only if the deviation is even.** This is the
surviving content of reciprocity for charge transfer. In terms of the differential transfer
coefficient `alpha = F'`, an even deviation says `alpha A + alpha (-A) = 1`: the coefficient
measured at opposite drives sums to one. That is a different statement from the detailed-balance
constraint `alpha A + beta A = 1`, which compares the two directions at a single drive. -/
theorem odd_iff_deviation_even
    {F G : ℝ → ℝ} (hDB : DetailedBalance F G) :
    (∀ A : ℝ, responseOfLogRates F G (-A) = -responseOfLogRates F G A) ↔
      (∀ A : ℝ, deviation F (-A) = deviation F A) := by
  constructor
  · intro hodd A
    -- Both sides are `2 * exp (deviation) * sinh (A/2)`, so cancel the nonzero sinh at a
    -- convenient nonzero drive and then transport the conclusion.
    have key : ∀ B : ℝ, B ≠ 0 → deviation F (-B) = deviation F B := by
      intro B hB
      have h1 := hodd B
      rw [flux_eq_two_exp_deviation_mul_sinh_half hDB (-B),
        flux_eq_two_exp_deviation_mul_sinh_half hDB B] at h1
      rw [show (-B) / 2 = -(B / 2) by ring, Real.sinh_neg] at h1
      have hsB : sinh (B / 2) ≠ 0 :=
        sinh_ne_zero_of_ne_zero (by simpa using hB)
      have hexp : exp (deviation F (-B)) = exp (deviation F B) := by
        have h2 : 2 * exp (deviation F (-B)) * sinh (B / 2)
            = 2 * exp (deviation F B) * sinh (B / 2) := by linear_combination -h1
        have h3 := mul_right_cancel₀ hsB h2
        linarith
      exact Real.exp_eq_exp.mp hexp
    rcases eq_or_ne A 0 with rfl | hA
    · simp
    · exact key A hA
  · intro heven A
    rw [flux_eq_two_exp_deviation_mul_sinh_half hDB (-A),
      flux_eq_two_exp_deviation_mul_sinh_half hDB A, heven A,
      show (-A) / 2 = -(A / 2) by ring, Real.sinh_neg]
    ring

/-- **The sign-blind premise carries no content beyond oddness.** For any `j`, an even mobility
reproducing `j` at some bridge scale exists exactly when `j` is odd. So the transport apparatus of
`ForcedResponseSignBlindMobility` does not constrain the response; only oddness does. -/
theorem exists_even_mobility_iff_odd (j : ℝ → ℝ) {k : ℝ} (hk : 0 < k) :
    (∃ M : ℝ → ℝ, (∀ A : ℝ, M (-A) = M A) ∧ ∀ A : ℝ, j A = generalFlux M k A) ↔
      (∀ A : ℝ, j (-A) = -j A) := by
  constructor
  · rintro ⟨M, hM, hrep⟩ A
    rw [hrep (-A), hrep A]
    exact generalFlux_odd_of_even_mobility hM k A
  · intro hodd
    refine ⟨inducedMobility j k, inducedMobility_even_of_odd hodd k, fun A => ?_⟩
    rw [generalFlux, inducedMobility]
    rcases eq_or_ne A 0 with rfl | hA
    · -- At zero drive both sides vanish, the left because an odd function does.
      have hj0 : j 0 = 0 := by
        have h := hodd 0
        rw [neg_zero] at h
        linarith
      simp [hj0]
    · have hsinh : k * sinh (k * A) ≠ 0 := by
        have hkA : k * A ≠ 0 := mul_ne_zero (ne_of_gt hk) hA
        exact mul_ne_zero (ne_of_gt hk) (sinh_ne_zero_of_ne_zero hkA)
      field_simp

/-- Marcus kinetics are odd, stated through the normal form. -/
theorem marcus_response_odd
    {F G : ℝ → ℝ} (hDB : DetailedBalance F G) (Lambda : ℝ)
    (hF : deviation F = marcusDeviation Lambda) (A : ℝ) :
    responseOfLogRates F G (-A) = -responseOfLogRates F G A := by
  refine (odd_iff_deviation_even hDB).mpr (fun B => ?_) A
  rw [hF]
  exact marcusDeviation_even Lambda B

What this page does not claim

This does not claim that the symmetry relation alpha(A) + alpha(-A) = 1 is empirically verified; its empirical status is open. This does not claim that detailed balance holds for all chemical reactions; it is an assumption of the theorem. This does not claim that the deviation function is unique or that it can be derived from first principles.

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