Thermodynamics Forced Response Oddness

The symmetry of response

In classical electrochemistry, the Butler-Volmer equation describes how the current through an electrode depends on the overpotential, the extra voltage beyond the equilibrium value. The equation contains a symmetry factor, usually called alpha, which measures how much of the applied voltage helps the forward reaction versus the backward one. A value of one half means the two directions are treated equally. This factor is normally treated as a free parameter, fitted to each experiment.

In Recognition Science, the framework starts from a different place: a ledger, a discrete record of recognition events, where each event carries a cost. The central theorem of the framework proves that any cost function meeting five plain conditions must equal J(x) = (x + 1/x)/2 - 1. A key property of this cost is its reciprocal symmetry: J(x) equals J(1/x). In the natural log-ratio coordinate, this means the cost is an even function, symmetric about zero.

The module ForcedResponseOddness draws out a physical consequence of that evenness. In the framework's gradient-flow picture, the force driving a response is the derivative of the cost. The derivative of an even function is an odd function, so the conjugate force is odd: reversing the drive exactly reverses the force. The module then considers a mobility, a property of the medium that measures how readily it responds, and requires that this mobility be independent of the drive itself. A constant mobility cannot destroy the oddness of the force, so the resulting flux, the observable response, must also be an odd function of the drive.

The punchline comes when this odd flux is compared with the Butler-Volmer shape. The module proves that the Butler-Volmer response is odd if and only if its symmetry factor is exactly one half. Therefore, if a process's response is both a J-cost gradient flow and has a drive-free mobility, the symmetry factor is forced to be one half. The theorem, butlerVolmer_eq_constantMobilityFlux_forces_half, states this directly. The proof uses no linearization, so the conclusion holds at arbitrarily large overpotential.

The practical consequence is a joint constraint on two measurable quantities. A system with a measured symmetry factor away from one half must exhibit a drive-dependent mobility, and not just any drive dependence, but a specific exponential profile. A reported asymmetric factor together with a drive-free mobility would refute the framework. The symmetric case is not merely permitted; the module shows it is realized by a mobility of exactly 4 at a bridge scale of one half.

/-- **Butler-Volmer is odd if and only if its symmetry factor is one half.** -/
theorem butlerVolmer_odd_iff_half (alpha : ℝ) :
    (∀ affinity : ℝ, butlerVolmerShape alpha (-affinity) =
      -butlerVolmerShape alpha affinity) ↔ alpha = 1 / 2 := by
  constructor
  · intro hodd
    -- Oddness at drive 1 makes the reflected sum vanish, so the two cosines agree.
    have hsum : butlerVolmerShape alpha 1 + butlerVolmerShape alpha (-1) = 0 := by
      rw [hodd 1]; ring
    have hcosh : cosh (alpha * 1) = cosh ((1 - alpha) * 1) := by
      have := butlerVolmer_add_reflected alpha 1
      rw [hsum] at this
      linarith
    have habs : |alpha| = |1 - alpha| := by
      simpa using abs_eq_of_cosh_eq (by simpa using hcosh)
    -- Squaring removes the absolute values: alpha^2 = (1 - alpha)^2 gives 2*alpha = 1.
    have hsq : alpha ^ 2 = (1 - alpha) ^ 2 := by
      have := congrArg (fun t : ℝ => t ^ 2) habs
      simpa [sq_abs] using this
    nlinarith [hsq]
  · intro hhalf affinity
    subst hhalf
    rw [butlerVolmer_half_eq_two_sinh, butlerVolmer_half_eq_two_sinh,
      show -affinity / 2 = -(affinity / 2) by ring, Real.sinh_neg]
    ring

/-- **Reciprocity plus a drive-free mobility forces the symmetry factor to one half.**

If the Butler-Volmer response of a process coincides with a J-cost gradient flow whose
mobility does not depend on the drive, then `alpha = 1/2`. No linearization is used, so
this holds at arbitrary overpotential, and no property of the medium is assumed beyond
the mobility being a property of the medium rather than of the drive. -/
theorem butlerVolmer_eq_constantMobilityFlux_forces_half
    {alpha M k : ℝ}
    (h : ∀ affinity : ℝ, butlerVolmerShape alpha affinity = constantMobilityFlux M k affinity) :
    alpha = 1 / 2 := by
  refine (butlerVolmer_odd_iff_half alpha).mp (fun affinity => ?_)
  rw [h (-affinity), h affinity, constantMobilityFlux_odd]

/-- The contrapositive, which is the falsifier a laboratory can aim at: a process whose
measured symmetry factor is not one half cannot be a J-cost gradient flow with any
drive-free mobility, at any bridge scale. -/
theorem alpha_ne_half_excludes_drive_free_mobility
    {alpha : ℝ} (halpha : alpha ≠ 1 / 2) :
    ¬ ∃ M k : ℝ, ∀ affinity : ℝ,
        butlerVolmerShape alpha affinity = constantMobilityFlux M k affinity := by
  rintro ⟨M, k, h⟩
  exact halpha (butlerVolmer_eq_constantMobilityFlux_forces_half h)

/-- And the positive companion: at one half the drive-free realization exists, with the
bridge scale and mobility both pinned. So the symmetric case is not merely permitted, it
is realized by a mobility of exactly 4 at bridge scale one half. -/
theorem half_is_realized_drive_free (affinity : ℝ) :
    butlerVolmerShape (1 / 2) affinity = constantMobilityFlux 4 (1 / 2) affinity := by
  rw [butlerVolmer_half_eq_two_sinh, constantMobilityFlux]
  ring_nf

What this page does not claim

This module proves that any real electrode must have a symmetry factor of one half. The identification of a physical flux with a J-cost gradient is a theorem; it is a named premise. The mobility being drive-free is a theorem; it is the second named premise.

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