Thermodynamics Forced Response Cost Determined Activity

Forced response and its cost

In thermodynamics, a system at equilibrium responds to a small external drive, such as a temperature difference or a voltage, by moving toward a new steady state. The standard linear response theory, developed by physicists in the early twentieth century, says that for small drives the response is proportional to the drive. The constant of proportionality is the transport coefficient, and it captures how easily the system conducts heat or charge. The classical formula for this coefficient, often associated with the work of Rudolph Marcus in electron transfer, takes a simple linear form: it starts at one half and drops linearly as the drive grows.

Recognition Science starts from a different premise. It treats the system as maintaining a discrete record of recognition events, a ledger of what the system has registered, and it forces the cost of maintaining that ledger to follow a specific function. The framework's central theorem, proved in a machine-checked library of formal theorems, shows that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. In log coordinates this is cosh(x) - 1. When this cost is evaluated at the ratio belonging to a drive, the resulting activity function is even, meaning it depends only on the size of the drive, not its direction.

In Recognition Science, the transport coefficient is not assumed linear from the start. The framework defines it as the derivative of the activity with respect to the drive, measured in units of a scale b. The result is a hyperbolic sine: transferCoefficient(c, b, A) = 1/2 + (c/b) * sinh(A/b). This function is odd, so it satisfies reciprocity: the coefficient for a positive drive plus the coefficient for the negative drive equals one. At zero drive, it returns to the classical value of one half. The framework then calibrates the constant c by requiring that the curvature of the activity at zero drive matches the classical linear response. This calibration forces c = Lambda/2, where Lambda is the scale of the drive. The result is a fully determined coefficient: 1/2 + (1/2) * sinh(A/Lambda).

This calibrated coefficient differs from the Marcus form. At the drive value A = Lambda, the Marcus coefficient is exactly zero, meaning the barrier to transfer vanishes. The framework's coefficient at that point is 1/2 + (1/2) * sinh(1), which is strictly positive. The theorem costActivity_ne_marcus proves these two values are unequal. The framework's coefficient only reaches zero at a larger drive, A = Lambda * arsinh(1), a value the library calls the barrierless ratio. This ratio is positive and less than one, so the framework predicts that the barrierless point occurs at a drive greater than the Marcus scale, and that the response continues to grow beyond the classical cutoff.

In Recognition Science, the cost-determined activity has a direct structural consequence. The theorem costDeterminedActivity_implies_reciprocity shows that if the deviation of a system from detailed balance equals the cost activity, then the response function is odd and the system satisfies state exchange. A second theorem, costDeterminedActivity_implies_even_response_zero, shows that under the same condition the even part of the response vanishes identically. In plain language: when the cost of recognition determines the activity, the system's response to a drive is purely antisymmetric, and the symmetric part that would appear in a classical linear theory is absent. The framework's library proves these results from the definitions alone, with no additional assumptions beyond the cost function taking its forced form.

/-- The recognition cost `J x = (x + 1/x)/2 - 1` evaluated at the ledger ratio belonging to a drive,
with the drive measured in units of the scale `b`. In log coordinates this is `cosh - 1`. -/
noncomputable def recognitionCost (b : ℝ) (A : ℝ) : ℝ :=
  cosh (A / b) - 1

/-- **The transfer coefficient of the derived law, and reciprocity as an identity.** With
`alpha A = 1/2 + P' A`, the law gives `alpha A = 1/2 + (c/b) sinh (A/b)`, and the two opposite
drives sum to one exactly. -/
noncomputable def transferCoefficient (c b : ℝ) (A : ℝ) : ℝ :=
  1 / 2 + c / b * sinh (A / b)

