Information Helmholtz Decomposition Divergence Free

The divergence-free condition

In vector calculus, a vector field is divergence-free when its sources and sinks balance exactly: what flows into any small region flows out again. The classical Helmholtz decomposition splits any sufficiently smooth vector field into a gradient part, which accounts for sources and sinks, and a divergence-free part, which circulates without accumulating. The Recognition Science library works in a finite, discrete setting, where the field assigns a real number to each point of a finite index type, and the condition takes a simpler form.

The declaration DivergenceFree, a definition in the machine-checked library, states that a function w from a finite index type to the real numbers is divergence-free exactly when the sum of all its values is zero. This is the discrete analogue of the integral of the divergence being zero: with no continuous geometry, the condition that total inflow equals total outflow collapses to the requirement that the total of the field over all points vanishes. The definition is a MODEL, a chosen formalization, not a proved theorem about the physical world.

The library uses this definition in a theorem about a non-equilibrium steady state, a system held away from equilibrium by balanced flows. The structure NESSVectorField packages a velocity field, a density, and a free-energy gradient. The theorem helmholtz_split proves that any such field can be written as the sum of a gradient part and a circulating part, point by point. A separate certificate structure records the claim that if the circulating part is divergence-free, then its total sum is zero; the proof is immediate from the definition.

In Recognition Science, this decomposition serves the free-energy principle bridge, which models how a system maintains its internal states against environmental noise. The divergence-free condition identifies the component of the flow that does not change the total quantity, the part that circulates without net production or destruction. This is the discrete, finite-dimensional analogue of the classical Helmholtz split, and it is what the declaration establishes.

The declaration does not claim anything about continuous vector fields, about the classical Helmholtz theorem in three dimensions, or about physical fluid dynamics. It is a definition in a finite setting, and the theorem that uses it is a formal identity, not a statement about empirical flows. The library proves the algebraic split; it does not prove that any particular physical system satisfies the condition.

def DivergenceFree {ι : Type*} [Fintype ι] (w : ι → ℝ) : Prop :=
  ∑ i, w i = 0

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

What this page does not claim

The declaration does not apply to continuous vector fields or to the classical three-dimensional Helmholtz theorem. The library does not prove that any physical system is divergence-free. The definition does not establish the classical Helmholtz decomposition in full generality.

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: