corePairStretchFactor_pos
plain-language theorem explainer
The theorem proves that the derived pair stretch factor 1 plus dt times the local velocity gradient magnitude is strictly positive at every site for any CoreNSOperator on a finite lattice. Discrete fluid modelers and Recognition Science lattice simulations cite it to guarantee that constructed pair events remain well-defined without external positivity assumptions. The proof is a term-mode one-liner that unfolds the definition and applies linear arithmetic to the built-in non-negativity of the time step and gradient magnitude.
Claim. Let $N$ be a natural number, let op be a CoreNSOperator on $N$ sites carrying a divergence-free velocity field, and let $i$ be any site index. Then $0 < 1 + dt(op) · |∇u|_i$, where $|∇u|_i$ is the velocity gradient magnitude at site $i$.
background
The module builds a concrete discrete incompressible Navier-Stokes operator on a finite three-direction lattice. CoreNSOperator is the structure that packages lattice topology, grid spacing h, viscosity ν, the velocity field, and the pointwise divergence-free condition, while leaving pair budgets to be derived rather than assumed. The corePairStretchFactor definition computes the local stretch as 1 + dt times the velocity gradient magnitude extracted from the core velocity field.
proof idea
The proof is a term-mode one-liner. It unfolds corePairStretchFactor to expose the expression 1 + dt · gradientMag, then feeds the non-negativity of dt (from op.dt_pos) and of the gradient magnitude (from op.gradientMag_nonneg) into the linarith tactic, which concludes the sum is positive.
why it matters
This result supplies the stretchFactor_pos field required by corePairEvent, which assembles the full derived PairEvent used inside the IncompressibleNSOperator structure. It completes the DerivedEstimates layer that replaces previously free pair-budget data with quantities computed directly from the core velocity field and its gradient, preserving consistency with the discrete divergence-free condition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.