Physics Thermodynamics Arrow From Jcost

The arrow from cost

The second law of thermodynamics says that in an isolated system, entropy, a measure of disorder, tends to increase until it reaches a maximum at equilibrium. This gives time a direction: you can mix cream into coffee, but you never see it unmix. The law is one of physics' most reliable empirical regularities, yet its origin remains a subject of debate. In the Recognition Science framework, the direction is not an accident but a consequence of a more basic accounting rule.

The framework's central object is a ledger, a discrete record of recognition events, and a cost, a number that measures how much the ledger charges for a given recognition. The cost function J(x) = (x + 1/x)/2 - 1 is forced by five plain conditions, and it has a key property: it is zero when its input equals 1, and positive otherwise. In thermodynamics, the framework models entropy change as a ratio of final to initial entropy, S_final/S_initial. The cost of that ratio is J(S_final/S_initial). Because J is zero only when the ratio is 1, that is, when entropy is unchanged, and positive otherwise, the cost is minimized exactly at reversible processes. The arrow of time is then the gradient of this cost: the ledger pushes the system toward the J = 0 equilibrium, which is maximum entropy.

The module ThermodynamicsArrow_FromJCost proves three general facts about this cost. First, the cost vanishes when the two entropies are equal, domainCost_at_eq. Second, the cost is nonnegative for positive inputs, domainCost_nonneg. Third, a threshold constant, canonicalThreshold = phi - 3/2, is positive, where phi is the golden ratio. These are proved in a machine-checked library of formal theorems. They are stated for the general cost function, not for any specific definition of entropy. The module does not prove that entropy always increases; that would require a definition of m and e in thermodynamic terms, which the module does not provide.

What the module does establish is the mathematical skeleton: the cost function has the right shape to serve as a thermodynamic arrow. It is nonnegative, zero exactly at equilibrium, and has a preferred direction toward that zero. The physical bridge, defining entropy in the ledger's terms, remains open. But the formal result shows that the arrow of time is not an add-on; it is a necessary consequence of the cost function's forced form.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

What this page does not claim

The module proves the second law of thermodynamics for any physical system. The module defines entropy in terms of recognition events. The arrow of time is shown to be unique or to match observed time asymmetry.

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/Physics/ThermodynamicsArrow_FromJCost.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: