pairwiseStretching_nonneg
plain-language theorem explainer
Paired stretching events cannot decrease J-cost for positive amplitude and stretch factor. Discrete Navier-Stokes modelers and researchers verifying J-cost monotonicity would cite this algebraic nonnegativity. The proof rewrites the change via the factored RCL balance, invokes J-cost nonnegativity on both arguments, and concludes with nonlinear linear arithmetic.
Claim. For positive reals $x > 0$ and $λ > 0$, the change in J-cost under paired stretching satisfies $0 ≤ Δ(x, λ)$, where Δ is the expression obtained from the Recognition Composition Law balance applied to the pair.
background
J-cost is the function $J(x) = (x + x^{-1})/2 - 1$, nonnegative for $x > 0$ by the AM-GM inequality. The Recognition Composition Law states that $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. This module isolates the algebraic core for paired stretching and compression events in a discrete, PDE-free setting intended for reuse by concrete Navier-Stokes operators. Upstream lemmas establish J-cost nonnegativity via the squared representation $J(x) = (x-1)^2/(2x)$ and direct positivity arguments.
proof idea
One-line wrapper that rewrites the pairwise stretching change via the factored RCL balance identity, introduces the nonnegativity of J-cost for both the amplitude and the stretch factor from the core Cost lemma, and concludes nonnegativity by nonlinear linear arithmetic.
why it matters
This result directly supplies the nonnegativity step for pair event budgets, which track total RCL pair budgets carried by finite families of stretching events. It advances the J-cost monotonicity program inside the discrete Navier-Stokes development, relying on the Recognition Composition Law and the nonnegativity properties established across Cost and Gravity modules. No open scaffolding questions are closed here, but the lemma removes a basic obstruction to budget nonnegativity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.