pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.NavierStokes.VortexStretching

show as:
view Lean formalization →

VortexStretching supplies J-cost bounds and pair-absorption controls for discrete vortex stretching on the RS lattice. It is cited by the Discrete Maximum Principle to absorb stretching contributions into the viscous term. The module reduces paired events to quadratic inequalities via the Recognition Composition Law and the elementary bound J(1+eps) <= eps^2/2.

claimThe module establishes $J(1 + e) = (e^2)/(2(1+e))$, hence $J(1 + e) <= e^2/2$ for $e >= 0$, together with viscous-rate and pair-budget controls derived from the discrete velocity gradient on the three-direction lattice.

background

The module imports the CoreNSOperator from DiscreteNSOperator, which encodes finite three-direction lattice topology, discrete differentials, and the velocity-gradient and Laplacian fields that generate pair budgets and viscous absorption. It further imports StretchingPairs, whose doc-comment isolates the algebraic core of J-cost monotonicity: paired stretching/compression events whose exact Recognition Composition Law balance J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) yields finite pair budgets indexed by lattice sites.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the Discrete Maximum Principle, whose doc-comment states that the sub-Kolmogorov condition becomes self-improving under the discrete Navier-Stokes evolution, eliminating it as an external hypothesis and making the lattice regularity result fully unconditional. It supplies the J-cost and absorption lemmas required to close the stretching term in that argument.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)