Import Nagata's prime-generated factoriality theorem

[Vilin97]

Imports all 19 upstream Lean modules from arthur742ramos/nagatafactoriality at 2efdf7f86085972bd758449ca43c76a2e7bdf4af, plus the generated project entry point. The development proves Nagata’s factoriality criterion for arbitrary prime-generated multiplicative sets, with concrete and abstract localization interfaces and polynomial applications through Laurent and fraction-field localizations. This extends the pool’s existing AndersonConjecture single-prime localization criterion; it is not a claim that Nagata’s criterion was previously absent from the pool.

The Lean/Mathlib 4.34 port preserves the upstream statements and attribution, uses public modules, and updates the localization and normalized-GCD interfaces. The secondary prime-or-unit argument now uses Mathlib’s localization-at-units equivalence: closure under squaring forces every member of such a submonoid to be a unit. This removes 98 lines while preserving the existing theorem signatures and applications.

The project records provenance: AI with a transparent evidence note. At the pinned upstream revision, 1,092 of 1,308 surviving noncomment Lean code lines (83.5%), including 94.8% of the core lemmas and 96.6% of the theorem module, trace to explicitly Copilot-coauthored commits. In particular, 5b169887 adds the prime-generated proof development, and ef73ee27 adds abstract localization proofs and the fraction-field application. This classification is an inference from documented coauthorship, not attribution of individual keystrokes.

Current main is integrated losslessly: all 218 main project cards remain unchanged, plus the Nagata card. The project card and module index were regenerated. Local validation covers all 20 project modules compiled serially without warnings, the declaration linter over their import closure, index consistency, and the unchanged static source/metadata checks. Compiler and linter validation ran under a shared lock and a 20 GiB aggregate memory limit. Fresh CI must still pass the style, full quality, public axiom, compiled environment, full-pool, and documentation checks; no local pass of those pending checks is claimed.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Changes requested by automated review

Reviewed exact head 2035cffd8ab6473666ce5da1ee62744d50dc8bf6. The exact-head NagataFactoriality protected run fails its zero-warning build gate. The PR also leaves the required provenance metadata absent because it is pending author evidence. Repair the warning failure and supply an honest provenance value before merge, then rerun complete CI.

[Vilin97]

/review

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low risk] Adds a new mathematical library module for Nagata's theorem.

No outstanding review finding blocks merging, subject to fresh required checks and independent upstream verification.

Summary

Imports the upstream Nagata factoriality development, including concrete and abstract localization interfaces and polynomial applications.

• Adds the project card with provenance: AI and supporting attribution notes.
• Consolidates the secondary prime-or-unit localization proof while retaining its theorem interfaces.
• The pinned upstream source and license were not independently verified in this review; fresh aggregate CI remains pending.

