Rees Algebras Decomposition with LEAN Verification

An example of using AI to do math research and verification.

Conductor-Reduced Defect Decompositions for Rees Algebras and a Fiber-Corrected Bridge to Linear Type

This is an example of AI-driven automatic mathematics research, verified via LEAN. The thinking model is ChatGPT 5.4 Pro. CLI Agents include ChatGPT 5.4 Codex, Claude Sonnet 4.6. Prompted and organized by Shengrong Wu.

Evaluation by Opus 4.6: The novelty is moderate but genuine within a narrow band. The core contributions — the reduced comparison map \(\phi_n^r\), its exact index formula, and the three-term decomposition \(\nu_r = d_r + \kappa_r - \tau_r\) — are new formal constructions, but they are obtained by fairly standard homological algebra (snake lemma, long exact sequences from multiplication by a regular element, composition series arguments) applied to the existing machinery of Puthenpurakal and Gasanova–Herzog–Kling–Moradi; the paper is transparent about this, explicitly stating it “does not improve the base \(R_1\) theorem itself” but “reorganizes the mechanism.” The fiber-corrected bridge theorem (Theorem B) is the most substantive new result, and the key inequality \(\lambda(\mathcal{E}_n) \leq C\,\lambda(D_n)\) under the \(J_{\mathrm{fib}} = 0\) hypothesis is a clean and useful statement, but the proof route — bounding minimal generators via \(\mathrm{Tor}_1\) and using the nilpotency from the conductor — is a well-worn technique in local algebra, and the hypothesis \(J_{\mathrm{fib}} = 0\) is quite restrictive (it fails whenever \(\mu(I) > d\), which is the generic situation for \(\mathfrak{m}\)-primary ideals). The obstruction result (Appendix A) is essentially a one-line consequence of tensoring with the residue field, so it adds clarity but not depth. In summary, the paper’s novelty lies more in the organizational synthesis — creating a unified defect-decomposition framework linking two previously separate invariants — than in any single technically surprising argument, and its publishability would likely depend on the community’s appetite for such “verified bridge” results connecting known theories rather than on breakthrough new techniques.

Introduction

ReesDefects is a Lean 4 package formalizing the paper research_article_rees_defects.md. A human-readable proof translation from the Lean code is available in formalized_research_article_rees_defects.md.

The package is organized into ten development phases:

1. Finite-length and exact-sequence infrastructure
2. Algebraic wrappers for annihilators, quotients, and support dimension
3. Rees and symmetric algebra interfaces
4. Degreewise defect packages
5. Normalized and first-coefficient abstractions
6. Fiber-cone infrastructure
7. Asymptotic wrappers
8. Main theorems

The central mathematical outputs are:

• The degreewise defect decomposition ν_r(n) = d_r(n) + κ_r(n) - τ_r(n), corresponding to ### The four reduced defects and ### The interaction term as an intersection defect.
• The reduced comparison index formula λ(ker φ_n^r) - λ(coker φ_n^r) = λ(E_n), corresponding to ### Theorem A (conductor-reduced comparison package).
• Theorem A(1)–(3) in paper notation.
• Hypothesis-driven versions of Theorem A(4)–(5), Theorem B, and Corollary C (see Conditional Gaps below).

---

Build and Entry Points

• Package root module: ReesDefects.lean
• Main theorem directory: ReesDefects/Main/
• Build command:

# from the repository root
lake update
lake build

All files in the package build with 0 sorry.

---

Conditional Gaps

Read this section before the verification summary. Every result listed in this README builds without sorry, but several results are proved conditionally — that is, relative to mathematical statements that are assumed as hypotheses rather than derived inside Mathlib. There are three such root assumptions. Each is a standard result in commutative algebra or homological algebra, and none is mathematically in doubt; the gap is purely one of Lean/Mathlib infrastructure.

Gap 1 — Existence of the first-coefficient ideals

File: ReesDefects/FirstCoefficient/ConcreteDefinition.lean

Mathematical content assumed. Given a Noetherian local ring \((A, \mathfrak{m})\) and an \(\mathfrak{m}\)-primary ideal \(I\), Puthenpurakal defines a family of ideals \((I^n)_1 \subseteq A\) (the first-coefficient ideals) satisfying

\[I^n \;\subseteq\; (I^n)_1 \;\subseteq\; \bar{I}^n \qquad \text{for all } n \geq 0,\]

where \(\bar{I}^n\) denotes the integral closure of \(I^n\). These ideals encode the first-coefficient module of the Rees algebra and are the central object of the paper. The formalization assumes their existence and defining properties as axioms, without constructing them internally in Lean.

