Foundations

Foundations and Definitions

This page collects the main mathematical objects that appear throughout the paper and shows how they are represented in Lean. The emphasis is on the mathematics first: graphs, binomial edge ideals, the term order, and the conditions used in the main theorems.

Core Algebraic Setup

The ambient ring is a polynomial ring in variables x_i and y_i, one pair for each vertex of the graph. From a graph G, the paper builds the binomial edge ideal generated by the $2 \times 2$ minors [ x_i y_j - x_j y_i ] attached to edges ${i,j}$.

Mathematical object	Lean declaration(s)	File	Notes
Variable type $x_i, y_i$	BinomialEdgeVars	Definitions.lean	Lean represents the two families of variables by a disjoint union of the vertex set with itself
Coordinate functions	x, y	Definitions.lean	Shorthand for the coordinate variables in MvPolynomial (BinomialEdgeVars V) K
Binomial edge ideal $J_G$	binomialEdgeIdeal	Definitions.lean	The ideal generated by the binomials $x_i y_j - x_j y_i$ for edges ${i,j}$ with i < j
Quadratic generators $f_{ij}$	fij, generatorSet	MonomialOrder.lean, ClosedGraphs.lean	fij is the explicit polynomial; generatorSet packages the generating family for Gröbner arguments

Graph-Theoretic Definitions

The first section of the paper is graph-theoretic. The main notion is that of a closed graph, which depends on the chosen linear order of the vertices. The closure construction then produces the smallest closed supergraph.

Mathematical object	Lean declaration(s)	File	Notes
Closed graph	IsClosedGraph	Definitions.lean	Encodes condition (b) from Theorem 1.1 directly against the fixed linear order on vertices
Closure $\bar G$	graphClosure, graphClosure_isClosedGraph, graphClosure_minimal	GraphProperties.lean	The unique minimal closed supergraph from Proposition 1.5
Directed shortest-path condition	IsDirectedWalk	GraphProperties.lean	Used in the formalization of Proposition 1.4
Path graphs	IsPathGraph, pathGraph, pathGraph_isClosedGraph	GraphProperties.lean	Used to package Corollary 1.3 in a paper-faithful connected form
Proposition 1.6 hypothesis	SatisfiesProp1_6Condition	Equidim.lean	Formalizes the transitivity-style graph condition used in the CM criterion

Monomial Order

The paper uses the lexicographic order \(x_1 > \cdots > x_n > y_1 > \cdots > y_n.\)

Lean fixes a linear order on BinomialEdgeVars V and then uses the usual lexicographic monomial order.

Mathematical object	Lean declaration(s)	File	Notes
Monomial order	binomialEdgeMonomialOrder	MonomialOrder.lean	Implemented as MonomialOrder.lex on BinomialEdgeVars V →₀ ℕ
Generator leading monomial	fij_degree	MonomialOrder.lean	Shows the leading monomial of fij is x_i y_j for i < j
Generator leading coefficient	fij_leadingCoeff, fij_leadingCoeff_isUnit	MonomialOrder.lean	Used to satisfy the Gröbner-basis API hypotheses

Lean snippet

noncomputable def binomialEdgeMonomialOrder : MonomialOrder (BinomialEdgeVars V) :=
  MonomialOrder.lex

noncomputable def fij (i j : V) : MvPolynomial (BinomialEdgeVars V) K :=
  x i * y j - x j * y i

theorem fij_degree (i j : V) (hij : i < j) :
    binomialEdgeMonomialOrder.degree (fij (K := K) i j) =
      Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr j) 1 := by

Gröbner-Basis Layer

The Gröbner-basis proofs use explicit remainder computations and Buchberger’s criterion. The formalization packages this through Lean predicates for remainders and Gröbner bases, and then applies them to the quadratic generators of the binomial edge ideal.

Mathematical object	Lean declaration(s)	File	Notes
Polynomial remainder	MonomialOrder.IsRemainder	GroebnerAPI.lean	Records when a polynomial is a remainder with respect to a generating set
Gröbner basis predicate	MonomialOrder.IsGroebnerBasis	GroebnerAPI.lean	The predicate used in the Section 1 and Section 2 theorems
Buchberger criterion	MonomialOrder.isGroebnerBasis_iff_sPolynomial_isRemainder	GroebnerAPI.lean	The main bridge used in the formal proof of Theorem 1.1
Closed-graph theorem	closed_implies_groebner, groebner_implies_closed, theorem_1_1	ClosedGraphs.lean	Main Section 1 theorem in both directions