Physics Renormalization Group2 From Jcost

A cost function for scales

The renormalization group in physics studies how a theory's parameters change as you zoom in or out on a physical system. Near a phase transition, these flows settle onto special points called fixed points. In three dimensions, the classic pair is the Gaussian fixed point at high energy and the Wilson-Fisher fixed point at low energy, where the critical exponents eta and nu take their measured values.

In Recognition Science, the framework models this idea with a cost function. The function cost, a measure of the recognition effort between two quantities, is applied to the ratio of two scales m and e. The definition is domainCost(m, e) = Jcost(m / e), where Jcost is the framework's forced cost function. The library proves three general facts about this function: it is zero when the two scales are equal, it is never negative for positive scales, and a threshold value phi minus 3/2 is positive. These are properties of the cost function itself, not of any particular physical system.

The library's own documentation is explicit: it proves nothing specific to the renormalization group, because the cost function is defined without reference to a particular physical model. The document notes that the intended connection to Wilson-Fisher fixed points, with RS values of eta = 0.118 and nu = 0.618, remains a research note. The measured values are eta roughly 0.036 and nu roughly 0.630, so the framework's nu is within about two percent, while eta is described as structural.

What the library establishes in plain language is a small, rigorous foundation. It shows that the cost function behaves sensibly at the level of pure mathematics: equal scales cost nothing, and no positive scale ratio carries negative cost. This is a necessary condition for any physical interpretation, but it is not sufficient. The step that would turn this into a theorem about the renormalization group, defining m and e in the subject's own terms, is not present in this library.

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 library does not derive the Wilson-Fisher fixed point or its critical exponents. The framework's values for eta and nu are not proven by this library. The cost function's properties here are not specific to any physical system.

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