Why it is a gap. The construction of \((I^n)_1\) from the Rees algebra requires algebraic infrastructure (integral closure, coefficient modules) not yet assembled in Mathlib in the needed form.

Why it is acceptable. The existence and properties of \((I^n)_1\) are given explicitly by definition in the paper. There is no mathematical content being bypassed — only the Lean construction is deferred.

Downstream impact. Parts of Theorem A(2) and Theorem A(3) involving the concrete identification \(U_n = (I^n)_1\).

---

Gap 2 — Tor long exact sequence (Proposition A.1)

File: ReesDefects/Fiber/TorSequenceFuture.lean

Mathematical content assumed. For any short exact sequence of \(A\)-modules \(0 \to K \to F \to M \to 0\), the associated long exact sequence in Tor with respect to \(A/\mathfrak{m}\),

\[\operatorname{Tor}_1^A\!\left(\tfrac{A}{\mathfrak{m}}, F\right) \to \operatorname{Tor}_1^A\!\left(\tfrac{A}{\mathfrak{m}}, M\right) \to \frac{K}{\mathfrak{m}K} \to \frac{F}{\mathfrak{m}F} \to \frac{M}{\mathfrak{m}M} \to 0,\]

is exact. In the paper this is applied with \(M = I^n\) and \(F\) a free module admitting a surjection \(A^g \twoheadrightarrow I^n\), giving the key exact sequence in Appendix Proposition A.1. The right-exact portion \(K/\mathfrak{m}K \to F/\mathfrak{m}F \to M/\mathfrak{m}M \to 0\) is proved unconditionally in RightExactBridge.lean; only the Tor terms on the left are assumed.

Why it is a gap. Mathlib’s derived-functor and \(\operatorname{Tor}\) API does not yet expose the long exact sequence in a form directly applicable to this setting.

Why it is acceptable. The Tor long exact sequence is a foundational theorem in homological algebra, appearing in every standard graduate text (Weibel, Matsumura, Bruns–Herzog). Its mathematical correctness is not in question.

Downstream impact. Proposition A.1 (propositionA1_future) and all of Theorem B.

---

Gap 3 — Polynomial growth of the defect functions

File: ReesDefects/Asymptotics/HilbertLength.lean

Mathematical content assumed. The functions

\[d_r(n) = \lambda_A(D_n) \qquad \text{and} \qquad \kappa_r(n) = \lambda_A(C_n),\]

where \(D_n\) and \(C_n\) are graded pieces of finitely generated modules over the Rees algebra, satisfy polynomial growth bounds: \(d_r(n) = O(n^s)\) for some \(s \geq 0\), and \(\kappa_r(n)\) agrees with a polynomial in \(n\) for all sufficiently large \(n\).

Why it is a gap. The Hilbert–Serre theorem — which guarantees that the length function of any finitely generated graded module over a polynomial ring is eventually polynomial — is not yet available in Mathlib for the graded module setting needed here.

Why it is acceptable. Polynomial growth of Hilbert functions is a classical theorem (Hilbert 1890, Serre 1955), and the paper itself invokes this growth without reproof. No mathematical novelty is bypassed.

Downstream impact. Theorem A(4)–(5), all four statements of Theorem B, and Corollary C.

---

Summary

Gap	Mathematical statement assumed	Downstream impact
First-coefficient ideals	\(I^n \subseteq (I^n)_1 \subseteq \bar{I}^n\) for all \(n \geq 0\)	Theorem A(2) cokernel form, A(3)
Tor long exact sequence	Exactness of \(\operatorname{Tor}_1^A(A/\mathfrak{m}, M) \to K/\mathfrak{m}K \to F/\mathfrak{m}F \to M/\mathfrak{m}M \to 0\)	Proposition A.1, Theorem B
Hilbert–Serre growth	\(d_r(n) = O(n^s)\) and \(\kappa_r(n)\) eventually polynomial	Theorem A(4)–(5), Theorem B, Corollary C

---

Verification Summary

Fully verified in Lean

The following results are proved with 0 sorry and no abstract inputs beyond what Mathlib already provides.

Foundations

Key theorems in the finite-length infrastructure: - ReesDefects.Foundations.isFiniteLength_iff_length_ne_top - ReesDefects.Foundations.finLengthNat_eq_add_of_exact - ReesDefects.Foundations.finLengthNat_modBy_eq_finLengthNat_torsionBy_add_finLengthNat_torsionBy_sub_finLengthNat_range - ReesDefects.Foundations.finLengthNat_ker_eq_finLengthNat_cokernel_add

Paper reference: ### Standard exact sequences

