EvolutionIdentity
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove any inequality or sign on the derivative.
- Does not include lattice topology or parameters such as viscosity.
- Does not compute the contribution fields from vorticity data.
- Does not address continuous limits or convergence.
formal statement (Lean)
68structure EvolutionIdentity (siteCount : ℕ) where
69 contributions : ContributionFields siteCount
70 dJdt : ℝ
71 split :
72 dJdt = totalTransport contributions
73 + totalViscous contributions
74 + totalStretching contributions
75
76/-- If the transport contribution has zero total, it cancels exactly. -/