corePairEvent
corePairEvent builds the PairEvent record at each lattice site from a CoreNSOperator by inserting the normalized vorticity amplitude and the local strain stretch factor together with their positivity witnesses. Discrete fluid modelers cite it when they need to derive the total pair budget directly from velocity and vorticity data instead of treating pair quantities as independent inputs. The definition is a record constructor that delegates amplitude and stretchFactor to the sibling corePairAmplitude and corePairStretchFactor functions.
claimLet $op$ be a CoreNSOperator on a lattice with $N$ sites. For each site index $i$, the pair event $E_i$ is the record whose amplitude equals the normalized absolute vorticity at $i$ and whose stretch factor equals $1 + dt$ times the local velocity-gradient magnitude, with both fields strictly positive.
background
The module supplies a concrete discrete incompressible Navier-Stokes operator on a finite three-direction lattice. CoreNSOperator is the structure that carries only the physical flow data: lattice topology, grid spacing $h$, viscosity $ν$, divergence-free velocity field, and transport flux; pair-budget and absorption fields are derived from these data rather than postulated. PairEvent is the record type (introduced in StretchingPairs) that packages an amplitude, a stretch factor, and proofs that both are positive.
proof idea
The definition is a one-line record constructor. It fills the amplitude field by calling corePairAmplitude (normalized vorticity), the stretchFactor field by calling corePairStretchFactor (one plus dt times gradient magnitude), and the two positivity fields by invoking the already-proved lemmas corePairAmplitude_pos and corePairStretchFactor_pos.
why it matters in Recognition Science
corePairEvent supplies the concrete PairEvent instances required by indexedPairBudget, which in turn feeds coreOperatorPairBudget and the absorption theorems core_pair_budget_absorbed and core_stretching_absorbed. It therefore closes the derivation layer that replaces free pair data with quantities computed from the core velocity gradient and Laplacian, satisfying the module's goal of constructing the full IncompressibleNSOperator surface from CoreNSOperator alone.
scope and limits
- Does not prove global existence or uniqueness for the discrete system.
- Does not address the continuous-space limit of the lattice discretization.
- Does not incorporate external body forces beyond the core transport flux.
- Does not compute global energy or enstrophy decay rates.
formal statement (Lean)
161def corePairEvent {siteCount : ℕ} (op : CoreNSOperator siteCount)
162 (i : Fin siteCount) : PairEvent where
163 amplitude := corePairAmplitude op i
proof body
Definition body.
164 stretchFactor := corePairStretchFactor op i
165 amplitude_pos := corePairAmplitude_pos op i
166 stretchFactor_pos := corePairStretchFactor_pos op i
167
168/-- The stretching bound from the core operator matches the pairwise change
169because both sides use the same amplitude and stretch factor. -/