EisenbudGreenHarris.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

4 declarations, 4 contain sorry, 0 declared as axioms

The Eisenbud-Green-Harris conjecture

Let $S = k[x_1, \dots, x_n]$ with $x_1 > x_2 > \dots > x_n$ and let $I \subseteq S$ be a homogeneous ideal. The Hilbert function of $I$ is $d \mapsto \dim_k I_d$.

A monomial ideal is an ideal generated by monomials. A monomial ideal $L$ is lex if for any two monomials $u, v$ of the same degree with $u >_{\mathrm{lex}} v$ we have $u \in L$ whenever $v \in L$. Macaulay's theorem says that every homogeneous ideal has the same Hilbert function as a unique lex ideal.

Eisenbud-Green-Harris conjecture. If $I$ contains a regular sequence of forms of degrees $d_1 \le \dots \le d_c$, then there is a lex ideal $L$ such that $I$ has the same Hilbert function as $L + (x_1^{d_1}, \dots, x_c^{d_c})$.

Eisenbud, Green and Harris proposed the conjecture in [EGH93] and [EGH96] to generalise a theorem of Castelnuovo and Cayley-Bacharach type theorems for zero-dimensional subschemes of $\mathbb P^m$. It refines Macaulay's theorem, which is the case $c = 0$.

The conjecture is open in general. It holds when the regular sequence is monomial, by the Clements-Lindström theorem [CL69], and when the degrees grow quickly, namely when $d_i \ge \sum_{j < i} (d_j - 1)$ for all $i \ge 3$: this is due to Caviglia and De Stefani [CDS20], improving on Caviglia and Maclagan [CM08], who assumed the strict inequality. Other known cases are $c \le 2$, and $d_1 = \dots = d_c = 2$ with $c \le 5$ by Güntürkün and Hochster; [CDS20] lists these with references.

The Lex-plus-powers conjecture, attributed to Charalambous and Evans, predicts that the ideal $L + (x_1^{d_1}, \dots, x_c^{d_c})$ above also has the largest graded Betti numbers among all ideals with that Hilbert function containing a regular sequence in those degrees. The Eisenbud-Green-Harris conjecture is its $i = 0$ case [CS18]. It is not formalised here.

The Hilbert function MvPolynomial.hilbertFunction, lex ideals MvPolynomial.IsLexIdeal and the ideal of pure powers MvPolynomial.purePowersIdeal are defined in FormalConjecturesForMathlib.RingTheory.MvPolynomial.LexPlusPowers.

References:

[EGH93] D. Eisenbud, M. Green, J. Harris, Higher Castelnuovo theory, in Journées de Géométrie Algébrique d'Orsay, Astérisque 218 (1993), 187-202.
[EGH96] D. Eisenbud, M. Green, J. Harris, Cayley-Bacharach theorems and conjectures, Bull. Amer. Math. Soc. 33 (1996), 295-324. PDF
[CS18] G. Caviglia, A. Sammartano, On the Lex-plus-powers conjecture, Adv. Math. 340 (2018), 1148-1163. arXiv:1802.03035, Conjecture 1.1.
[CDS20] G. Caviglia, A. De Stefani, The Eisenbud-Green-Harris conjecture for fast-growing degree sequences, Trans. Amer. Math. Soc. 375 (2022), 2777-2792. arXiv:2007.15467, Definition 2.1, Conjecture 2.3 and Theorem A. The statement formalised below is Conjecture 2.3.
[CM08] G. Caviglia, D. Maclagan, Some cases of the Eisenbud-Green-Harris conjecture, Math. Res. Lett. 15 (2008), 427-433.
[CL69] G. F. Clements, B. Lindström, A generalization of a combinatorial theorem of Macaulay, J. Combin. Theory 7 (1969), 230-238.
[FR12] C. A. Francisco, B. P. Richert, Lex-plus-powers ideals, in Syzygies and Hilbert functions, Lect. Notes Pure Appl. Math. 254, 113-144. PDF

Imports (1)

FormalConjecturesUtil

theorem EisenbudGreenHarris.eisenbud_green_harris The Eisenbud-Green-Harris conjecture sorry line 92 source
Source documentation
The Eisenbud-Green-Harris conjecture. Let $I \subseteq k[x_1, \dots, x_n]$ be a homogeneous ideal containing a regular sequence of forms of degrees $d_1 \le \dots \le d_c$. Then there is a lex ideal $L$ such that $I$ has the same Hilbert function as $L + (x_1^{d_1}, \dots, x_c^{d_c})$.

depends on sorry what this means
Statement uses: Nat, Field, LE.le, Fin, Monotone, Ideal, MvPolynomial, Finsupp, Ideal.IsHomogeneous, Submodule, MvPolynomial.homogeneousSubmodule, MvPolynomial.gradedAlgebra, MvPolynomial.IsHomogeneous, Membership.mem, RingTheory.Sequence.IsRegular, List.ofFn, Exists, And, MvPolynomial.IsLexIdeal, Eq and 3 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
61 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eisenbud_green_harris {c : ℕ} (hc : c ≤ n) (d : Fin c → ℕ) (hd : Monotone d)
    (I : Ideal (MvPolynomial (Fin n) k))
    (hI : I.IsHomogeneous (homogeneousSubmodule (Fin n) k))
    (f : Fin c → MvPolynomial (Fin n) k) (hfd : ∀ i, (f i).IsHomogeneous (d i))
    (hfI : ∀ i, f i ∈ I)
    (hf : RingTheory.Sequence.IsRegular (MvPolynomial (Fin n) k) (List.ofFn f)) :
    ∃ L : Ideal (MvPolynomial (Fin n) k), IsLexIdeal L ∧
      ∀ e, hilbertFunction I e = hilbertFunction (L + purePowersIdeal hc d) e := by
