Section 3: Prime Decomposition, Dimension, Minimal Primes

Section 3 contains the algebraic core of the paper: the prime ideals P_S, the decomposition of J_G, the dimension formula, and the description of the minimal primes.

For mathematicians, this is the page that explains how the graph controls the prime ideals of the binomial edge ideal. The complete prime decomposition and dimension formula are formalized. What remains open is not the prime theory itself, but the later Cohen–Macaulay consequences derived from it.

Theorem map

Paper result Lean declaration(s) Lean file Fidelity
Lemma 3.1 lemma_3_1 PrimeIdeals.lean Exact
Theorem 3.2 theorem_3_2 PrimeDecomposition.lean Exact
Corollary 3.3 corollary_3_3 PrimeDecompositionDimension.lean Exact
Corollary 3.3 lower bound corollary_3_3_lower_bound PrimeDecompositionDimension.lean Exact
Corollary 3.4 corollary_3_4_equidim PrimeDecompositionDimension.lean Partial
Proposition 3.6 prop_3_6 PrimeDecomposition.lean Equivalent
Corollary 3.7 corollary_3_7, corollary_3_7_unmixed, corollary_3_7_equidim PrimeDecomposition.lean, MinimalPrimes.lean, PrimeDecompositionDimension.lean Partial
Proposition 3.8 prop_3_8 MinimalPrimes.lean Equivalent
Corollary 3.9 corollary_3_9 MinimalPrimes.lean Equivalent

Reading the table

  • Exact means the Lean theorem follows the paper statement closely.
  • Equivalent means the same mathematics is formalized, but the Lean theorem is packaged differently.
  • Partial means a paper statement has only been reached through an equidimensional or otherwise incomplete substitute so far.

Notes

Prime decomposition, minimal primes, and the dimension formula are formalized. The Cohen–Macaulay consequences are still partial:

  • the prime decomposition is formalized;
  • the dimension consequences are formalized;
  • the minimal-prime characterization is formalized;
  • the prime and unmixed cycle-graph equivalences are formalized exactly;
  • and the remaining Cohen–Macaulay statements are currently represented by corollary_3_4_equidim and corollary_3_7_equidim.