cert
plain-language theorem explainer
Packages three elementary facts about the viscosity domain cost into a single certificate: cost vanishes on the diagonal, is non-negative for positive arguments, and the canonical threshold is positive. Anyone deriving the RS η/s bound from J-cost cites this witness. The definition is a pure structure assembly of three sibling lemmas.
Claim. There exists a viscosity certificate asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is non-negative; (iii) the canonical threshold is strictly positive.
background
The module derives the shear-viscosity-to-entropy ratio $\eta/s$ from the Recognition Science J-cost. In natural units the KSS bound is $\eta/s \ge 1/(4\pi)$; RS predicts a structural minimum $\eta/s = J(\varphi)/(4\pi^2) \approx 0.003$, order-of-magnitude consistent with quark-gluon plasma data near $0.1$.
The domain cost is the J-cost specialized to a mass-energy pair $(m,e)$. At equilibrium ($m=e$) the cost vanishes, matching the unique minimum of $J$ at argument $1$. Non-negativity of cost is inherited from the global fact that every recognition event has non-negative J-cost (ObserverForcing.cost_nonneg).
ViscosityCert is the structure that packages exactly the three positivity and equilibrium facts needed before any numerical $\eta/s$ bound can be stated.
proof idea
One-line structure constructor. Each field is filled by a sibling lemma already proved in the same module: domainCost_at_equilibrium supplies diagonal vanishing, domainCost_nonneg supplies non-negativity for positive arguments, and canonicalThreshold_pos supplies strict positivity of the threshold. No additional reasoning occurs inside the definition.
why it matters
This certificate is the formal gate that any later viscosity-ratio theorem must pass through: without diagonal vanishing, non-negativity, and a positive threshold, the RS claim $\eta/s = J(\varphi)/(4\pi^2)$ cannot even be stated as a lower bound. It sits inside the Physics domain of the monolith and ties the abstract J-cost (T5 uniqueness, RCL) to a concrete hydrodynamic observable. The module status is structural (zero sorry, zero axiom), so the certificate closes the scaffolding for the viscosity side of the forcing chain rather than leaving an open hypothesis interface. No downstream consumers are yet wired; the certificate is the ready witness for that next step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.