Information Helmholtz Decomposition Helmholtz Split

The split

Helmholtz decomposition is a classical result: a sufficiently smooth vector field on a bounded domain splits uniquely into a curl-free (gradient) part and a divergence-free (solenoidal) part. The framework's helmholtz_split declaration establishes a finite-dimensional analogue for a specific structure called a NESS vector field. A NESS vector field, in the framework's vocabulary, is a triple of functions on a finite index type: a velocity v, a density rho, and a free energy gradient. The declaration proves, by direct algebra, that at every index i the velocity equals the sum of two defined components: the negative free energy gradient, called gradPart, and the remainder, called circulatingPart.

The theorem is a tautology in the best sense: it certifies that the split is algebraically valid. The proof is a single ring simplification, not a deep analytic argument. The classical Helmholtz theorem requires boundary conditions and regularity; this finite version requires neither, because it is purely algebraic. The declaration also packages a certificate structure, HelmholtzDecompositionCert, which bundles the split with a divergence-free condition. The certificate holds trivially: the divergence-free condition is stated as an implication, and the proof passes the hypothesis through unchanged.

In Recognition Science, this split models a non-equilibrium steady state (NESS) as a gradient flow plus a circulating component. The gradient part points down the free energy surface; the circulating part represents the rotational, non-dissipative flow that keeps the system away from equilibrium. The framework uses this decomposition in its free energy principle bridge, where the split separates what is driven by free energy minimization from what circulates independently. The declaration does not prove that the circulating part is divergence-free in the analytic sense; it defines divergence-free as a finite sum condition and leaves the implication as a conditional.

What the declaration does not claim is worth stating plainly. It does not establish the classical Helmholtz theorem with its boundary integrals and uniqueness conditions. It does not show that the split is unique, because uniqueness would require additional structure not present in the finite algebraic setting. It does not interpret the components physically; the names gradPart and circulatingPart are definitional choices, not derivations. The theorem is a structural fact about the framework's definitions, a useful algebraic tool for the free energy bridge, not a new physical law.

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 the classical Helmholtz theorem with boundary conditions and regularity. The split is not shown to be unique; uniqueness is not part of the theorem. The names gradPart and circulatingPart are definitional choices, not physical derivations.

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: