Information Helmholtz Decomposition Nessvector Field

The decomposition

In vector calculus, the Helmholtz decomposition states that a sufficiently smooth vector field on a bounded domain can be written as the sum of an irrotational (gradient) part and a solenoidal (divergence-free) part. The Recognition Science framework carries this idea into a finite-dimensional setting through a structure called NESSVectorField, where NESS stands for non-equilibrium steady state. The declaration packages three ingredients: a velocity field v, a density rho, and a free-energy gradient. From these it defines two components: the gradPart, which is the negative of the free-energy gradient, and the circulatingPart, which is the velocity plus the free-energy gradient.

The central theorem, helmholtz_split, proves that for every index i in the finite type, the original velocity equals the sum of these two parts: v(i) = gradPart(i) + circulatingPart(i). This is an algebraic identity, verified by the machine-checked library of formal theorems; it holds by definitional unfolding and the ring axiom, with no extra assumptions. The framework also defines a condition called DivergenceFree, which in this finite setting means the sum of the components is zero, and a certificate structure that bundles the split together with a divergence-free condition on the circulating part. A second theorem, helmholtzDecompositionCert_holds, shows that this certificate is always satisfiable: for any finite type, the split holds and the divergence-free condition is exactly the statement that the circulating part sums to zero.

What the declaration does not claim is more telling. It does not assert that every vector field admits a unique decomposition into gradient and divergence-free parts; uniqueness would require boundary conditions or additional regularity that the finite algebraic setting does not supply. It does not claim that the circulating part is divergence-free in the analytic sense of vanishing divergence; the framework's DivergenceFree is a discrete sum condition, not the continuous differential operator. And it does not claim that this decomposition describes actual physical dynamics; the structure is a formal template that the free-energy principle bridge can use, not a theorem about real-world systems.

In plain terms, the declaration establishes a bookkeeping fact: any finite velocity field can be written as a downhill part plus a remainder, and the remainder's divergence-free condition is just that its components sum to zero. This is the algebraic skeleton that later framework results about non-equilibrium steady states can build upon, without pretending that the skeleton alone determines the physics.

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 decomposition is not claimed to be unique without boundary conditions or extra regularity. The circulating part is not claimed to be divergence-free in the analytic sense; DivergenceFree is a discrete sum condition. The declaration does not claim that the decomposition describes actual physical dynamics.

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: