Code Map

A one-line gloss for every Lean file in BEI/ and toMathlib/, grouped by purpose. For the paper-to-Lean theorem table, see FORMALIZATION_MAP.md; for an editorial overview, see OVERVIEW.md.

`BEI/` — Main development

Foundations and term order

File	Contents
`Definitions.lean`	`BinomialEdgeVars V := V ⊕ V`, the polynomial ring, `binomialEdgeIdeal G`, `IsClosedGraph G`.
`Groebner.lean`	Custom `LinearOrder (BinomialEdgeVars V)` with `x_1 > … > x_n > y_1 > … > y_n`.
`MonomialOrder.lean`	The lex `MonomialOrder` instance; leading-term lemmas for `f_{ij}`.
`GroebnerAPI.lean`	`IsRemainder`, `IsGroebnerBasis`, Buchberger’s criterion.
`AdmissiblePaths.lean`	`pathMonomial`, admissible paths, `groebnerBasisSet`.

Section 1 — closed graphs and Theorem 1.1

File	Contents
`GraphProperties.lean`	`IsChordal`, `IsClawFree`, `graphClosure`; Propositions 1.2 / 1.4 / 1.5 and Corollary 1.3.
`ClosedGraphs.lean`	Theorem 1.1 — closed graph ↔ quadratic Gröbner basis.

Section 2 — Theorem 2.1 and radicality

File	Contents
`HerzogLemmas.lean`	`f_{ij}` algebraic identities and `IsRemainder` helpers used in Theorem 2.1.
`CoveredWalks.lean`	Walk and path arithmetic, S-polynomial helpers, covered-walk lemmas.
`GroebnerBasisSPolynomial.lean`	Theorem 2.1 — Buchberger / S-polynomial proof.
`GroebnerBasis.lean`	Reducedness half of Theorem 2.1 and the paper-facing wrapper.
`Radical.lean`	Corollary 2.2 — `J_G` is radical.

Section 3 — prime decomposition, dimension, minimal primes

File	Contents
`PrimeIdeals.lean`	`primeComponent`, `componentCount`, `numConnectedComponents`.
`PrimeDecomposition.lean`	Theorem 3.2 and Proposition 3.6.
`PrimeDecompositionDimensionCore.lean`	Corollary 3.3, quotient-dimension chain machinery, third-isomorphism dimension helper.
`PrimeDecompositionDimension.lean`	Equidimensional surrogate variants of Corollaries 3.4 and 3.7.
`Prop1_6Equidim.lean`	Path-graph (Example 1.7b) and Proposition 1.6 equidimensional surrogate.
`Corollary3_4.lean`	Corollary 3.4, the connected-case wrapper, Corollary 3.7 CM branch.
`MinimalPrimes.lean`	Propositions 3.8 / 3.9, minimal-prime classification.
`CycleUnmixed.lean`	Cycle component-count lemmas; unmixed branch of Corollary 3.7.

Section 4 — conditional independence ideals

File	Contents
`CIIdeals.lean`	`ciGraph`, `ciIdeal`, `CIStatement`; bridge theorems and transferred results.

Proposition 1.6 (Cohen–Macaulay criterion)

File	Contents
`Equidim.lean`	Herzog–Hibi bipartite ring infrastructure and global CM theorem on the monomial side.
`ReducedHH.lean`	The reduced Herzog–Hibi ring used by the F2 route.
`GroebnerDeformation.lean`	One-parameter deformation `S[t] ⧸ Ĩ`; CM transfer from initial ideal to `J_G`.
`Proposition1_6.lean`	Proposition 1.6 assembled and the path-graph corollaries.

`toMathlib/` — Supporting library

Material intended for possible upstreaming to Mathlib, plus project-local generic infrastructure.

Cohen–Macaulay layer

File	Contents
`CohenMacaulay/Defs.lean`	`ringDepth`, `IsCohenMacaulayLocalRing`, `IsCohenMacaulayRing`.
`CohenMacaulay/Basic.lean`	Quotient-local-ring setup; regular-quotient CM transfer.
`CohenMacaulay/Localization.lean`	Localization, unmixedness, and local-to-global CM transfer.
`CohenMacaulay/Polynomial.lean`	CM lemmas for polynomial rings and finite-free extensions.
`CohenMacaulay/TensorPolynomialAway.lean`	Tensor-away isomorphism; localization preserves global CM.

Graded algebra

File	Contents
`GradedIrrelevant.lean`	Irrelevant ideal of a connected graded algebra; maximality and homogeneous core.
`GradedQuotient.lean`	Graded structure on `A ⧸ I` for homogeneous `I`.
`GradedAssociatedPrime.lean`	Annihilators of homogeneous elements are homogeneous.
`GradedPrimeAvoidance.lean`	Homogeneous prime avoidance and pairwise-incomparable reduction.
`GradedRegularSop.lean`	Graded-algebra structure on `A ⧸ ⟨ℓ⟩` for a regular homogeneous element.
`GradedFiniteFree.lean`	Finite-free Case C route for connected graded CM algebras.
`GradedCM.lean`	Graded local-to-global Cohen–Macaulay theorem.
`GradedEquidim.lean`	Equidimensionality for connected graded CM algebras via finite-free + flat.
`MvPolynomialHomogeneous.lean`	Graded contraction in `MvPolynomial`; non-zero-divisor criterion.

Equidimensionality and dimension

File	Contents
`Equidim/Defs.lean`	Local working definition `IsEquidimRing`.
`IntegralDimension.lean`	`ringKrullDim` invariant under integral injective extensions.
`FiniteFreeEquidim.lean`	Equidimensionality for module-finite, module-flat algebras over a Noetherian domain.
`QuotientDimension.lean`	Monotonicity of quotient dimension; supremum over minimal primes.
`HeightVariableIdeal.lean`	Krull dimension of `MvPolynomial / span(X_i)`.
`HeightDeterminantal.lean`	`height(J_{K_m}) = m − 1` for the complete graph.

Monomial and squarefree primes

File	Contents
`IsPrimeSpanX.lean`	Variable-generated ideals in `MvPolynomial` are prime over a domain.
`MonomialIdeal.lean`	`Ideal.IsMonomial`; prime and primary classification.
`SquarefreeMonomialPrimes.lean`	Edge ideals, vertex covers, minimal-prime ↔ minimal-vertex-cover bijection.

Other helpers

File	Contents
`IdealQuotientHelpers.lean`	Double-quotient and `QuotSMulTop` ↔ `R ⧸ span {x}` bridges.
`MinimalPrimesRegular.lean`	Non-zero-divisor criterion via minimal-prime avoidance in reduced rings.
`PolynomialAwayTensor.lean`	`K[α] ⊗_K K[β][m^{-1}] ≃ K[α ⊔ β][m'^{-1}]`.
`TensorLocalisation.lean`	Localization of a tensor product at a prime contracting to `m`.