Overview

What the formalization covers

  • Section 1 characterizes closed graphs by a quadratic Gröbner basis criterion and derives the Cohen–Macaulay condition.
  • Section 2 shows that the edge binomials give a reduced Gröbner basis, and deduces that $J_G$ is radical.
  • Section 3 describes the prime decomposition, the dimension formula, and the minimal primes of $J_G$ in graph-theoretic terms.
  • Section 4 identifies conditional independence ideals in algebraic statistics with binomial edge ideals, and transfers the earlier results to that setting.

The Lean statements stay close to the paper; in a handful of places a formal statement is reformulated (same mathematics, different packaging) and each section page flags those cases in prose.

Main source files

The core development lives in:

Supporting generic lemmas intended for possible upstreaming live in: