IndisputableMonolith.Information.HelmholtzDecomposition
Finite-dimensional Helmholtz split for NESS vector fields on a discrete index set: every field factors as a gradient piece plus a divergence-free circulating piece. Information and non-equilibrium steady-state arguments in the monolith cite the split and the certificate that it holds. The module is mostly definitions plus a short certification lemma.
claimOn a finite index type, a NESS vector field $V$ admits a Helmholtz decomposition $V = \nabla \Phi + C$ with $C$ divergence-free (the circulating part). The module packages the gradient part, circulating part, the split identity, and a certificate that the decomposition holds.
background
In continuum mechanics the Helmholtz theorem writes a sufficiently regular vector field as the sum of an irrotational (gradient) field and a solenoidal (divergence-free) field. The same algebraic split is useful for discrete flows on a finite index set when one studies non-equilibrium steady states (NESS).
This module works in that discrete setting. A NESS vector field is a real-valued assignment of fluxes or forces to the finite index. The gradient part is the conservative contribution recoverable from a scalar potential; the circulating part is the residual that carries zero discrete divergence. The Recognition Science information layer uses the split to separate reversible cost from irreversible circulation in steady recognition flows.
Only Mathlib is imported; the constructions are elementary finite-dimensional linear algebra over the reals.
proof idea
Definition module with a thin certification layer. It introduces the NESS vector-field type, extractors for the gradient and circulating summands, the pointwise split identity, and a DivergenceFree predicate on the circulating summand. A certificate structure packages these data; a short lemma asserts that the certificate holds for the canonical split. No deep analytic estimates appear; the argument is finite-dimensional bookkeeping.
why it matters in Recognition Science
Separating gradient cost from circulating flux is a standard move when one analyses steady-state recognition currents and information balances. Downstream information and thermodynamics developments can quote the split and the certificate rather than re-deriving the decomposition. Within the broader Recognition framework the circulating piece is the natural carrier of irreversible eight-tick and ladder dynamics, while the gradient piece ties back to J-cost potentials. The module itself has no recorded reverse dependencies yet; it is infrastructure for later NESS and information theorems.
scope and limits
- Does not treat continuum or infinite-dimensional Helmholtz theorems.
- Does not prove uniqueness of the potential beyond the finite discrete setting.
- Does not identify the circulating part with a physical current or measure entropy production.
- Does not connect the split to the J-cost functional or the forcing chain T0–T8.
- Does not supply numerical bounds or stability estimates for the decomposition.