Thermodynamics Entropy Arrow3 From Jcost

The arrow's formal core

Thermodynamics describes why some processes run forward and not backward: heat flows from hot to cold, a dropped glass shatters but never reassembles. In Recognition Science, this asymmetry has a formal expression. The framework models a system's state by a ratio m/e, where m and e are positive real numbers, and it measures the cost of recognition, a discrete record of events, through the function Jcost. The arrow of time is the claim that this cost never decreases along a real process; it rises or stays flat, and it stays flat only at equilibrium.

The formal development proves three general facts about this cost. First, when m equals e, the cost is exactly zero. Second, for any positive m and e, the cost is never negative. Third, a threshold value, phi minus 3/2, is positive, where phi is the golden ratio. These three facts combine into a certificate, a packaged object that the framework's machine-checked library verifies in full. The certificate exists, and it is inhabited, meaning the proof is complete and not hypothetical.

The plain-language meaning is direct. The cost function Jcost(x) = (x + 1/x)/2 - 1 is zero when the ratio is 1, which is the balanced state. Away from balance, the cost is positive, and the larger the imbalance, the larger the cost. The arrow of time is the direction in which this cost increases, which is the direction away from balance and toward disorder. The positive threshold involving the golden ratio marks a canonical separation, a built-in scale for when an imbalance is significant.

What this development does not do is tie that cost to any specific thermodynamic system. The definition of domainCost uses the ratio m/e without saying what m and e are in a gas, a star, or a living cell. The three facts are universal properties of the cost function itself, and the accompanying note says plainly that nothing subject-specific is proved. The bridge from this formal core to real thermodynamics, the identification of m and e in physical terms, remains a target for future work.

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]

theorem cert_inhabited : Nonempty ArrowOfTime3Cert := ⟨cert⟩

What this page does not claim

This development proves nothing about any specific thermodynamic system. The arrow of time is not derived here as a physical law, only as a property of the cost function. No identification of m and e with entropy, temperature, or heat is made in this file.

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/EntropyArrow3_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: