module module moderate

`IndisputableMonolith.NavierStokes.DiscreteVorticity`

The DiscreteVorticity module defines a finite discrete vorticity field on a lattice window of siteCount sites together with associated functionals. It supplies the basic data structure for discrete vorticity in the Recognition Science treatment of Navier-Stokes. Downstream modules import it to construct operators and stretching pairs. The module is purely definitional with no theorems or proofs.

claimA finite discrete vorticity field $ω$ on a lattice window $V$ with $N$ sites ($N=$ siteCount), equipped with total J-cost $J(ω)$, rms amplitude, normalized amplitude, ContributionFields for transport/viscous/stretching terms, and EvolutionIdentity.

background

This module sits inside the Recognition Science derivation of Navier-Stokes regularity from the φ-ladder cutoff. The upstream PhiLadderCutoff module formalizes the algebraic core showing that the φ-ladder supplies an ultraviolet cutoff that terminates the energy cascade on the RS discrete lattice. Definitions introduced here include the State type for vorticity configurations, total and rms functionals, totalJcost, ContributionFields, totalTransport, totalViscous, totalStretching, and EvolutionIdentity. The module imports Mathlib and PhiLadderCutoff.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The vorticity field and its functionals feed DiscreteNSOperator, which builds the concrete discrete incompressible Navier-Stokes operator with lattice topology and differential operators, and StretchingPairs, which isolates paired stretching/compression events and the exact RCL balance for J-cost monotonicity. It supplies the discrete data required for the φ-ladder ultraviolet cutoff argument in Navier-Stokes regularity.

scope and limits

Does not treat the continuous Navier-Stokes equations.
Does not implement numerical simulations or discretizations beyond the lattice window.
Does not prove energy-cascade termination or regularity results.
Does not define the φ-ladder or the cutoff mechanism itself.

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