Section 1

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	Fidelity
Theorem 1.1	theorem_1_1	ClosedGraphs.lean	Exact
Proposition 1.2	prop_1_2	GraphProperties.lean	Exact
Corollary 1.3	cor_1_3 and related wrappers	GraphProperties.lean	Exact
Proposition 1.4	prop_1_4	GraphProperties.lean	Equivalent
Proposition 1.5	prop_1_5	GraphProperties.lean	Exact
Proposition 1.6	prop_1_6_equidim, prop_1_6_herzogHibi, sum_XY_isSMulRegular_mod_diagonalSum	PrimeDecompositionDimension.lean, Equidim.lean	Partial

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

proved Exact

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

proved Exact

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

proved Exact

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

proved 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

proved Exact

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

partial Partial

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

prop_1_6_herzogHibi, sum_XY_isSMulRegular_mod_diagonalSum, prop_1_6_equidim

theorem prop_1_6_herzogHibi (n : ℕ) (G : SimpleGraph (Fin n))
    (hConn : G.Connected) (hClosed : IsClosedGraph G)
    (hCond : SatisfiesProp1_6Condition n G) :
    HerzogHibiConditions n G := by

theorem sum_XY_isSMulRegular_mod_diagonalSum {n : ℕ} {G : SimpleGraph (Fin n)}
    (hHH : HerzogHibiConditions n G) (i : Fin n) (hi : i.val + 1 < n)
    (hik : k ≤ i.val) :
    IsSMulRegular ... := by

theorem prop_1_6_equidim (n : ℕ) (_hn : 0 < n) (G : SimpleGraph (Fin n))
    (hConn : G.Connected) (hClosed : IsClosedGraph G)
    (hCond : SatisfiesProp1_6Condition n G) :
    IsEquidim
      (MvPolynomial (BinomialEdgeVars (Fin n)) K ⧸ binomialEdgeIdeal G) := by

View proof in Equidim.lean View proof in PrimeDecompositionDimension.lean

Notes The full paper statement is still open. The current Lean development has the Herzog--Hibi reduction, the diagonal regularity theorem, and an equidimensional surrogate, but not yet the final Cohen--Macaulay theorem.

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 are formalized at the equidimensional level:

• Example 1.7(a): complete_isEquidim in BEI/Equidim.lean
• Example 1.7(b): path_isEquidim in BEI/PrimeDecompositionDimension.lean

Proposition 1.6

This branch is still partial.

Already proved:

• the graph-combinatorial reduction from the paper;
• the monomial initial ideal and variable-shift reduction;
• the Herzog-Hibi bipartite-graph side;
• the iterated HH regularity theorem sum_XY_isSMulRegular_mod_diagonalSum;
• a direct equidimensional substitute in PrimeDecompositionDimension.lean;
• and most of the real Cohen–Macaulay infrastructure behind the HH side.

Still open:

• the actual depth-based Cohen-Macaulay statement from the paper;
• the last HH-side global Cohen–Macaulay step in Equidim.lean;
• the separate paper-faithful Gröbner CM transfer theorem;
• and therefore the full paper statement of Proposition 1.6.