_{Reviews (13) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."}

[Vilin97]

Changes requested by automated review

Reviewed exact current head febc72f8be747c6872b5a5f6b34a52e68f2effbc.

The exact-head Build pool, Build project, and documentation checks fail, and the project card still lacks the required honest provenance metadata. Supply the provenance value, repair the build/warning failure, and rerun complete protected CI.

Acceptance condition: repair the named defects on a new head and make all required protected checks green. Do not change repository policy or add waivers.

[Vilin97]

Exact-head reconciliation\n\nReviewed exact current head febc72f8be747c6872b5a5f6b34a52e68f2effbc. The PR's imported Nagata files and metadata remain as in the prior review; current protected CI is failing and the project card still lacks the required provenance field. Supply an honest provenance value, repair the build/warning failure, and rerun all required gates.

[Vilin97]

Changes requested by automated review

Reviewed head 50e507016e9bcaa0489e039c0e413f0f41b7e483. Meaningful arbitrary prime-generated criterion; existing AndersonConjecture/Jensen/KrullDomain/Nagata covers localization at powers of one prime, not this full statement.

1. Complete the pinned-toolchain integration. The exact-head build fails. Its concrete error includes:

   error: LeanPool.lean:1:0: cannot import non-`module` LeanPool.NagataFactoriality from `module`
   

   The file/dependency audit finds 20 changed Lean files without the required module form. Repair the affected dependency closure, regenerate the module index, and obtain a warning-free full pool build plus the unchanged linter, quality and axiom gates. A project-only or previous-head build does not resolve this failure.

2. Resolve the substantive source/interface defect. The new registry card omits the required provenance. Record the actual human/AI/mix proof provenance and regenerate the card. Also disclose and compare the existing LeanPool/AndersonConjecture/Jensen/KrullDomain/Nagata.lean:nagata_criterion; the arbitrary-prime-generated generalization is the relevant additional scope.

Review coverage: complete changed-file inventory and full diff retained; 20 changed project files, 1,807 lines, import reachability and executable trust-token scan; advertised endpoints and supporting definitions examined with bounded implementation sampling and existing review findings reconciled. Potential reusable value: General localization and factoriality interfaces. Source/provenance and prior-art evidence were considered separately from CI; these findings do not assert that every proof line was manually read. Earlier automated scores are advisory and are not approval of this failing head.

[Vilin97]

Repair review of exact head fe1cea32f88cb37332ff28256e6fe4d26bef7035: approve the repaired content, subject to successful current-head required CI. This is a COMMENT review because GitHub prevents approving a PR authored by the authenticated account.

The missing provenance is now documented as AI, with the inference and its limits recorded in the card. At upstream pin 2efdf7f86085972bd758449ca43c76a2e7bdf4af, git blame -w -M -C attributes 1,092 of 1,308 surviving noncomment Lean code lines to explicitly Copilot-coauthored commits, including 94.8% of the core lemmas and 96.6% of the theorem module. The inspected proof additions in 5b169887 and ef73ee27 establish substantive proof development, rather than documentation-only assistance. Coauthor trailers do not attribute individual keystrokes.

The duplicate-factorization advisory is addressed by replacing the long secondary localization argument with Mathlib's IsLocalization.atUnits. The new helper proves that the prime-or-unit submonoid contains only units: its closure under squaring makes each s * s prime or a unit, and either alternative makes s a unit. The algebra equivalence then transports irreducibility. This removes 98 lines; all existing theorem binders and conclusions remain unchanged. The significant prime-generated proof and both polynomial applications remain intact. Independent review also approved this consolidation.

The advertised theorem still proves unique factorization for a noetherian integral domain from unique factorization after localizing at an arbitrary prime-generated multiplicative set. Its extra scope over the pool's existing AndersonConjecture/Jensen/KrullDomain/Nagata.lean:nagata_criterion is the arbitrary prime-generated set; the existing result inverts one prime. This overlap is disclosed in the updated PR description.

Current main is integrated losslessly: its 218 project cards are an unchanged byte prefix of the registry, followed by the Nagata card. The existing module migration is preserved. The complete repair diff is reviewed; no checks, linter settings, or waivers changed.

Validation: all 20 project modules compile serially without warnings; the declaration linter passes over the project's complete import closure; generated index and unchanged scoped static source/metadata checks pass. Compiler and linter commands used the shared lock, a 20 GiB aggregate memory limit, and timeouts. The final local full-quality attempt timed out waiting to acquire the shared lock, before executing any checker. Fresh CI must still pass style, full quality, public axiom, compiled environment, full-pool, and documentation checks before merge; no local pass of those pending checks is claimed.

[Vilin97]

🤖 LLM review (gpt-6-astra, 5 rubrics)

Reviewed head: c1db365d95ee8c3bc32a2fe7c7f6b06d2c3fbe4c

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	The Lean faithfully proves the card’s prime-generated Nagata criterion and supports the stated localization applications.
Novelty	✅ pass	Searches of pinned Mathlib and the existing pool found no duplicate of the arbitrary prime-generated factoriality criterion.
Significance	✅ pass	The development centered on NagataFactoriality.nagata_theorem is a substantial graduate-level project, with localization descent proofs and polynomial applications; no generated-bulk maintenance concern was found.
Sources	✅ pass	The pinned upstream source supports the claimed noetherian prime-generated criterion and polynomial applications, and the PR explicitly credits that prior formalization.
Code quality (advisory)	✅ pass	The core proofs are maintainable, with minor cleanup opportunities in duplicate helpers and unused localization hypotheses.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The integral-domain structure, noetherianity, PrimeGenerated S, and unique factorization of Localization S are hypotheses, all disclosed in the card; exclusion of zero from S, existence of factorizations in R, and descent of primality are proved.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	graduate
Branch	commutative algebra
Mode	theory_building
Code quality	3 / 5

Statement check: NagataFactoriality.nagata_theorem establishes Mathlib’s unique-factorization predicate for a noetherian integral domain whenever its localization at a prime-generated submonoid has unique factorization, without restricting the generating set to be finite.

It formalizes Nagata’s factoriality criterion for noetherian domains localized at arbitrary prime-generated multiplicative sets, developing divisibility descent and irreducibility transfer through concrete and abstract localization interfaces.

Code quality findings (2)

• duplicate-definition — LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean:25
  The unused listProd family recreates List.prod and its basic API, adding a separate definition that library product lemmas cannot directly address. Remove this family or use List.prod. Another unused duplicate is ufd_of_factorization_and_prime_irreducibles in Nagata/Theorem.lean:110, whose signature repeats ufd_of_factorization_and_primes from Basic/UFD.lean:44.
  Evidence: def listProd {α : Type*} [CommMonoid α] : List α → α
  | [] => 1
  | a :: as => a * listProd as

theorem listProd_append {α : Type*} [CommMonoid α] (xs ys : List α) :
listProd (xs ++ ys) = listProd xs * listProd ys := by
induction xs with
| nil => simp [listProd]
| cons x xs ih => simp [listProd, ih, mul_assoc]

theorem ufd_of_factorization_and_prime_irreducibles {α : Type*} [CommRing α] [IsDomain α]
(hfac : WfDvdMonoid α)
(hprime : ∀ p : α, Irreducible p → Prime p) :
UniqueFactorizationMonoid α :=
ufd_of_factorization_and_primes hfac hprime

• unused-hypothesis — LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean:449
  The units-equivalence proofs leave unnecessary obligations in the public API: dvd_of_localization_dvd_isLocalization and prime_of_localization_prime_isLocalization ignore both irreducibility and avoidance, while localization_irreducible_of_irreducible_isLocalization ignores avoidance. Their concrete wrappers propagate the same restrictions. In particular, the divisibility helper unnecessarily excludes composite numerators. Drop these hypotheses from the usable interface; upstream signatures can remain compatibility wrappers if needed.
  Evidence: theorem dvd_of_localization_dvd_isLocalization {α β : Type*}
  [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β]
  [root.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p a : α}
  (_hp : Irreducible p) (_havoid : Avoids S p) (hdiv : algebraMap α β p ∣ algebraMap α β a) :
  p ∣ a := by
  let e : α ≃ₐ[α] β :=
  root.IsLocalization.atUnits α S (Submonoid.le_isUnit_of_prime_or_unit hS)
  exact (map_dvd_iff e).mp hdiv

The other declarations likewise bind (_havoid : Avoids S p) at line 435 and (_hp : Irreducible p) (_havoid : Avoids S p) at line 470, then conclude with exact (MulEquiv.irreducible_iff e).mpr hp and exact (MulEquiv.prime_iff e).mp hploc, respectively.

---

Tokens: 2,834,170 in / 19,953 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $58.1799 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

Reviewed current integration head b1d25a41d569fc5f604276c2530f92f8aa2c5b17. The project's Lean source is byte-identical to the previously reviewed fe1cea32f88cb37332ff28256e6fe4d26bef7035; the existing mathematical assessment and fixes carry forward. The merge retains all 218 current-main project cards and this project's complete card, including their original text. The actual pinned mk_all --module --check command passes.

Recommendation: accept once fresh required CI passes. This review covers the lossless main integration; it does not claim another full local rebuild.

[Vilin97]

/review

Please review exact head c1db365d95ee8c3bc32a2fe7c7f6b06d2c3fbe4c after the substantive quality repair and current-main integration. Reused the existing localization equivalence and abstract localization API, eliminating 109 net lines of duplicate transport proofs. All 20 project modules, targeted Mathlib linters, style, unchanged quality/axiom/backdoor checks and generated indexes pass. Main integration changes no project declarations.

[Vilin97]

{
"reviewed_head": "c1db365d95ee8c3bc32a2fe7c7f6b06d2c3fbe4c",
"verdict": "approve",
"assessment": "The incoming two-file repair resolves the three advisory findings from the previous complete five-rubric review. The prime-generated Nagata theorem, project card, and all 20 project modules are retained. The prior faithfulness, novelty, significance, and source assessments carry forward.",
"source_review": [
"Concrete localization lemmas now specialize the existing abstract IsLocalization lemmas with exactly the same domain and nonzero-denominator hypotheses; no duplicate denominator-clearing proof remains at the reported sites.",
"The prime-or-unit compatibility lemmas use the already proved fact that such a multiplicatively closed set contains only units. IsLocalization.atUnits has the canonical algebra map as its forward map, so irreducibility, divisibility, and primality transport through the same localization. These simplifications do not replace or strengthen the separate prime-generated headline hypothesis.",
"The factor-splitting induction never uses irreducibility of its residual factor. Removing that argument generalizes the helper, and its caller still uses irreducibility at the subsequent factorization step."
],
"validation": "Independently read the complete two-file delta, full affected proof contexts, reused abstract localization lemmas, the unit-submonoid proof, and the pinned Mathlib equivalence definition. Project inventory, card bytes and generated project index are unchanged. The author reports a clean 20-module build and scoped gates; this follow-up is a source review and does not claim a new independent compiler run. Fresh required CI and branch protection must pass before merge.",
"findings": []
}

[Vilin97]

Daily disposition: needs maintainer — protected merge operation

Reviewed exact head e6405e8d08f00a92086b8d6bc173446fe8ef1c76. Nagata’s criterion for arbitrary prime-generated multiplicative sets is stronger than the existing single-prime localization theorem. Concrete localization now specializes the shared abstract API; source, overlap and AI provenance are explicit. The complete source/dependency review and recovered repairs were reconciled through the lossless main integration; fresh protected CI remains the integration authority.

Build project: pending/not yet reported, Content / non-content separation: SUCCESS, Documentation preflight: SUCCESS. These are observed check states, not an assertion that unfinished checks passed.

The remaining authority boundary is operational: this repository has allow_auto_merge=false, and GitHub rejected enablePullRequestAutoMerge with “Auto merge is not allowed for this repository.” The maintainer must make protected queuing available through an authorized repository-setting decision, or remove this label and perform a normal squash merge after the required checks and current-base integration pass. This cycle does not change repository settings or bypass protection. No unresolved substantive author-actionable finding justifies another change request or closure; the label is not for draft status, missing profiling, or an old advisory score.