Section 1: Closed Graphs and Quadratic Gröbner Bases

Section 1 proves that closed graphs are exactly the graphs whose quadratic binomials form a Gröbner basis. It also records the main graph-theoretic consequences and the closure construction.

Theorem map

Paper result	Lean declaration(s)	Lean file
Theorem 1.1	theorem_1_1	ClosedGraphs.lean
Proposition 1.2	prop_1_2	GraphProperties.lean
Corollary 1.3	cor_1_3 and related wrappers	GraphProperties.lean
Proposition 1.4	prop_1_4	GraphProperties.lean
Proposition 1.5	prop_1_5	GraphProperties.lean
Proposition 1.6	proposition_1_6, binomialEdgeIdeal_cm_of_monomialInitialIdeal_cm, prop_1_6_herzogHibi, monomialInitialIdeal_isCohenMacaulay	Proposition1_6.lean, GroebnerDeformation.lean, Equidim.lean

Proposition 1.4 is packaged equivalently in Lean (same mathematics, slightly different phrasing); the card below has the paper statement and the Lean statement side by side.

Paper vs Lean

Each card below places the paper statement next to the current Lean theorem.

Paper vs Lean Theorem 1.1 Closed Graphs and Quadratic Gröbner Bases

Paper Statement

Let $G$ be a simple graph on $[n]$. Then the quadratic generators of the binomial edge ideal $J_G$ form a Gröbner basis with respect to the lexicographic order $x_1 > \cdots > x_n > y_1 > \cdots > y_n$ if and only if $G$ is closed with respect to the given labeling.

Lean Formalization

theorem_1_1

theorem theorem_1_1 (G : SimpleGraph V) :
    binomialEdgeMonomialOrder.IsGroebnerBasis (generatorSet (K := K) G)
      (binomialEdgeIdeal (K := K) G) ↔
    IsClosedGraph G :=
  ⟨groebner_implies_closed G, closed_implies_groebner G⟩

View proof in ClosedGraphs.lean

Notes This is the central entry point for the Section 1 formalization. The paper statement is represented directly rather than through a surrogate or weaker wrapper.

Paper vs Lean Proposition 1.2 Closed Graphs Are Chordal and Claw-Free

Paper Statement

If $G$ is closed, then $G$ is chordal and has no induced claw.

Lean Formalization

prop_1_2

theorem prop_1_2 (G : SimpleGraph V) (h : IsClosedGraph G) :
    IsChordal G ∧ IsClawFree G :=
  ⟨closedGraph_isChordal G h, closedGraph_isClawFree G h⟩

View proof in GraphProperties.lean

Notes The Lean conclusion packages the paper's two graph-theoretic consequences as `IsChordal G ∧ IsClawFree G`.

Paper vs Lean Corollary 1.3 Closed Bipartite Graphs Are Paths

Paper Statement

A bipartite graph is closed if and only if it is a line.

Lean Formalization

cor_1_3, cor_1_3_connected_forward, pathGraph_isClosedGraph

theorem cor_1_3 (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj]
    (hBip : ∃ (φ : V → Bool), ∀ ⦃u v : V⦄, G.Adj u v → φ u ≠ φ v)
    (hClosed : IsClosedGraph G) :
    G.IsAcyclic ∧ ∀ v, G.degree v ≤ 2 := by

theorem cor_1_3_connected_forward (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj]
    (hBip : ∃ (φ : V → Bool), ∀ ⦃u v : V⦄, G.Adj u v → φ u ≠ φ v)
    (hClosed : IsClosedGraph G) (hConn : G.Connected) :
    IsPathGraph G := by

theorem pathGraph_isClosedGraph (n : ℕ) :
    IsClosedGraph (pathGraph n) := by

View proof in GraphProperties.lean

Notes The paper's "line graph" formulation is formalized through a connected path-graph wrapper plus the converse theorem for the canonical path graph.

Paper vs Lean Proposition 1.4 Characterization by Directed Shortest Paths

Equivalent

Paper Statement