/-- **The derived law is a strict strengthening, and it disagrees with Marcus.** The two coefficients
agree at zero drive and to leading order, but they are different functions: at drive equal to the
reorganization scale the derived law exceeds Marcus, because `sinh 1 > 1`. So the framework's claim
is falsifiable against the incumbent theory rather than a rewording of it. -/
theorem costActivity_ne_marcus {Lambda : ℝ} (hL : 0 < Lambda) :
    transferCoefficient (Lambda / 2) Lambda Lambda ≠ marcusTransferCoefficient Lambda Lambda := by
  rw [calibrated_transferCoefficient hL]
  simp only [marcusTransferCoefficient]
  have hdiv : Lambda / Lambda = 1 := div_self hL.ne'
  rw [hdiv]
  have hone : Lambda / (2 * Lambda) = 1 / 2 := by field_simp
  rw [hone]
  have hsinh : (1 : ℝ) < sinh 1 := Real.self_lt_sinh_iff.mpr one_pos
  intro hcontra
  linarith [hcontra, hsinh]

/-- The derived law reaches the barrierless point at `A = Lambda * arsinh 1`. -/
theorem derived_barrierless_at_arsinh {Lambda : ℝ} (hL : 0 < Lambda) :
    transferCoefficient (-(Lambda / 2)) Lambda (Lambda * barrierlessRatio) = 0 := by
  rw [calibrated_transferCoefficient_signed hL]
  have hL' : Lambda ≠ 0 := hL.ne'
  have hdiv : Lambda * barrierlessRatio / Lambda = barrierlessRatio := by
    field_simp
  rw [hdiv]
  simp only [barrierlessRatio, Real.sinh_arsinh]
  norm_num

theorem barrierlessRatio_pos : 0 < barrierlessRatio := by
  have : Real.arsinh 0 < Real.arsinh 1 := Real.arsinh_lt_arsinh.mpr (by norm_num)
  simpa [barrierlessRatio, Real.arsinh_zero] using this

/-- **The barrierless point strictly precedes Marcus's.** Since `sinh` exceeds its argument,
`arsinh 1 < 1`, so the derived rate maximum sits at a driving force strictly below the
reorganization energy. -/
theorem barrierlessRatio_lt_one : barrierlessRatio < 1 := by
  have h1 : (1 : ℝ) < sinh 1 := Real.self_lt_sinh_iff.mpr one_pos
  have := Real.arsinh_lt_arsinh.mpr h1
  rwa [Real.arsinh_sinh] at this

/-- **The closure.** If the deviation from equal splitting is the cost-determined activity, then the
response is odd in the drive and state exchange holds. Reciprocity of the recognition cost, plus
linearity of traffic in cost, yields the kinetic symmetry. -/
theorem costDeterminedActivity_implies_reciprocity
    {F G : ℝ → ℝ} (hDB : DetailedBalance F G) {base c b : ℝ}
    (hP : ∀ A : ℝ, deviation F A = costActivity base c b A) :
    (∀ A : ℝ, responseOfLogRates F G (-A) = -responseOfLogRates F G A)
      ∧ StateExchange F G := by
  have hev : ∀ A : ℝ, deviation F (-A) = deviation F A := by
    intro A; rw [hP (-A), hP A, costActivity_even]
  exact ⟨(odd_iff_deviation_even hDB).mpr hev,
    (stateExchange_iff_deviation_even hDB).mpr hev⟩

/-- And the even part of the measured current vanishes identically, which is the fit-free
experimental signature. -/
theorem costDeterminedActivity_implies_even_response_zero
    {F G : ℝ → ℝ} (hDB : DetailedBalance F G) {base c b : ℝ}
    (hP : ∀ A : ℝ, deviation F A = costActivity base c b A) (A : ℝ) :
    evenResponse F G A = 0 := by
  have hev : ∀ B : ℝ, deviation F (-B) = deviation F B := by
    intro B; rw [hP (-B), hP B, costActivity_even]
  exact evenResponse_eq_zero_of_deviation_even hDB hev A

What this page does not claim

This module does not prove that real thermodynamic systems obey the recognition cost function. The framework does not claim the Marcus linear coefficient is wrong for all drives, only that it differs from the cost-determined form. No experimental measurement of transport coefficients is cited in this module.

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