dJdt_eq_viscous_plus_stretching
When the total transport contribution to the J-cost derivative vanishes, the derivative equals the sum of the viscous and stretching contributions. Researchers deriving monotonicity bounds for discrete Navier-Stokes models in the Recognition Science framework cite this identity to simplify derivative expressions before applying absorption conditions. The proof is a one-line algebraic reduction that substitutes the EvolutionIdentity split, cancels the transport term, and applies zero_add.
claimLet $e$ be an EvolutionIdentity recording an exact split of the J-cost derivative on a lattice with $siteCount$ sites. If the total transport contribution of $e$ vanishes, then the J-cost derivative equals the sum of the total viscous contribution and the total stretching contribution.
background
The Discrete Vorticity module supplies exact bookkeeping objects for finite vorticity fields on a lattice window. It defines total, RMS, and normalized amplitudes together with separate transport, viscous, and stretching contribution fields. EvolutionIdentity is the structure that packages these fields with the J-cost derivative and the exact decomposition dJdt = totalTransport + totalViscous + totalStretching. The module deliberately isolates this algebraic surface from the hard PDE inequalities so that monotonicity lemmas can be added incrementally. The proof relies on the zero_add theorem from the arithmetic foundations.
proof idea
The proof is a one-line wrapper. It rewrites using the split field of the EvolutionIdentity structure, substitutes the hypothesis that totalTransport equals zero, and applies zero_add to drop the remaining zero term.
why it matters in Recognition Science
The identity is invoked directly by dJdt_nonpos_of_transport_cancel_and_absorption to conclude that the derivative is nonpositive once stretching is absorbed by viscosity. It therefore supplies the algebraic step needed for the J-cost monotonicity program inside the discrete vorticity bookkeeping layer. This layer supports the broader Recognition Science effort to obtain Navier-Stokes behavior from exact functional identities rather than from continuum limits.
scope and limits
- Does not establish when transport cancellation occurs for physical flows.
- Does not prove the absorption inequality between stretching and viscous terms.
- Does not address the continuous-space Navier-Stokes limit.
- Does not incorporate boundary conditions or specific lattice geometries.
Lean usage
theorem example {siteCount : ℕ} (e : EvolutionIdentity siteCount) (htransport : totalTransport e.contributions = 0) : e.dJdt = totalViscous e.contributions + totalStretching e.contributions := dJdt_eq_viscous_plus_stretching e htransportformal statement (Lean)
105theorem dJdt_eq_viscous_plus_stretching {siteCount : ℕ} (e : EvolutionIdentity siteCount)
106 (htransport : totalTransport e.contributions = 0) :
107 e.dJdt = totalViscous e.contributions + totalStretching e.contributions := by
proof body
Term-mode proof.
108 rw [e.split, htransport, zero_add]
109
110/-- If stretching is absorbed by viscosity, then the total derivative is nonpositive. -/