module module high

`IndisputableMonolith.NavierStokes.DiscreteNSOperator`

The DiscreteNSOperator module assembles the concrete discrete incompressible Navier-Stokes operator on the RS lattice from vorticity bookkeeping and RCL pair events. Researchers on J-cost monotonicity and lattice regularity cite it as the surface where transport cancellation and stretching bounds are verified. It is a definition module exporting the operator and supporting fields without internal proofs.

claimThe discrete NS operator on the RS lattice is assembled as conservative transport plus viscous Laplacian plus RCL-bounded stretching, with fields ScalarField, VectorField on LatticeTopology, forwardDiff, backwardDiff, scalarLaplacian, vectorLaplacian, divergence, advection, and conservativeTransportField satisfying total_conservativeTransportField_zero.

background

The module imports DiscreteVorticity, which packages finite vorticity fields on a lattice window together with total, RMS and normalized amplitudes plus transport, viscous and stretching contribution fields. It also imports StretchingPairs, which isolates paired stretching/compression events and the exact Recognition Composition Law balance for such pairs. Local definitions include Axis, ScalarField, VectorField, LatticeTopology, forwardDiff, backwardDiff, scalarLaplacian, vectorLaplacian, divergence, advection, conservativeTransportField and total_conservativeTransportField_zero.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the concrete operator surface for the J-cost monotonicity program. It feeds DiscreteMaximumPrinciple (self-improving sub-Kolmogorov condition), JcostMonotonicity (transport cancellation from conservative flux and stretching bounded by RCL pair budget) and VortexStretching (analytic gaps closed via published papers P1-P3).

scope and limits

Does not prove any theorems or contain sorry-free proofs.
Does not address the continuous Navier-Stokes regularity problem.
Does not define the J-cost function or the full forcing chain.
Does not import or depend on UnifiedForcingChain or phi-ladder results.

used by (3)

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

IndisputableMonolith.NavierStokes.DiscreteMaximumPrinciple module_import
IndisputableMonolith.NavierStokes.JcostMonotonicity module_import
IndisputableMonolith.NavierStokes.VortexStretching module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.NavierStokes.DiscreteVorticity module_import
IndisputableMonolith.NavierStokes.StretchingPairs module_import

declarations in this module (33)

abbrev Axis L34
abbrev ScalarField L36
abbrev VectorField L38
structure LatticeTopology L40
def forwardDiff L44
def backwardDiff L48
def scalarLaplacian L52
def vectorLaplacian L56
def divergence L60
def advection L64
def conservativeTransportField L68
theorem total_conservativeTransportField_zero L73
def velocityGradientMag L86
structure CoreNSOperator L96
theorem core_transport_zero L132
def corePairAmplitude L142
theorem corePairAmplitude_pos L146
def corePairStretchFactor L151
theorem corePairStretchFactor_pos L155
def corePairEvent L161
theorem core_stretching_le_pair_budget L170
def coreOperatorPairBudget L178
theorem coreOperatorPairBudget_nonneg L181
theorem core_pair_budget_absorbed L187
theorem core_stretching_absorbed L195
theorem core_dJdt_nonpos L205
structure IncompressibleNSOperator L215
def pairEventAt L270
def operatorPairBudget L277
theorem operator_transport_zero L280
theorem operatorPairBudget_nonneg L287
theorem totalStretching_le_operatorPairBudget L293
theorem operatorPairBudget_absorbed_by_viscosity L301