Jcost_one_plus_eps_le_sq
plain-language theorem explainer
The inequality supplies a quadratic upper bound on the recognition cost of a stretch factor 1+eps. Navier-Stokes analysts working in the Recognition Science framework cite it when controlling the energy budget of paired vortex-stretching events. The proof rewrites the exact closed-form expression for Jcost(1+eps) and compares denominators with a non-negative division lemma.
Claim. For every real number $eps$ with $eps geq 0$, the canonical cost satisfies $J(1 + eps) leq frac{eps^2}{2}$.
background
The canonical cost Jcost measures the information penalty of a length-scale change and obeys the Recognition Composition Law. The pairwise stretching change is defined as Jcost(x lam) + Jcost(x/lam) - 2 Jcost(x). The sibling result Jcost_one_plus_eps supplies the exact identity Jcost(1 + eps) = eps^2 / (2(1 + eps)) for eps geq 0. This module replaces former sorry markers with complete proofs for the analytic gaps in finite-volume rigidity and uniqueness results from Thapa & Washburn (2026) and Washburn & Zlatanovic (2026).
proof idea
The proof rewrites via the exact identity from Jcost_one_plus_eps. It then applies div_le_div_of_nonneg_left to compare the two denominators, using that the numerator eps^2 is non-negative and that 1 + eps geq 1. The facts 0 < 1 + eps and 0 < 2 are obtained by linarith.
why it matters
The bound is the algebraic step that lets pair_budget_factored_bound conclude pairwiseStretchingChange(a, 1 + d) leq (Jcost a + 1) d^2. It closes one of the three analytic gaps listed in the module header and supports the viscous-dissipation estimates that feed exponential vorticity decay. The result rests on the Recognition Composition Law identity for Jcost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.