Resolution of the ENO-TV conjecture: a parity dichotomy
We resolve the ENO–TV conjecture, a discrete coercivity problem in compactness theory for entropy-stable approximations of hyperbolic conservation laws. For order-k essentially non-oscillatory (ENO) reconstruction from compactly supported cell averages, it asks whether the nonnegative ENO source times the (k-1)st power of the amplitude uniformly controls the (k+1)st absolute-jump moment. We prove a parity dichotomy: the estimate holds for odd k\ge3 and fails for even k\ge4; the known second-order case completes the classification. Localization gives a selection-independent finite-difference functional uniformly comparable to the source and reduces the conjecture to discrete interpolation. For odd orders, summation by parts reveals a hidden square; a discrete Gagliardo–Nirenberg inequality yields coercivity. For even orders, Euler-polynomial blocks from the functional's polynomial kernel yield counterexamples that persist under arbitrarily small perturbations making all affected ENO comparisons strict. We also prove two coercive estimates for every k\ge2: control of jumps larger than a fixed fraction of the amplitude and of local blocks modulo sampled polynomials of degree at most k-2. Via the Cayley–Sylvester decomposition, we compute the dimensions of homogeneous first-cohomology spaces for the lattice shift on polynomial jump profiles. At fourth order, for a cubic flux and a globally strictly convex entropy, a total-degree-seven component of a reduced entropy-flux mismatch represents a nonzero class on profiles of degree at most two and hence has no translation-invariant finite-stencil C^7 local primitive at the zero constant state. Odd-order coercivity persists on globally quasi-uniform meshes, whereas for each k\ge2 it fails on a fixed irregular mesh even though every interface contribution remains nonnegative. This failure is due to the mesh geometry.
The paper completely classifies when ENO reconstruction supplies the coercivity needed for compactness of entropy-stable schemes. The parity mechanism explains why odd high orders succeed while even high orders admit robust polynomial-profile counterexamples.
Reproduction
✓ reproduced
Attempted: Uniform-grid ENO–TV coercivity holds exactly for k = 2 and odd k, while failing structurally for even k ≥ 4. Declared target: R3 — faithfully state the result, verify its finite calculations, and prove the hidden-square energy lemma underlying the odd-order argument.
R1–R3 achieved across Repro.lean, Computations.lean, and Core.lean: the numerical obstruction calculations and exact Euler-block instances verified, then Lemma 3.3's energy identity and localized bound proved. R4 remains beyond this run. Independent re-verification: all three files elaborate cleanly with zero sorry; every declaration depends only on propext, Classical.choice, Quot.sound (or no axioms at all) — no native_decide anywhere, the computations are kernel-checked.
trace (15 events) · code (3 files)