Encyclopedia Physics Physics Entropy Arrow From Jcost

ARTICLE 4 claims 4 theorems

Physics Entropy Arrow From Jcost

Entropy increase defines time's direction, and Recognition Science derives this arrow from a single cost function.

The thermodynamic arrow

The thermodynamic arrow of time is the observation that entropy increases as time moves forward. A dropped glass shatters, but shattered glass never reassembles. In physics, this one-way direction is puzzling because the underlying laws of mechanics are time-reversible: they work the same whether time runs forward or backward. The puzzle is why a reversible world produces an irreversible experience.

Recognition Science offers an answer from a different starting point. It models reality as maintaining a ledger, a discrete record of recognition events, where each event carries a forced cost. The cost function J(r) is positive for every state except one, and that special state is equilibrium. The framework proves J(r) ≥ 0 for all positive r, and J(1) = 0, meaning the state r = 1 costs nothing. Evolution, in this account, drives r toward 1, and that movement defines the future direction of time.

The framework's library of machine-checked theorems establishes four properties. First, the cost is always non-negative. Second, equilibrium sits at exactly r = 1 with zero cost. Third, the cost function is symmetric under inversion: J(r) = J(1/r). This last property is the time-reversal symmetry of the underlying cost, which mirrors the reversibility of classical mechanics. The arrow emerges not from the cost itself but from the direction of approach to equilibrium.

The module also counts the five standard arrows of time, thermodynamic, cosmological, causal, psychological, and quantum, and proves their count equals 5. This is a structural claim: the framework identifies the number of distinct arrows with a dimension of its configuration space, not with any physical content about each arrow. The classical puzzle of time's direction remains, but Recognition Science relocates it: the arrow is not a mystery to be explained away, but a consequence of a cost function that forces r toward 1.

THEOREM jcost_nonneg · IndisputableMonolith/Physics/EntropyArrowFromJCost.lean
theorem jcost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ Jcost r := by
  by_cases h : r = 1
  · rw [h, Jcost_unit0]
  · exact le_of_lt (Jcost_pos_of_ne_one r hr h)
THEOREM equilibrium_zero · IndisputableMonolith/Physics/EntropyArrowFromJCost.lean
theorem equilibrium_zero : Jcost 1 = 0 := Jcost_unit0
THEOREM time_reversal_symmetric · IndisputableMonolith/Physics/EntropyArrowFromJCost.lean
theorem time_reversal_symmetric {r : ℝ} (hr : 0 < r) :
    Jcost r = Jcost r⁻¹ := Jcost_symm hr
THEOREM arrowCount · IndisputableMonolith/Physics/EntropyArrowFromJCost.lean
theorem arrowCount : Fintype.card ThermodynamicArrow = 5 := by decide

What this page does not claim

This module does not prove that entropy must increase; it proves properties of the cost function and identifies the direction of approach as the arrow. The count of five arrows is a structural theorem, not a derivation of the physical content of each arrow. The framework does not claim to resolve the classical puzzle of why the universe started in a low-entropy state.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND