Physics Phase Space3 From Jcost

Phase space volume

Phase space is the abstract room in which every possible state of a physical system is a single point. A swinging pendulum, for instance, has a phase space whose points record both its current angle and its current speed. The volume of a region of this room counts how many distinct states are packed into it. In classical mechanics, a famous result called Liouville's theorem states that this volume is preserved over time for systems that follow Hamiltonian dynamics, the standard equations of motion that conserve energy. A drop of ink spreading in water, by contrast, is a non-Hamiltonian process: its phase space volume grows as the system becomes more disordered.

Recognition Science (RS) is a framework that starts from a single forced cost function, J(x) = (x + 1/x)/2 - 1, which measures the price of recognizing one state from another. The module in question defines a domain cost, a measure of how far a system's current state has drifted from its initial state, as J applied to the ratio of two phase space densities. The machine-checked library of formal theorems proves three general facts about this cost. First, when the current density equals the initial density, meaning no change has occurred, the cost is exactly zero. Second, for any positive densities, the cost is never negative. Third, the constant phi - 3/2, which is about 0.118, is positive.

These three facts are deliberately modest. The module proves nothing specific to phase space, because its definition of cost does not yet connect the symbols m and e to any physical quantity. The research note attached to the module records the intended direction: for Hamiltonian dynamics, the cost should remain zero, mirroring Liouville's theorem; for non-Hamiltonian processes, the cost should become positive, tracking entropy production. That intended theorem remains unproved, awaiting a definition of the densities in physical terms.

What the module does establish is a reusable template. The same three facts, zero at equality, nonnegativity, and a positive threshold, are proven once and shared across many sibling modules. The certification structure bundles them into a single object, showing that the cost function behaves as a sensible measure of departure from an initial state. This is the groundwork on which a genuine phase space theorem would be built, but it is not that theorem itself.

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]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

This module does not prove Liouville's theorem or any statement about actual Hamiltonian systems. The cost function is not shown to track entropy production for any specific physical process. No claim is made that phase space volume is quantized or discrete in this framework.

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