CoreNSOperator
plain-language theorem explainer
CoreNSOperator assembles the physical lattice data for a discrete incompressible Navier-Stokes flow on a finite site set. It carries a divergence-free velocity field, positive grid spacing and viscosity, conservative transport realized by flux difference under permutation, and explicit J-cost bounds on local stretching together with viscous absorption of the total pair budget. Researchers deriving monotonicity of J-cost or pair budgets in discrete fluid models cite this structure as the base data layer. The declaration is a structure definition
Claim. A lattice flow on $N$ sites consists of a directed topology, positive spacing $h$ and viscosity $ν$, a discrete state with vorticity field $ω$, a divergence-free velocity field $u$, a scalar flux, and a site permutation. Transport contribution equals flux at site $i$ minus flux at the permuted site; viscous contribution equals $ν$ times the scalar Laplacian of $ω$. Normalized vorticity amplitudes are positive, local strain factors satisfy the J-cost inequality bounding pairwise stretching change, and total stretching change is absorbed by the negative total viscous term.
background
LatticeTopology supplies plus and minus successor maps on each of three axes for a finite site set. VectorField and ScalarField are simply functions from sites to real vectors or scalars. State is the discrete 2D Galerkin state carrying vorticity. Conservative transport is realized exactly by the difference flux(i) − flux(perm(i)). The module constructs the full incompressible operator by deriving pair amplitude, stretch factor, and absorption from these core fields rather than postulating them.
proof idea
This is a structure definition. The transport and viscous contributions are set by direct equality to the conservativeTransportField and ν-scaled scalarLaplacian. The stretching bound and viscous absorption are recorded as field hypotheses; downstream theorems such as core_dJdt_nonpos and core_pair_budget_absorbed simply unfold these fields and apply the general dJdt_nonpos_of_transport_cancel_and_absorption lemma.
why it matters
CoreNSOperator supplies the concrete data from which coreOperatorPairBudget, corePairAmplitude, and core_pair_budget_absorbed are derived. These feed core_dJdt_nonpos, which establishes non-positive J-cost change from transport cancellation and viscous absorption alone. In the Recognition framework the construction discretizes the incompressible operator while preserving the J-cost monotonicity that follows from the Recognition Composition Law and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.