Physics Heat Capacity Anomaly From Jcost

The anomaly and its limits

Near a phase transition, the heat capacity of a material often diverges. The standard way to describe this is a power law: C_p ∝ |T - T_c|^(-α), where T_c is the critical temperature and α is the critical exponent. In the simplest mean-field theory, α equals 0, meaning the heat capacity jumps but does not diverge. In the three-dimensional Ising model, a more accurate description of magnetic transitions, α is about 0.110.

Recognition Science proposes a connection. Its cost function, a measure of the forced price of recognition events, has a unique form J(x) = (x + 1/x)/2 - 1. The framework's research note suggests that the critical exponent might be α = J(φ)/2, where φ is the golden ratio. Since J(φ) ≈ 0.118, this gives α ≈ 0.059, a value between the mean-field prediction of 0 and the Ising value of 0.110.

The machine-checked library of formal theorems proves something much narrower. It defines a cost function on a ratio of two real numbers, m and e, as J(m/e). It then proves three general facts: this cost is zero when m equals e, it is never negative for positive inputs, and the golden-ratio constant φ - 3/2 is positive. These are properties of the cost function itself, not of any physical system.

The gap between the physics and the proof is explicit. The library's own documentation states that it proves nothing specific to heat capacity, because the cost function is defined without reference to any particular physical quantities. To become a theorem about critical exponents, the library would need a definition of m and e in terms of the system's actual parameters, such as temperature and energy. That definition does not exist in the formal library.

What the library does establish is a template. It shows that the cost function has the basic mathematical properties one would want for a physical quantity: it vanishes at equilibrium, stays nonnegative, and has a natural threshold. Whether those properties connect to the measured critical exponent remains an open question, not a proved result.

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

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

The library proves that the critical exponent α equals J(φ)/2. The value 0.059 is a measured or derived critical exponent for any real material. The cost function is defined in terms of temperature or energy.

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