corePairEvent
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.