IndisputableMonolith.Information.HelmholtzDecomposition
The module defines finite-dimensional NESS vector fields on an index type together with their Helmholtz decomposition into gradient and circulating components. Researchers in Recognition Science cite it when modeling steady-state information flows or force decompositions. It supplies a certificate that the split holds. The module consists entirely of definitions and a basic holding theorem built on Mathlib linear algebra.
claimLet $I$ be an index type. A NESS vector field is a map $V:I→ℝ^d$. The Helmholtz decomposition states $V=∇ϕ + C$ where $∇ϕ$ is the gradient part, $C$ is the circulating part, and $C$ satisfies the divergence-free condition.
background
In the Information domain the module treats vector fields as carriers of recognition or information propagation. NESSVectorField encodes a finite-dimensional non-equilibrium steady-state field on an index set. Supporting definitions include gradPart (irrotational component), circulatingPart (solenoidal component), helmholtz_split (the explicit decomposition map), DivergenceFree (the zero-divergence predicate), and HelmholtzDecompositionCert together with its holding theorem.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the vector-field primitives required by higher-level information-theoretic results in the Recognition framework. It supports decomposition steps that appear in analyses of steady-state dynamics and feeds into parent constructions on forcing chains and phi-ladder structures.
scope and limits
- Does not treat infinite-dimensional or continuous fields.
- Does not derive numerical constants such as phi or alpha.
- Does not prove uniqueness of the decomposition beyond the supplied certificate.
- Does not address time-dependent or stochastic extensions.