corePairStretchFactor
plain-language theorem explainer
Defines the local stretch factor for pair events on a discrete lattice as one plus the time step times the maximum absolute forward difference of the velocity field at site i. Researchers constructing derived budgets for incompressible Navier-Stokes flows cite this when replacing free pair parameters with quantities computed from core velocity data. The definition is a direct one-line composition of the operator's time step with the precomputed velocityGradientMag.
Claim. For a core operator $op$ on a lattice with $N$ sites, the stretch factor at site $i$ is $1 + dt(op) · |∇u|(i)$, where $|∇u|(i)$ denotes the supremum of absolute forward differences of all velocity components across all lattice directions at $i$.
background
CoreNSOperator is the structure carrying the minimal physical data of a discrete incompressible flow: lattice topology, spacing $h$, viscosity $ν$, a divergence-free velocity field, and transport flux. It extends EvolutionIdentity but leaves pair-budget and absorption fields undefined so they can be derived from the flow itself. velocityGradientMag returns the largest absolute forward difference of any velocity component in any direction at a given site, using the forwardDiff operator on the supplied topology and spacing.
proof idea
One-line definition that directly returns 1 plus the product of the operator's time step and the value of velocityGradientMag applied to the topology, spacing, and velocity field at the chosen site.
why it matters
Supplies the stretch factor that corePairEvent, corePairStretchFactor_pos, core_stretching_le_pair_budget, and core_pair_budget_absorbed all unfold. It completes the DerivedEstimates layer that turns any CoreNSOperator into a full IncompressibleNSOperator whose pair-budget fields are constructed rather than postulated. This removes the six previously free fields listed in the module documentation and ensures the stretching bound matches the pairwise change by construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.