pair_budget_factored_bound
plain-language theorem explainer
The theorem establishes that for a > 0 and d ≥ 0 the pairwise stretching change satisfies pairwiseStretchingChange(a, 1 + d) ≤ (J(a) + 1) d². Analysts studying discrete Navier-Stokes flows or vortex stretching estimates would cite this to control the energy transfer term under the sub-Kolmogorov condition. The short tactic proof rewrites the change via the factored RCL identity and invokes the quadratic upper bound on J(1 + d) together with non-negativity of J.
Claim. Let $a > 0$ and $d ≥ 0$. Then the pairwise stretching change obeys pairwiseStretchingChange$(a, 1+d) ≤ (J(a) + 1) d^2$, where $J$ denotes the J-cost function.
background
The module develops vortex-stretching and viscous-dissipation estimates for discrete Navier-Stokes operators, replacing three former sorry markers with complete proofs drawn from papers P1–P3. The J-cost function satisfies J(x) ≥ 0 for x > 0 by the AM-GM inequality, as recorded in the upstream lemma Jcost_nonneg. The pairwise stretching change is the RCL-derived budget for a pair (a, λ) with λ = 1 + d; the factored form of this budget is supplied by the sibling result pairwise_RCL_balance_factored.
proof idea
The proof first obtains 0 < 1 + d by linarith. It rewrites the left-hand side via the factored RCL identity pairwise_RCL_balance_factored. Non-negativity of J(a) follows from Jcost_nonneg. The quadratic bound J(1 + d) ≤ d²/2 is taken from Jcost_one_plus_eps_le_sq. The final inequality is discharged by nlinarith using non-negativity of J(1 + d).
why it matters
This bound supplies the key estimate that absorbs the pair budget into the viscous dissipation term, closing Gap 3 in the Navier-Stokes analysis. It combines the RCL factored identity from [P2] with the quadratic bound on J(1 + d) from [P1, P2]. The result feeds into the sub-Kolmogorov pair absorption and master absorption theorems in the same module, advancing the Recognition Science program toward a zero-sorry proof of the Navier-Stokes regularity criterion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.