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≥3 and fails for even k≥4; 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≥2: 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≥2 it fails on a fixed irregular mesh even though every interface contribution remains nonnegative. This failure is due to the mesh geometry.
The paper classifies exactly which ENO reconstruction orders admit the global total-variation coercivity estimate: order two and every odd order succeed, while every even order at least four fails — resolving a longstanding stability question and identifying parity, through Euler-polynomial obstructions, as the decisive mechanism.
Reproduction
✓* reproduced, conditional on declared hypotheses
Attempted: Assuming the prior FMT reconstruction/sign theorem, the all-order discrete Gagliardo–Nirenberg inequality, and the known second-order ENO–TV estimate, Lean proves that for every k ≥ 2 the literal Lagrange-reconstructed ENO coercivity estimate holds exactly when k = 2 or k is odd.
A 4,000-line development proving the reconstruction/source equivalence, the odd-order energy argument, the Euler-polynomial counterexamples, and even-order noncoercivity — both directions of the dichotomy, for every order. Zero sorry, no project axioms. The three declared hypotheses are all external to the paper's contribution: two are prior results the paper itself cites rather than proves, and the discrete interpolation theorem stands in for higher-order Gagliardo–Nirenberg/cardinal-spline theory absent from mathlib — classical analysis at research-program formalization scale. The paper's strict-comparison robustness refinement is not included. Independent re-verification: all sixteen modules elaborate cleanly; the main theorem depends only on propext, Classical.choice, Quot.sound; the hypotheses were audited as explicit Prop parameters. Details in the run's README.
trace (650 events) · code (19 files)