State
plain-language theorem explainer
Discrete vorticity on a finite lattice window is encoded as a map from Fin siteCount to the reals. Fluid modelers building J-cost monotonicity arguments in the Recognition Science Navier-Stokes bridge cite this structure when packaging states for CPM functionals and octave-loop constructions. The declaration is a bare structure definition with a single field and no proof obligations.
Claim. Let $N$ be a natural number. A discrete vorticity field on a lattice window of $N$ sites is a function $omega : Fin N to R$.
background
The Discrete Vorticity module supplies exact bookkeeping objects for the J-cost monotonicity program. It isolates finite vorticity fields on lattice windows together with total, RMS, and normalized amplitudes so that the derivative of total J-cost decomposes exactly into transport, viscous, and stretching contribution fields. The module documentation states that hard PDE inequalities are deliberately kept outside this bookkeeping surface.
proof idea
The declaration is a direct structure definition that introduces the omega field without additional constraints or proofs.
why it matters
This structure serves as the base state type for CPMBridge, RSNSBridgeSpec, and the Functionals record in the classical fluids bridge. It supplies the state space for OctaveLoop constructions in coherence technology and for the discrete model inside the CPM LawOfExistence instantiation. In the Recognition framework it completes the discrete bookkeeping layer that precedes monotonicity lemmas for J-cost evolution, separating exact accounting from the inequality proofs as required by the module setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.