Physics Viscosity Ratio From Jcost

The viscosity bound

In fluid dynamics, the ratio of shear viscosity to entropy density, written η/s, measures how strongly a fluid resists flowing relative to its disorder. A lower value means a more nearly perfect fluid. The Kovtun-Son-Starinets bound (KSS bound), proposed in 2004, conjectures that η/s is at least 1/(4π) in natural units, a value that string-theory calculations suggested as a universal floor.

The ledger, a discrete record of recognition events, provides a cost function J(x) = (x + 1/x)/2 - 1. This function is proved in the framework's library to vanish when its input equals 1, to be nonnegative for positive inputs, and to have a positive canonical threshold φ - 3/2, where φ is the golden ratio. The module ViscosityRatioFromJCost defines a domain cost as J(measured / expected), a generic measure of deviation between an observed and an expected value.

In Recognition Science, the framework models the minimum η/s as J(φ)/(4π²) ≈ 0.118/39.5 ≈ 0.003 in natural units. This value is about 30 times smaller than the KSS bound. The framework notes that empirical measurements of the quark-gluon plasma, a state of matter created in heavy-ion collisions, give η/s ≈ 0.1, which is order-of-magnitude consistent with J(φ)/(2 × 2π) ≈ 0.009, though not with the exact minimum.

The Lean code proves three general facts about the cost function: it vanishes at equilibrium, it is nonnegative for positive inputs, and the threshold φ - 3/2 is positive. It proves nothing specific to viscosity, because the module defines domainCost as J(measured / expected) without specifying what "measured" and "expected" mean for a real fluid. The physics claim remains a research note, not a theorem. What the module does establish is a template: any physical ratio that obeys this cost structure inherits the three proved properties.

theorem domainCost_at_equilibrium (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 (measured expected : ℝ) : ℝ := Jcost (measured / expected)

What this page does not claim

The framework proves a specific numerical value for the viscosity ratio of any real fluid. The KSS bound is derived within the framework. The empirical quark-gluon plasma value of η/s ≈ 0.1 is explained by the 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/ViscosityRatioFromJCost.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: