GrowthLeDelta.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 8 curated AI-written annotations and 1204 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, Pinned FLT blueprint introduction

10 declarations, 0 contain sorry, 0 declared as axioms

`d(R) ≤ δ(R)`

The growth degree of the Hilbert–Samuel function is at most the number of generators of any ideal of definition — one inequality of the dimension theorem (Stacks Project, tag 00KQ).

Strategy: monomial counting

If q = (x₁, …, xₖ) has radical 𝔪, then qⁿ/qⁿ⁺¹ is generated over R/q by the images of the degree-n monomials in the xᵢ (span_pow_eq_span_monomial), of which there are at most (n+1)^(k-1) (card_sym_le from FLT/Slop/DimensionTheorem/Numeric.lean). A module with N generators each killed by q has length at most N · ℓ(R/q) (length_span_range_le), so summing along the filtration via length_quotient_eq_add gives ℓ(R/qⁿ) ≤ ℓ(R/q) · (n+1)^k (colength_pow_le). Since qⁿ ≤ 𝔪ⁿ, also ℓ(R/𝔪ⁿ) ≤ ℓ(R/qⁿ), whence GrowthLE (hilbertSamuel R) k (growthLE_hilbertSamuel_spanFinrank).

Classically this inequality is deduced from the Hilbert–Serre theorem applied to the associated graded ring gr_q(R), a quotient of a polynomial ring in k variables over R/q (Atiyah–Macdonald, Ch. 11). The counting argument here uses the same underlying idea — the associated graded ring is generated in degree one by k elements — without any graded-ring machinery.

Main results

DimensionTheorem.growthLE_hilbertSamuel_spanFinrank — the growth bound.
DimensionTheorem.growthLE_hilbertSamuel_growthDeg — the defining set of growthDeg is nonempty, so growthDeg is an attained minimum.
DimensionTheorem.growthDeg_le_minGenPrimary — d(R) ≤ δ(R).

Imports (2)

Imported by 2 files

lemma DimensionTheorem.multiset_prod_mem_pow A product of a multiset of elements of an ideal lies in the corresponding power of the ideal line 58 source
Source documentation
A product of a multiset of elements of an ideal lies in the corresponding power of the ideal.
```
private lemma multiset_prod_mem_pow {q : Ideal R} {t : Multiset R}
    (h : ∀ x ∈ t, x ∈ q) : t.prod ∈ q ^ Multiset.card t := by
…
```
def DimensionTheorem.monomial The degree-n monomial in the elements of s indexed by a symmetric power line 68 source
Source documentation
The degree-n monomial in the elements of s indexed by a symmetric power.
```
private def monomial (s : Finset R) {n : ℕ} (a : Sym {x // x ∈ s} n) : R :=
…
```
lemma DimensionTheorem.monomial_mem line 72 source
lemma DimensionTheorem.span_pow_eq_span_monomial qⁿ is spanned by the degree-n monomials in a generating set of q line 84 source
Source documentation
qⁿ is spanned by the degree-n monomials in a generating set of q.
```
private lemma span_pow_eq_span_monomial (s : Finset R) (n : ℕ) :
    Ideal.span (s : Set R) ^ n = Ideal.span (Set.range (monomial s (n := n))) := by
…
```
Mentions: DimensionTheorem.monomial
lemma DimensionTheorem.length_span_range_le A module spanned by finitely many elements each killed by q has length at most (number of generators) * length (R ⧸ q) line 110 source
Source documentation
A module spanned by finitely many elements each killed by q has length at most (number of generators) * length (R ⧸ q).
```
private lemma length_span_range_le {M : Type*} [AddCommGroup M] [Module R M]
    (q : Ideal R) {ι : Type*} [Fintype ι] (w : ι → M)
    (hw : ∀ r ∈ q, ∀ i, r • w i = 0) :
    Module.length R (Submodule.span R (Set.range w)) ≤
      (Fintype.card ι : ℕ∞) * Module.length R (R ⧸ q) := by
…
```
lemma DimensionTheorem.length_pow_quotient_le Documented declaration: length_pow_quotient_le line 154 source
Source documentation
The key counting bound: for an ideal q spanned by a finset s of size k ≥ 1, the length of qⁿ/qⁿ⁺¹ is bounded by the length of R/q times (n+1)^(k-1), a bound on the number of degree-n monomials in k variables.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Finset, LE.le, Nat, OfNat.ofNat, Finset.card, Ideal, Eq, Ideal.span, ENat, Module.length, Subtype, HasQuotient.Quotient, Submodule, HPow.hPow, HAdd.hAdd, Membership.mem, Submodule.map, RingHom.id, Submodule.mkQ and 2 more
Proof uses: Submodule.span, Set.range, Sym, Eq.mpr, id, congrArg, Eq.symm, Ideal.submodule_span_eq, Eq.refl, Set.image, LinearMap, Submodule.map_span, Function.comp, Set, Set.range_comp, HSMul.hSMul, map_smul, Submodule.Quotient.mk, Submodule.mkQ_apply, propext and 17 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma length_pow_quotient_le (s : Finset R) (hs : 1 ≤ s.card) (n : ℕ)
    (q : Ideal R) (hq : q = Ideal.span (s : Set R)) :
    Module.length R
        (Submodule.map (Submodule.mkQ ((q ^ (n + 1) : Ideal R) : Submodule R R))
          ((q ^ n : Ideal R) : Submodule R R)) ≤
      ((n + 1) ^ (s.card - 1) : ℕ) * Module.length R (R ⧸ q) := by
…
```
lemma DimensionTheorem.colength_pow_le Summing the filtration bounds: ℓ(R/qⁿ) is bounded by ℓ(R/q) * (n+1)^k where k = s.card ≥ 1 line 183 source
Source documentation
Summing the filtration bounds: ℓ(R/qⁿ) is bounded by ℓ(R/q) * (n+1)^k where k = s.card ≥ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Finset, LE.le, Nat, OfNat.ofNat, Finset.card, Ideal, Eq, Ideal.span, Ideal.radical, IsLocalRing.maximalIdeal, DimensionTheorem.colength, HPow.hPow, HMul.hMul, HAdd.hAdd
Proof uses: ENat, Module.length, HasQuotient.Quotient, Nat.recAux, Subsingleton, Eq.mpr, id, congrArg, pow_zero, Top.top, Ideal.one_eq_top, Iff.mpr, Submodule, Submodule.Quotient.subsingleton_iff, rfl, Module.length_eq_zero, zero_le, Ideal.pow_le_pow_right, Nat.le_succ, HSub.hSub and 68 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma colength_pow_le (s : Finset R) (hs : 1 ≤ s.card)
    (q : Ideal R) (hq : q = Ideal.span (s : Set R))
    (hrad : q.radical = maximalIdeal R) (n : ℕ) :
    colength R (q ^ n) ≤ colength R q * (n + 1) ^ s.card := by
…
```
Mentions: DimensionTheorem.colength
theorem DimensionTheorem.growthLE_hilbertSamuel_spanFinrank d(R) ≤ δ(R), main lemma: the Hilbert–Samuel function grows at most like n^k where k is the number of generators of any ideal of definition line 229 source
Source documentation
d(R) ≤ δ(R), main lemma: the Hilbert–Samuel function grows at most like n^k where k is the number of generators of any ideal of definition.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Ideal, Eq, Ideal.radical, IsLocalRing.maximalIdeal, DimensionTheorem.GrowthLE, DimensionTheorem.hilbertSamuel, Submodule.spanFinrank
Proof uses: Finset, And, Nat, Finset.card, Submodule, Submodule.span, Exists, Submodule.FG.exists_span_finset_card_eq_spanFinrank, IsNoetherian.noetherian, Ideal.span, Eq.mpr, id, congrArg, Eq.symm, Ideal.submodule_span_eq, Eq.refl, dite, LE.le, OfNat.ofNat, Exists.intro and 47 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
theorem growthLE_hilbertSamuel_spanFinrank {I : Ideal R}
    (h : I.radical = maximalIdeal R) :
    GrowthLE (hilbertSamuel R) I.spanFinrank := by
…
```
Mentions: DimensionTheorem.GrowthLE, DimensionTheorem.hilbertSamuel
theorem DimensionTheorem.growthLE_hilbertSamuel_growthDeg The defining set of growthDeg is nonempty; growthDeg is a true minimum line 263 source
Source documentation
The defining set of growthDeg is nonempty; growthDeg is a true minimum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, DimensionTheorem.GrowthLE, DimensionTheorem.hilbertSamuel, DimensionTheorem.growthDeg
Proof uses: Submodule.spanFinrank, IsLocalRing.maximalIdeal, DimensionTheorem.growthLE_hilbertSamuel_spanFinrank, Ideal.IsPrime.radical, Ideal.IsMaximal.isPrime, Nat.sInf_mem, Set.ofPred, Nat, Exists.intro, Membership.mem, Set
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem growthLE_hilbertSamuel_growthDeg :
    GrowthLE (hilbertSamuel R) (growthDeg R) := by
…
```
Mentions: DimensionTheorem.GrowthLE, DimensionTheorem.hilbertSamuel, DimensionTheorem.growthDeg
theorem DimensionTheorem.growthDeg_le_minGenPrimary d(R) ≤ δ(R) line 271 source
Source documentation
d(R) ≤ δ(R).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, LE.le, Nat, DimensionTheorem.growthDeg, DimensionTheorem.minGenPrimary
Proof uses: Set.Nonempty, Set.ofPred, Exists, Ideal, And, Eq, Ideal.radical, IsLocalRing.maximalIdeal, Submodule.spanFinrank, Exists.intro, Membership.mem, Set, And.intro, Ideal.IsPrime.radical, Ideal.IsMaximal.isPrime, rfl, Nat.sInf_mem, Nat.sInf_le, DimensionTheorem.GrowthLE, DimensionTheorem.hilbertSamuel and 2 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem growthDeg_le_minGenPrimary : growthDeg R ≤ minGenPrimary R := by
…
```
Mentions: DimensionTheorem.growthDeg, DimensionTheorem.minGenPrimary