CoreNSOperator
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
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove existence or uniqueness of solutions for given initial data.
- Does not take the continuum limit as siteCount tends to infinity.
- Does not incorporate external forcing or boundary conditions beyond the finite lattice.
- Does not evaluate numerical values of fundamental constants such as alpha or phi.
formal statement (Lean)
96structure CoreNSOperator (siteCount : ℕ) extends EvolutionIdentity siteCount where
97 topology : LatticeTopology siteCount
98 h : ℝ
99 ν : ℝ
100 h_pos : 0 < h
101 ν_pos : 0 < ν
102 state : State siteCount
103 velocity : VectorField siteCount
104 divergence_free : ∀ x : Fin siteCount, divergence topology h velocity x = 0
105 transportFlux : ScalarField siteCount
106 transportPerm : Equiv.Perm (Fin siteCount)
107 transport_def :
108 contributions.transport = conservativeTransportField transportFlux transportPerm
109 viscous_def :
110 contributions.viscous = fun x => ν * scalarLaplacian topology h state.omega x
111 omega_rms : ℝ
112 omega_rms_pos : 0 < omega_rms
113 normalized_omega_pos : ∀ i : Fin siteCount, 0 < |state.omega i| / omega_rms
114 gradientMag_nonneg : ∀ i : Fin siteCount,
115 0 ≤ velocityGradientMag topology h velocity i
116 dt : ℝ
117 dt_pos : 0 < dt
118 stretching_bound :
119 ∀ i : Fin siteCount,
120 contributions.stretching i ≤
121 Jcost (|state.omega i| / omega_rms * (1 + dt * velocityGradientMag topology h velocity i))
122 + Jcost (|state.omega i| / omega_rms / (1 + dt * velocityGradientMag topology h velocity i))
123 - 2 * Jcost (|state.omega i| / omega_rms)
124 viscous_absorbs :
125 total (fun i =>
126 pairwiseStretchingChange
127 (|state.omega i| / omega_rms)
128 (1 + dt * velocityGradientMag topology h velocity i)) ≤
129 - totalViscous contributions
130
131/-- Transport cancellation is structural: conservative flux on a finite set. -/