Information Helmholtz Decomposition

Information Helmholtz Decomposition

In vector calculus, the Helmholtz decomposition splits a vector field into two parts: one that flows downhill from a potential (the gradient part) and one that circulates without accumulating (the divergence-free part). The classical theorem, named after Hermann von Helmholtz and proved in the 1850s, guarantees that under mild conditions any smooth vector field in three dimensions admits such a split. In Recognition Science, the same idea applies not to physical space but to the space of possible states a system can occupy. The framework models a system's dynamics as a recognition process, a discrete record of events that tracks how the system's internal state changes. The information Helmholtz decomposition is the claim that this dynamics also splits cleanly into a gradient part and a circulating part.

The module defines a finite-dimensional vector field for non-equilibrium steady states (NESS), which are states where the system keeps moving but its overall statistics stay fixed. The field is described by three ingredients: the velocity at each state, a probability density, and a free-energy gradient. The gradient part is just the negative free-energy gradient, the component that pushes the system toward lower energy. The circulating part is everything left over, defined as the velocity plus the free-energy gradient. The central theorem, helmholtz_split, proves that for every state the velocity equals the sum of these two parts. This is the information analogue of the classical decomposition: one part drives relaxation toward equilibrium, the other sustains the steady flow that keeps the system away from equilibrium.

The module also certifies a stronger property. It defines a certificate structure that packages the split together with a divergence-free condition: if the circulating part has zero total divergence, then its sum over all states is zero. The theorem helmholtzDecompositionCert_holds proves that every finite state space satisfies this certificate. In plain language, the framework guarantees that the circulating part never creates or destroys net probability mass; it only moves probability around in a closed loop. This is what makes the decomposition useful for the free-energy principle bridge: the gradient part accounts for the system's tendency to minimize surprise, and the circulating part accounts for the persistent, non-equilibrium flow that observation shows in living and cognitive systems.

The consequence is that two distinct dynamical roles can be separated and studied independently. Any NESS dynamics in this framework can be read as a sum of a relaxation term and a circulation term, with the circulation provably conserving total probability. That separation is what lets the framework connect its cost-based theory of recognition to the mathematics of non-equilibrium steady states used across physics and biology.

theorem helmholtz_split {ι : Type*} (X : NESSVectorField ι) :
    ∀ i, X.v i = gradPart X i + circulatingPart X i := by
  intro i
  unfold gradPart circulatingPart
  ring

theorem helmholtzDecompositionCert_holds (ι : Type*) [Fintype ι] :
    HelmholtzDecompositionCert ι :=
{ split := helmholtz_split
  divergence_free_condition := by
    intro X h
    exact h }

What this page does not claim

The classical Helmholtz theorem in three-dimensional Euclidean space. Any claim about the physical existence of NESS dynamics beyond the finite-dimensional model. A derivation of the free-energy gradient from the cost function.

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/Information/HelmholtzDecomposition.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: