EvolutionIdentity
plain-language theorem explainer
EvolutionIdentity records the exact decomposition of the J-cost time derivative into transport, viscous, and stretching totals over a finite lattice. Researchers building discrete incompressible Navier-Stokes models in the Recognition Science framework cite this structure when assembling the operator surface. The declaration is a structure definition that enforces the split equation by construction.
Claim. A record consisting of contribution fields $c$ (with transport, viscous, and stretching components over $n$ sites), a real number $dJ/dt$, and the identity $dJ/dt = $ total transport of $c$ + total viscous of $c$ + total stretching of $c$.
background
The Discrete Vorticity module supplies exact bookkeeping objects for the J-cost monotonicity program on finite lattices. It separates the decomposition of the derivative from later PDE inequalities, defining finite fields, totals, and the three contribution pieces. ContributionFields is the structure holding the three scalar maps from Fin siteCount to reals; total sums any such map over the sites.
proof idea
This is a structure definition that bundles ContributionFields with the derivative value while requiring the split identity to hold by construction. No lemmas or tactics are applied; the equality is part of the data.
why it matters
The structure is extended by CoreNSOperator and IncompressibleNSOperator. It directly supports the theorems dJdt_eq_viscous_plus_stretching and dJdt_nonpos_of_transport_cancel_and_absorption that rewrite the derivative after transport cancellation and establish nonpositivity under absorption. In the framework it supplies the bookkeeping surface needed for discrete Navier-Stokes approximations that preserve J-cost properties tied to the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.