pairEventAt
plain-language theorem explainer
pairEventAt assembles the paired stretching event record for a lattice site by projecting amplitude and stretch factor data from an incompressible Navier-Stokes operator. Lattice fluid modelers cite it when building the total pair budget for stretching events in discrete flows. The definition works as a direct record constructor that copies the four fields from the operator's precomputed components.
Claim. Let $ns$ be an incompressible Navier-Stokes operator on a lattice with $N$ sites. For site index $i$, the pair event at $i$ is the structure whose amplitude equals the pair amplitude of $ns$ at $i$, whose stretch factor equals the pair stretch factor of $ns$ at $i$, and whose positivity proofs are those supplied by $ns$.
background
IncompressibleNSOperator is the full operator surface extending EvolutionIdentity, carrying a LatticeTopology, lattice spacing $h>0$, viscosity $ν>0$, a divergence-free velocity field, and transport flux. PairEvent is the record type holding a positive real amplitude, a positive real stretch factor, and their positivity proofs. The module constructs these pair events from core flow data rather than treating them as free parameters, so that pair budgets become derived quantities.
proof idea
The definition is a direct record constructor. It sets the amplitude field to ns.pairAmplitude i, the stretchFactor field to ns.pairStretchFactor i, the amplitude_pos field to ns.pairAmplitude_pos i, and the stretchFactor_pos field to ns.pairStretchFactor_pos i.
why it matters
This definition supplies the concrete PairEvent instances required by operatorPairBudget and the three downstream theorems on nonnegativity, viscous absorption, and stretching bound. It completes the construction of IncompressibleNSOperator from core data, embedding the Recognition Composition Law pair events into the discrete Navier-Stokes surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.