A graph $G$ on $[n]$ is closed with respect to the given labeling if and only if, for any two distinct vertices $i \neq j$ of the associated directed graph $G^*$, all shortest paths from $i$ to $j$ are directed.

Lean Formalization

prop_1_4

theorem prop_1_4 (G : SimpleGraph V) :
    IsClosedGraph G ↔
    ∀ (i j : V), i < j →
    ∀ (w : G.Walk i j), w.length = G.dist i j → IsDirectedWalk G w.support := by

View proof in GraphProperties.lean

Notes This is equivalent rather than verbatim: the paper quantifies over all distinct vertices, while the Lean statement fixes the orientation by requiring `i < j`.

Paper vs Lean Proposition 1.5 Unique Minimal Closed Supergraph

Paper Statement

For every simple graph $G$ on $[n]$, there exists a unique minimal graph $\bar{G}$ on $[n]$ that is closed with respect to the given labeling and contains $G$ as a subgraph.

Lean Formalization

prop_1_5

theorem prop_1_5 (G : SimpleGraph V) :
    ∃! H : SimpleGraph V,
      G ≤ H ∧ IsClosedGraph H ∧
      ∀ H' : SimpleGraph V, G ≤ H' → IsClosedGraph H' → H ≤ H' := by

View proof in GraphProperties.lean

Notes Lean names the closure construction explicitly and proves the same uniqueness and minimality statement as in the paper.

Paper vs Lean Proposition 1.6 A Sufficient Cohen–Macaulay Criterion

Paper Statement

Let $G$ be a connected graph on $[n]$ that is closed with respect to the given labeling. Suppose further that whenever $\{i,j+1\}$ with $i < j$ and $\{j,k+1\}$ with $j < k$ are edges of $G$, then $\{i,k+1\}$ is an edge of $G$. Then $S/J_G$ is Cohen--Macaulay.

Lean Formalization

proposition_1_6, binomialEdgeIdeal_cm_of_monomialInitialIdeal_cm

theorem proposition_1_6
    {K : Type} [Field K] {n : ℕ} (hn : 2 ≤ n) {G : SimpleGraph (Fin n)}
    (hConn : G.Connected) (hClosed : IsClosedGraph G)
    (hCond : SatisfiesProp1_6Condition n G) :
    IsCohenMacaulayRing
      (MvPolynomial (BinomialEdgeVars (Fin n)) K ⧸ binomialEdgeIdeal G) := by

View proof in Proposition1_6.lean View proof in GroebnerDeformation.lean View proof in Equidim.lean

Notes The paper statement is formalized as `proposition_1_6`. The proof combines the Herzog--Hibi reduction, the monomial-side CM theorem, and a Gröbner deformation transfer back to `J_G`. The direct equidimensional route remains in the repo as a separate surrogate argument.

Notes

Theorem 1.1

Closed graphs are characterized by the quadratic generators of the binomial edge ideal forming a Gröbner basis.

Corollary 1.3

The Lean statement keeps the connected-graph hypothesis explicit and spells out the path-graph conclusion directly.

Examples 1.7

The supporting examples now split by strength:

• Example 1.7(a): complete_isEquidim in BEI/Equidim.lean
• Example 1.7(b): pathGraph_binomialEdgeIdeal_isCohenMacaulay and pathGraph_binomialEdgeIdeal_ringKrullDim in BEI/Proposition1_6.lean
• The direct surrogate route is also still available as path_isEquidim in BEI/PrimeDecompositionDimension.lean

Proposition 1.6

The main declaration is proposition_1_6 in BEI/Proposition1_6.lean. Its proof is assembled in the same order as the paper’s strategy:

• prop_1_6_herzogHibi packages the graph hypotheses into the HH bipartite conditions;
• monomialInitialIdeal_isCohenMacaulay proves the monomial-side CM theorem;
• binomialEdgeIdeal_cm_of_monomialInitialIdeal_cm and groebnerDeformation_cm_transfer carry CM back from the initial ideal to J_G;
• and the direct equidimensional route in PrimeDecompositionDimension.lean remains available as a separate surrogate argument, not as the main theorem recorded on this page.