module module high

`IndisputableMonolith.NavierStokes.DiscreteVorticity`

The module defines a finite discrete vorticity field on a lattice window with a given number of sites. Workers on discrete Navier-Stokes regularity cite it for the vorticity data structures that feed operator and stretching analyses. The module supplies only definitions and auxiliary functions for totals, rms quantities, and term contributions.

claimA finite discrete vorticity field on a lattice window of $N$ sites, equipped with a state vector, total J-cost, rms amplitude, and separate transport, viscous, and stretching contribution fields.

background

The module sits inside the Recognition Science treatment of Navier-Stokes regularity via the φ-ladder cutoff. It supplies the discrete vorticity object that the downstream operator and pair modules consume. The upstream PhiLadderCutoff module states that the φ-ladder supplies an ultraviolet cutoff terminating the energy cascade on the RS discrete lattice.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the vorticity representation required by DiscreteNSOperator for the concrete incompressible operator and by StretchingPairs for the RCL pair events that support J-cost monotonicity. It therefore fills the discrete vorticity slot in the algebraic core of the φ-ladder regularity argument.

scope and limits

Does not treat infinite or periodic lattices.
Does not derive the continuous Navier-Stokes equations.
Does not contain numerical evolution or simulation code.
Does not prove any regularity or existence statement.

used by (2)

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

IndisputableMonolith.NavierStokes.DiscreteNSOperator module_import
IndisputableMonolith.NavierStokes.StretchingPairs module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.NavierStokes.PhiLadderCutoff module_import

declarations in this module (17)

structure State L28
def total L32
def rmsSq L36
def rms L40
def normalizedAmplitude L44
def totalJcost L48
structure ContributionFields L52
def totalTransport L58
def totalViscous L61
def totalStretching L64
structure EvolutionIdentity L68
theorem transport_term_cancels L77
theorem viscous_term_dissipative L83
theorem stretching_term_nonneg L91
theorem zero_transport_cancels L98
theorem dJdt_eq_viscous_plus_stretching L105
theorem dJdt_nonpos_of_transport_cancel_and_absorption L111