DimLeGrowth.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

`dim R ≤ d(R)`

The Krull dimension of a Noetherian local ring is at most the growth degree of its Hilbert–Samuel function — the hardest inequality of the dimension theorem (Stacks Project, tag 00KQ), following the classical Artin–Rees induction of Atiyah–Macdonald, Ch. 11, adapted to the growth-order formulation of d(R).

Strategy: induction on `d` (`ringKrullDim_le_of_growthLE`)

Base case d = 0 (ringKrullDim_le_zero_of_growthLE_zero): if ℓ(R/𝔪ⁿ) is bounded, it stabilizes, so 𝔪ⁿ = 𝔪ⁿ⁺¹ for some n; Nakayama (Submodule.eq_bot_of_le_smul_of_le_jacobson_bot) gives 𝔪ⁿ = ⊥, so every prime equals 𝔪 and dim R ≤ 0.
Inductive step: it suffices to bound dim (R ⧸ p) for each minimal prime p (ringKrullDim_le_of_forall_minimalPrimes, proved by transporting prime chains to the quotient). R ⧸ p is a Noetherian local domain whose Hilbert–Samuel function is dominated by that of R (hilbertSamuel_quotient_le). If its maximal ideal is ⊥ it is a field of dimension 0; otherwise pick x ≠ 0 in the maximal ideal. The Artin–Rees lemma (Mathlib's Ideal.exists_pow_inf_eq_pow_smul) yields c > 0 with hs_{R/(x)}(n) + hs_R(n - c) ≤ hs_R(n) for n ≥ c (exists_hilbertSamuel_quotient_span_singleton_add_le); the key point is the colon-ideal bound (𝔪ⁿ : x) ≤ 𝔪^(n-c), using that x is a nonzerodivisor. The telescoping lemma GrowthLE.of_le_sub (FLT/Slop/DimensionTheorem/Numeric.lean) then drops the growth degree by one, and Mathlib's ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors (dim (R/(x)) + 1 = dim R for a nonzerodivisor x ∈ 𝔪) closes the induction.

The comparison of the Samuel functions of R and R/(x) via Artin–Rees is the standard textbook argument. The telescoping lemma replaces the classical "a difference of a polynomial has strictly smaller degree" step, which is not available in the growth-order formulation of d(R).

Main result

DimensionTheorem.ringKrullDim_le_of_growthLE : GrowthLE (hilbertSamuel R) d → ringKrullDim R ≤ d.

Imports (5)

Imported by 2 files

lemma DimensionTheorem.hilbertSamuel_zero line 72 source
lemma DimensionTheorem.hilbertSamuel_coe line 80 source
lemma DimensionTheorem.map_mk_maximalIdeal The image of the maximal ideal in a proper quotient is the maximal ideal line 92 source
Source documentation
The image of the maximal ideal in a proper quotient is the maximal ideal.
```
private lemma map_mk_maximalIdeal (I : Ideal R) [Nontrivial (R ⧸ I)] :
    (maximalIdeal R).map (Ideal.Quotient.mk I) = maximalIdeal (R ⧸ I) := by
…
```
lemma DimensionTheorem.length_quotient_map_quotient The length of a double quotient over R ⧸ I equals the length of the corresponding single quotient over R line 103 source
Source documentation
The length of a double quotient over R ⧸ I equals the length of the corresponding single quotient over R.
```
private lemma length_quotient_map_quotient (I J : Ideal R) :
    Module.length (R ⧸ I) ((R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)) =
      Module.length R (R ⧸ (I ⊔ J)) := by
…
```
lemma DimensionTheorem.hilbertSamuel_quotient_eq The Hilbert–Samuel function of R ⧸ I as a colength in R line 113 source
Source documentation
The Hilbert–Samuel function of R ⧸ I as a colength in R.
```
private lemma hilbertSamuel_quotient_eq (I : Ideal R) [Nontrivial (R ⧸ I)] (n : ℕ) :
    hilbertSamuel (R ⧸ I) n = colength R (I ⊔ maximalIdeal R ^ n) := by
…
```
Mentions: DimensionTheorem.hilbertSamuel, DimensionTheorem.colength
lemma DimensionTheorem.hilbertSamuel_quotient_le The Hilbert–Samuel function decreases when passing to a proper quotient ring line 124 source
Source documentation
The Hilbert–Samuel function decreases when passing to a proper quotient ring.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Ideal, Nontrivial, HasQuotient.Quotient, Nat, LE.le, DimensionTheorem.hilbertSamuel
Proof uses: Eq, OfNat.ofNat, GT.gt, Or, Nat.eq_zero_or_pos, Eq.mpr, id, congrArg, Nat.zero_le, Eq.symm, Ideal.radical, HPow.hPow, IsLocalRing.maximalIdeal, DimensionTheorem.radical_pow_eq_of_radical_eq, Ideal.IsPrime.radical, Ideal.IsMaximal.isPrime, LT.lt.ne', DimensionTheorem.colength, Max.max, DimensionTheorem.colength_le_colength and 1 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma hilbertSamuel_quotient_le (I : Ideal R) [Nontrivial (R ⧸ I)] (n : ℕ) :
    hilbertSamuel (R ⧸ I) n ≤ hilbertSamuel R n := by
…
```
Mentions: DimensionTheorem.hilbertSamuel
lemma DimensionTheorem.exists_hilbertSamuel_quotient_span_singleton_add_le Artin–Rees difference bound line 138 source
Source documentation
Artin–Rees difference bound. In a Noetherian local domain, quotienting by 0 ≠ x ∈ 𝔪 drops the Hilbert–Samuel function by at least a shifted copy of itself: there is c > 0 with hs_{R/(x)}(n) + hs_R(n - c) ≤ hs_R(n) for all n ≥ c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, IsDomain, Membership.mem, Ideal, IsLocalRing.maximalIdeal, Ne, OfNat.ofNat, Nontrivial, HasQuotient.Quotient, Ideal.span, Singleton.singleton, Set, Exists, Nat, And, LT.lt, LE.le, HAdd.hAdd and 2 more
Proof uses: GE.ge, Eq, Submodule, Min.min, HSMul.hSMul, HPow.hPow, Top.top, Ideal.exists_pow_inf_eq_pow_smul, Eq.mpr, HMul.hMul, id, congrArg, Ideal.smul_eq_mul, Ideal.mul_top, Eq.refl, Exists.intro, And.intro, Nat.succ_pos, Iff.mpr, Submodule.mem_inf and 82 more
158 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
```
lemma exists_hilbertSamuel_quotient_span_singleton_add_le [IsDomain R] {x : R}
    (hx : x ∈ maximalIdeal R) (hx0 : x ≠ 0)
    [Nontrivial (R ⧸ Ideal.span {x})] :
    ∃ c, 0 < c ∧ ∀ n, c ≤ n →
      hilbertSamuel (R ⧸ Ideal.span {x}) n + hilbertSamuel R (n - c) ≤
        hilbertSamuel R n := by
…
```
Mentions: DimensionTheorem.hilbertSamuel
lemma DimensionTheorem.ringKrullDim_le_zero_of_growthLE_zero Base case: bounded Hilbert–Samuel function forces dimension ≤ 0 line 249 source
Source documentation
Base case: bounded Hilbert–Samuel function forces dimension ≤ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, DimensionTheorem.GrowthLE, DimensionTheorem.hilbertSamuel, OfNat.ofNat, Nat, LE.le, WithBot, ENat, ringKrullDim
Proof uses: HMul.hMul, HPow.hPow, HAdd.hAdd, And, Eq, Exists, Classical.byContradiction, Not, LT.lt, Nat.succ, Or, lt_or_eq_of_le, DimensionTheorem.hilbertSamuel_monotone, Nat.le_succ, absurd, Exists.intro, And.intro, Eq.symm, Nat.recAux, of_eq_true and 71 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
```
lemma ringKrullDim_le_zero_of_growthLE_zero
    (h : GrowthLE (hilbertSamuel R) 0) : ringKrullDim R ≤ 0 := by
…
```
Mentions: DimensionTheorem.GrowthLE, DimensionTheorem.hilbertSamuel
lemma DimensionTheorem.ringKrullDim_le_of_forall_minimalPrimes Reduction to domain quotients: to bound dim R it suffices to bound dim (R ⧸ p) for every minimal prime p line 317 source
Source documentation
Reduction to domain quotients: to bound dim R it suffices to bound dim (R ⧸ p) for every minimal prime p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Nat, Ideal, Membership.mem, Set, minimalPrimes, LE.le, WithBot, ENat, ringKrullDim, HasQuotient.Quotient
Proof uses: Eq.mpr, Order.krullDim, PrimeSpectrum, id, Eq, congrArg, ringKrullDim.eq_1, iSup, LTSeries, RelSeries.length, Set.ofPred, Prod, FiniteDimensionalOrder.match_1, LT.lt, Order.krullDim.eq_1, propext, iSup_le_iff, Ideal.IsPrime, PrimeSpectrum.asIdeal, RelSeries.head and 43 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma ringKrullDim_le_of_forall_minimalPrimes {n : ℕ}
    (h : ∀ p ∈ minimalPrimes R, ringKrullDim (R ⧸ p) ≤ (n : WithBot ℕ∞)) :
    ringKrullDim R ≤ (n : WithBot ℕ∞) := by
…
```
theorem DimensionTheorem.ringKrullDim_le_of_growthLE dim R ≤ d(R), inductive form: any bound on the growth of the Hilbert–Samuel function bounds the Krull dimension line 354 source
Source documentation
dim R ≤ d(R), inductive form: any bound on the growth of the Hilbert–Samuel function bounds the Krull dimension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, CommRing, IsLocalRing, IsNoetherianRing, DimensionTheorem.GrowthLE, DimensionTheorem.hilbertSamuel, LE.le, WithBot, ENat, ringKrullDim
Proof uses: Nat.recAux, OfNat.ofNat, Eq.mpr, id, Eq, congrArg, CharP.cast_eq_zero, DimensionTheorem.ringKrullDim_le_zero_of_growthLE_zero, HAdd.hAdd, DimensionTheorem.ringKrullDim_le_of_forall_minimalPrimes, Ideal, Membership.mem, Set, minimalPrimes, Ideal.IsPrime, And.left, Bot.bot, And, Nontrivial, HasQuotient.Quotient and 53 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
theorem ringKrullDim_le_of_growthLE :
    ∀ (d : ℕ) (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R],
      GrowthLE (hilbertSamuel R) d → ringKrullDim R ≤ (d : WithBot ℕ∞) := by
…
```
Mentions: DimensionTheorem.GrowthLE, DimensionTheorem.hilbertSamuel

FLT/Slop/DimensionTheorem/DimLeGrowth.lean

dim R ≤ d(R)

Strategy: induction on d (ringKrullDim_le_of_growthLE)

Main result

`FLT/Slop/DimensionTheorem/DimLeGrowth.lean`

`dim R ≤ d(R)`

Strategy: induction on `d` (`ringKrullDim_le_of_growthLE`)