Information Helmholtz Decomposition Circulating Part

The circulating part

In the mathematics of dynamical systems, a vector field assigns a direction and magnitude to every point in a space. The Helmholtz decomposition, named after Hermann von Helmholtz, is the classical result that a sufficiently well-behaved vector field can be written as the sum of a gradient (a part that flows downhill from a potential) and a divergence-free part (a part that circulates without accumulating). The Recognition Science framework's ledger, a discrete record of events, uses a finite-dimensional version of this idea for its study of nonequilibrium steady states (NESS), systems that maintain a constant flow while energy passes through them.

The declaration circulatingPart is a definition, not a theorem. It takes a NESS vector field X and at each index i returns the value X.v i + X.freeEnergyGradient i. In plain words, it is the part of the flow that remains after the gradient contribution has been subtracted. Its companion gradPart is the negative of the free-energy gradient. The two definitions are chosen so that the original field is exactly their sum, and the framework proves this as the theorem helmholtz_split: for every index i, X.v i = gradPart X i + circulatingPart X i. The proof is a direct algebraic expansion, verified by the machine-checked library of formal theorems.

The framework also defines DivergenceFree for a finite index type as the condition that the sum of the values over all indices is zero. A certificate structure packages the split together with a conditional statement: if the circulating part is divergence-free, then its total sum is zero. The framework proves this certificate holds for every finite index type, so the decomposition is available as a formal tool. This matters because the split is the bridge the framework uses to separate dissipative, energy-lowering motion from conservative circulation in its models of information flow.

What the declaration does not claim is just as important. The name circulatingPart does not by itself prove that the part is divergence-free; that is a separate condition the framework states as a hypothesis in its certificate. The framework does not claim that this finite-dimensional split is the full infinite-dimensional Helmholtz theorem of classical analysis, which requires differentiability and boundary conditions. It also does not claim that the split is unique, since the decomposition into gradient and circulating parts depends on the choice of the free-energy gradient function. What is proved is the algebraic identity, and that is the solid ground the framework builds on.

def circulatingPart {ι : Type*} (X : NESSVectorField ι) : ι → ℝ :=
  fun i => X.v i + X.freeEnergyGradient i

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 declaration does not prove that the circulating part is divergence-free. The split is not claimed to be the full infinite-dimensional Helmholtz theorem of classical analysis. The decomposition is not claimed to be unique without further conditions on the free-energy gradient.

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: