2607.19283v1 / ENOTV/Main.lean

all files

import ENOTV.Positive
import ENOTV.EvenFailure

/-!
# The ENO--TV parity dichotomy

The theorem below is the paper's central result on the uniform grid.
Its hypotheses name exactly the three earlier results the development
imports: the FMT reconstruction/sign theorem, the standard all-order
discrete Gagliardo--Nirenberg inequality, and the previously established
second-order ENO--TV estimate.
-/

noncomputable section

namespace ENOTV

/-- The previously established second-order ENO--TV estimate, which the
paper cites and explicitly does not reprove. -/
def SecondOrderENOCoercivity : Prop := CCoercive 2

/-- Complete parity classification in the compact-sequence formulation. -/
theorem eno_tv_parity_dichotomy
    (hFMT : FMTReconstructionTheorem)
    (hGN : DiscreteGagliardoNirenberg)
    (hSecond : SecondOrderENOCoercivity) :
    ∀ k : ℕ, 2 ≤ k →
      (CCoercive k ↔ k = 2 ∨ Odd k) := by
  intro k hk
  constructor
  · intro hco
    by_cases hk2 : k = 2
    · exact Or.inl hk2
    · right
      rcases Nat.even_or_odd k with heven | hodd
      · have hk4 : 4 ≤ k := by
          obtain ⟨q, hq⟩ := heven
          omega
        exact (not_CCoercive_even hFMT hk4 heven hco).elim
      · exact hodd
  · rintro (rfl | hodd)
    · exact hSecond
    · obtain ⟨q, hq⟩ := hodd
      have hq1 : 1 ≤ q := by omega
      have hform : k = 2 * (q + 1) - 1 := by omega
      rw [hform]
      exact odd_coercive hFMT hGN (q + 1) (by omega)

end ENOTV