…
```
Mentions: c
theorem EisenbudGreenHarris.eisenbud_green_harris.variants.macaulay Macaulay's theorem: every homogeneous ideal has the same Hilbert function as a lex ideal sorry line 108 source
Source documentation
Macaulay's theorem: every homogeneous ideal has the same Hilbert function as a lex ideal. This is the case $c = 0$ of eisenbud_green_harris, where the ideal of pure powers is zero (MvPolynomial.purePowersIdeal_zero).

depends on sorry what this means
Statement uses: Nat, Field, Ideal, MvPolynomial, Fin, Finsupp, Ideal.IsHomogeneous, Submodule, MvPolynomial.homogeneousSubmodule, MvPolynomial.gradedAlgebra, Exists, And, MvPolynomial.IsLexIdeal, Eq, MvPolynomial.hilbertFunction
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eisenbud_green_harris.variants.macaulay (I : Ideal (MvPolynomial (Fin n) k))
    (hI : I.IsHomogeneous (homogeneousSubmodule (Fin n) k)) :
    ∃ L : Ideal (MvPolynomial (Fin n) k), IsLexIdeal L ∧
      ∀ e, hilbertFunction I e = hilbertFunction L e := by
…
```
theorem EisenbudGreenHarris.eisenbud_green_harris.variants.clements_lindstrom The Clements-Lindström theorem [CL69]: the conjecture holds for an ideal that already contains the pure powers $x_1^{d_1}, \dots, x_c^{d_c}$ sorry line 119 source
Source documentation
The Clements-Lindström theorem [CL69]: the conjecture holds for an ideal that already contains the pure powers $x_1^{d_1}, \dots, x_c^{d_c}$.

depends on sorry what this means
Statement uses: Nat, Field, LE.le, Fin, Monotone, Ideal, MvPolynomial, Finsupp, Ideal.IsHomogeneous, Submodule, MvPolynomial.homogeneousSubmodule, MvPolynomial.gradedAlgebra, MvPolynomial.purePowersIdeal, Exists, And, MvPolynomial.IsLexIdeal, Eq, MvPolynomial.hilbertFunction, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
47 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eisenbud_green_harris.variants.clements_lindstrom {c : ℕ} (hc : c ≤ n) (d : Fin c → ℕ)
    (hd : Monotone d) (I : Ideal (MvPolynomial (Fin n) k))
    (hI : I.IsHomogeneous (homogeneousSubmodule (Fin n) k)) (hIp : purePowersIdeal hc d ≤ I) :
    ∃ L : Ideal (MvPolynomial (Fin n) k), IsLexIdeal L ∧
      ∀ e, hilbertFunction I e = hilbertFunction (L + purePowersIdeal hc d) e := by
…
```
Mentions: c
theorem EisenbudGreenHarris.eisenbud_green_harris.variants.caviglia_deStefani The conjecture holds when the degrees grow quickly enough, namely when $d_i \ge \sum_{j < i} (d_j - 1)$ for all $i \ge 3$ sorry line 134 source
Source documentation
The conjecture holds when the degrees grow quickly enough, namely when $d_i \ge \sum_{j < i} (d_j - 1)$ for all $i \ge 3$. This is [CDS20, Theorem A]; Caviglia and Maclagan [CM08] had proved it under the strict inequality. Indices here are 0-based, so $i \ge 3$ becomes 2 ≤ i. The subtraction is on ℕ, which is harmless because a regular sequence of degrees d forces 1 ≤ d j.

depends on sorry what this means
Statement uses: Nat, Field, LE.le, Fin, Monotone, OfNat.ofNat, Finset.sum, Finset.Iio, HSub.hSub, Ideal, MvPolynomial, Finsupp, Ideal.IsHomogeneous, Submodule, MvPolynomial.homogeneousSubmodule, MvPolynomial.gradedAlgebra, MvPolynomial.IsHomogeneous, Membership.mem, RingTheory.Sequence.IsRegular, List.ofFn and 7 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
70 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eisenbud_green_harris.variants.caviglia_deStefani {c : ℕ} (hc : c ≤ n) (d : Fin c → ℕ)
    (hd : Monotone d) (hgrow : ∀ i : Fin c, 2 ≤ (i : ℕ) → ∑ j ∈ Finset.Iio i, (d j - 1) ≤ d i)
    (I : Ideal (MvPolynomial (Fin n) k))
    (hI : I.IsHomogeneous (homogeneousSubmodule (Fin n) k))
    (f : Fin c → MvPolynomial (Fin n) k) (hfd : ∀ i, (f i).IsHomogeneous (d i))
    (hfI : ∀ i, f i ∈ I)
    (hf : RingTheory.Sequence.IsRegular (MvPolynomial (Fin n) k) (List.ofFn f)) :
    ∃ L : Ideal (MvPolynomial (Fin n) k), IsLexIdeal L ∧
      ∀ e, hilbertFunction I e = hilbertFunction (L + purePowersIdeal hc d) e := by
…
```
Mentions: c