2607.19283v1 / README.md

all files

# ENO--TV parity dichotomy: Lean reproduction

## Result

The formalization proves the uniform-grid parity classification (Theorem A):
for every reconstruction order `k ≥ 2`, the ENO--TV coercive estimate holds
for every compactly supported sequence if and only if `k = 2` or `k` is odd.

The closest literal statement is
`ENOTV.eno_tv_parity_dichotomy_literal` in
`ENOTV/Representation.lean`:

```lean
theorem eno_tv_parity_dichotomy_literal
    (hFMT : FMTReconstructionTheorem)
    (hGN : DiscreteGagliardoNirenberg)
    (hSecond : SecondOrderENOCoercivity) :
    ∀ k : ℕ, 2 ≤ k →
      (LiteralCoercive k ↔ k = 2 ∨ Odd k)
```

Here `LiteralCoercive` is

```lean
∃ C : ℝ, 0 ≤ C ∧ ∀ u : ℤ →₀ ℝ,
  ∑ i, |u (i+1) - u i|^(k+1) ≤
    C * ‖u‖_∞^(k-1) * Q_k(u),
```

where `Q_k` is defined directly from the difference of the two derivatives
of the degree-`k` Lagrange interpolants of the cumulative cell averages at
each interface. Thus the theorem does not define the reconstructed jump by
the desired localized formula.

There is also
`ENOTV.eno_tv_parity_dichotomy_paper`, stated for functions `ℤ → ℝ`
with finite support. `coercive_iff_CCoercive` proves that this and the
`Finsupp` implementation quantify over exactly the same data, while
`amplitude_coe`, `jumpMoment_coe`, and `source_coe` prove equality of the
three quantities in the estimate.

## Explicit theorem inputs

No mathematical proposition is installed as a Lean `axiom`. The final
theorem has three explicit arguments:

1. `FMTReconstructionTheorem`. This is the earlier
   Fjordholm--Mishra--Tadmor theorem used by the paper: classical ENO
   reconstruction has the localized jump formula and every localized term
   has the sign of the cell-average jump. Its statement relates the literal
   Lagrange reconstruction to the finite-difference formula, rather than
   merely assuming positivity of an abstract source.
2. `DiscreteGagliardoNirenberg`. For every `m ≥ 2` and every finitely
   supported `v`,

   \[
   \sum_i |Dv_i|^{2m}
     \le C_m\|v\|_\infty^{2m-2}\sum_i |D^m v_i|^2.
   \]

   This is the analytic interpolation theorem used in Section 3. Mathlib
   contains the first-order Gagliardo--Nirenberg--Sobolev inequality, but
   not this all-order one-dimensional inequality, cardinal B-splines, or
   the required spline stability result. The discrete theorem is therefore
   exposed as one named analytic input.
3. `SecondOrderENOCoercivity`, namely `CCoercive 2`. This is exactly the
   known second-order theorem which the paper cites and does not reprove.

These inputs are minimal for the proof as organized here. In particular,
the ENO source/local-energy comparison, all odd-order summation-by-parts
identities, the Euler-polynomial obstruction, its compactly supported
realization, every global bound for that realization, and the
noncoercivity contradiction are proved in Lean. The even-order half uses
only the FMT input; the discrete interpolation input is used only for odd
orders at least three.

The paper proves its discrete interpolation theorem by a cardinal
B-spline lift followed by a classical continuous Gagliardo--Nirenberg
inequality. I checked the local mathlib tree and searched available Lean
library sources for a reusable higher-order interpolation or cardinal
spline development; none was available. Rebuilding the missing Sobolev
and B-spline theory was the remaining library-sized analytic dependency,
so it is disclosed rather than hidden behind `sorry` or an axiom.

## Correspondence with the paper

- `Seq`, `diff`, `diffIter`, `jumps`, and `FiniteSupport` implement lattice
  sequences and \(D\).
- `enoLeft` is the paper's strict-left/weak-right ENO recursion.
  `enoLeft_bounds` and `enoLeft_mono_step` verify its stencil geometry.
- `cumulativeInterpolant`, `literalTrace`, and
  `literalReconstructedJump` implement the naive cell-average
  reconstruction: interpolate the cumulative values on the selected
  `k+1` boundaries, differentiate, and subtract the two interface traces.
- `literalSource_eq_cSource` proves that the naive source is the localized
  source under the stated FMT theorem.
- `gamma` is

  \[
  \gamma_{k,d}
    =(-1)^{k-1-d}\frac{d!(k-1-d)!}{k!}
    =\frac{(-1)^{k-1-d}}{k\binom{k-1}{d}}.
  \]

- `cEnergy` is the paper's local-amplitude energy
  \(\sum_j A_j^{(k)}|D^{k-1}a_j|\).
  `source_dominates_energy` and `source_le_energy` prove uniform
  comparability with \(Q_k\), using the full local-amplitude lemma and the
  unique-owner form of the localized source.
- `square_energy_le_localized` proves the odd-order
  summation-by-parts/square-energy estimate. Combined with the discrete
  Gagliardo--Nirenberg input it gives `odd_coercive`.
- `eulerPoly` is constructed from mathlib's Bernoulli polynomials.
  The development proves its forward-difference identity, reflection
  symmetry, integer endpoint zeros, and the properties of the truncated
  alternating Euler blocks.
- `multiJumps` and `multiDatum` are the compactly supported even-order
  family. Lean proves exact jump recovery, zero total jump, disjoint
  support, amplitude and bulk-moment estimates, block/junction formulas,
  endpoint estimates, and the global source upper bound.
- `not_CCoercive_even_core` chooses the scale parameter after an arbitrary
  proposed constant and derives a strict contradiction. Thus the negative
  result is genuinely universal, not a check of finitely many examples.

The extra robustness assertion in Theorem A about making every affected
ENO comparison strict on a relatively open set, and the paper's later
Theorems B--D, are not part of the classification theorem formalized here.

## File map

- `ENOTV/Basic.lean`: paper-level definitions and stencil facts.
- `ENOTV/Compact.lean`: exact finite-support implementation.
- `ENOTV/Energy.lean`: finite summation by parts and square energy.
- `ENOTV/Localization.lean`: literal reconstruction, FMT interface, and
  local-amplitude lemma.
- `ENOTV/SourceComparison.lean`: source ownership and two-sided energy
  comparison.
- `ENOTV/Positive.lean`: odd-order coercivity.
- `ENOTV/Euler.lean`: Euler-polynomial identities.
- `ENOTV/Counterexample.lean`: compact Euler blocks and primitives.
- `ENOTV/Estimates.lean`, `ENOTV/Bulk.lean`,
  `ENOTV/Endpoint.lean`, `ENOTV/Junction.lean`: quantitative bounds.
- `ENOTV/EvenEnergy.lean`: complete block/junction source estimate.
- `ENOTV/EvenFailure.lean`: scale choice and even-order contradiction.
- `ENOTV/Main.lean`: parity classification.
- `ENOTV/Representation.lean`: equivalence to the paper's formulations.
- `ENOTV/Audit.lean`: kernel axiom audit.

## Verification

From this directory:

```sh
lake build ENOTV
lake env lean ENOTV/Representation.lean
lake env lean ENOTV/Audit.lean
rg -n '\bsorry\b|\badmit\b|^axiom\b' ENOTV
```

The build succeeds. The audit prints, for all three main formulations:

```text
depends on axioms: [propext, Classical.choice, Quot.sound]
```

These are mathlib's standard logical principles. There are no `sorry`,
`admit`, project axioms, or unsafe declarations.