corePairStretchFactor_pos
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not address convergence to the continuous Navier-Stokes equations.
- Does not depend on specific numerical values of viscosity or grid spacing beyond their positivity.
- Does not apply to compressible or non-divergence-free velocity fields.
- Does not supply upper bounds on the stretch factor magnitude.
formal statement (Lean)
155theorem corePairStretchFactor_pos {siteCount : ℕ} (op : CoreNSOperator siteCount)
156 (i : Fin siteCount) : 0 < corePairStretchFactor op i := by
proof body
Term-mode proof.
157 unfold corePairStretchFactor
158 linarith [mul_nonneg op.dt_pos.le (op.gradientMag_nonneg i)]
159
160/-- The derived pair event at each site. -/