Intermediate defect calculus

The core mathematical identities of the paper are proved unconditionally: - DegreewiseDefectPackage.nu_eq_d_add_kappa_sub_tau - DegreewiseDefectPackage.nu_eq_d_add_kappa_sub_tauIntersection — the main identity \(\nu_r(n) = d_r(n) + \kappa_r(n) - \tau_r(n)\) - ReducedComparisonData.kernelLength_eq_nuDefect_add_equationDefectLength — the index formula

Paper references: ### The four reduced defects, ### The interaction term as an intersection defect

Normalized and first-coefficient layer

• GlobalPackage.r1_iff_closurePow_eq_U — characterizing the first coefficient condition
• ClosurePowerSystem.mem_normalizedReesAlgebra_iff — normalized Rees algebra membership

Main layer — Theorem A(1)–(3)

The main paper theorems are fully proved in Lean: - ConcreteTheoremA123.theoremA1 — The reduced defect comparison formula - ConcreteTheoremA123.theoremA2_defectDecomposition — The defect decomposition - ConcreteTheoremA123.theoremA3_interactionTerm — The interaction term as an intersection defect

Paper reference: ### Theorem A (conductor-reduced comparison package)

---

Conditionally verified

These results are valid Lean theorems proved with 0 sorry, but their statements depend on the abstract inputs from the three gaps above.

Main-layer conditional results (relative to Gap hypotheses)

• ConcreteTheoremA2.theoremA2_cokernel — depends on ConcreteTheoremA123.HasCokernelNuIdentification (Gap 1)
• ConcreteTheoremA45.theoremA4_r1_implies_low_degree and theoremA4_not_r1_implies_high_degree — depend on HasAsymptoticDetection and HasTrivialDConsequences (Gap 3)
• FiberCorrectedBridge.theoremB_equationDefectBound, theoremB_equationDefectGrowth, theoremB_kernelAsymptotic, theoremB_cokernelAsymptotic — depend on FiberCorrectionData (Gaps 2 and 3)
• CorollaryLinearType.corollaryC — depends on LinearTypeCriterion (Gap 3)

Paper reference: ### Theorem B (fiber-corrected bridge to linear type)

---

Paper Navigation

All sections of the paper have a corresponding formal development in Lean:

• Setup and notation: ### Setup and notation
• Standard exact sequences: ### Standard exact sequences
• Fiber-cone definitions: ### Fiber-cone notation
• Reduced comparison maps: ### Conductor-reduced comparison maps
• Reduced defects: ### The four reduced defects
• Interaction term: ### The interaction term as an intersection defect
• Main theorem package: ### Theorem A (conductor-reduced comparison package)
• Fiber-corrected bridge: ### Theorem B (fiber-corrected bridge to linear type)
• Linear-type consequence: ### Corollary C
• Appendix obstruction theorem: ### Proposition A.1, ### Corollary A.2, ### Corollary A.3

---

Repository Structure

View on GitHub

• ReesDefects.lean — root module importing all Main files
• lakefile.lean — package configuration
• lean-toolchain — Lean 4 version specification

Phases 1–10 subdirectories: - Foundations/ — Finite-length infrastructure - Algebra/ — Annihilators, quotients, support dimension - Rees/ — Rees algebra API - Symmetric/ — Symmetric algebra layer - Intermediate/ — Defect calculus - Normalized/ — Normalized Rees algebra - FirstCoefficient/ — First-coefficient package - Fiber/ — Fiber cone and Tor infrastructure - Asymptotics/ — Asymptotic bounds and growth - Main/ — Theorems A, B, and Corollary C

---

How to build locally

Clone the repository and build:

git clone https://github.com/Shengrong-Wu/AI-Driven-Math-Research.git
cd AI-Driven-Math-Research/ReesDefects
lake update
lake build

The build completes with 0 sorry — every proof is either complete or explicitly conditional on one of the three identified gaps.

---

Remarks on verification

This formalization demonstrates that large portions of a nontrivial commutative algebra result can be mechanically verified in Lean, even when the underlying algebraic machinery is only partially available in Mathlib. The three identified gaps are not mathematical weaknesses but rather infrastructure gaps in the proof assistant — the underlying results (first-coefficient ideals, Tor exact sequence, Hilbert polynomial growth) are classical and are standard in the algebra literature.

The honest conditional structure — where the gaps are explicit hypotheses rather than hidden sorry statements — allows readers to understand exactly what additional Mathlib development would be needed to complete the formalization.

Repository: https://github.com/Shengrong-Wu/AI-Driven-Math-Research/tree/main/ReesDefects

License: MIT