{"id":"74097876-2ebc-4d69-a5d2-a59efa626def","arxiv_id":"2411.16460","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Buchberger and Schreyer algorithms are generalized to strongly discrete coherent rings, with convergence characterized by finite generation of the leading term module.","lead":"This paper generalizes the classic Gröbner basis algorithms of Buchberger and Schreyer to polynomial modules over coefficient rings that are coherent and have decidable arithmetic. It proves that the leading term module is countably generated and that the generalized Buchberger algorithm terminates exactly when that module is finitely generated.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Termination of Buchberger's algorithm for non-noetherian coherent rings is not proved; the cited Adams–Loustaunau proof may rely on noetherianity, so the iff claim is unsupported.","rationale":"The reader's verdict identified the algorithmic hypotheses on the base ring as the main weakness and treated the delegation of Theorem 6.1(1) as a completeness issue. That is not the most load-bearing gap. The deeper problem is Theorem 6.1(2): the termination of the generalized Buchberger algorithm is the point on which the abstract's central claim ('converges if, and only if, MLT(M) is finitely generated') depends, and this is exactly where the manuscript delegates to a theorem whose hypotheses (per Comment 4.12) include noetherianity. The fact that MLT(M) is finitely generated does not, by itself, rule out infinite ascending chains of submodules in a non-noetherian ring; in particular, coefficient ideals at a fixed monomial can increase indefinitely within a fixed finitely generated ideal. The paper does not supply a replacement argument for the non-noetherian case. This is a correctness risk in the central theorem, not merely a style issue. A correct termination proof might exist, and the theorem might be true, but the present text does not provide it. Hence the verdict should be conditional on supplying that proof; if the proof cannot be supplied, the claim should be rejected. The rest of the paper, especially Fundamental theorem 4.11, appears sound and is a real contribution.","tokens_in":19316,"tokens_out":30544,"duration_ms":287438,"concrete_test":"Inspect the proof of Theorem 4.2.3 in Adams and Loustaunau (1994) and locate every use of noetherianity or of the ascending chain condition in the termination argument. If the termination argument depends on ACC, then Theorem 6.1(2) has no proof for non-noetherian strongly discrete coherent rings. To test the claim directly, attempt a computational run of Algorithm 6.2 on a non-noetherian strongly discrete coherent ring with an infinite ascending chain inside a finitely generated ideal, using a finite tuple whose MLT is finitely generated; any infinite run would refute the theorem.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central claim that the generalized Buchberger algorithm converges if and only if MLT(M) is finitely generated rests on Theorem 6.1(2). No proof is given: the text says the proof 'parallels exactly' Adams–Loustaunau's Theorem 4.2.3. But Comment 4.12 indicates Adams–Loustaunau's setting is strongly discrete, coherent, and noetherian. In that setting termination follows from the ascending chain condition on submodules of a finitely generated module. For a non-noetherian strongly discrete coherent ring, a finitely generated module can contain infinite strictly ascending chains of submodules; even at a fixed monomial, the ideals of leading coefficients inside a fixed finitely generated ideal need not stabilize. The paper supplies no argument showing that the particular chain of leading term modules produced by Algorithm 6.2 must stabilize when MLT(M) is finitely generated. Therefore the 'if and only if' convergence claim in the abstract is not established; the proof of the nontrivial 'if' direction is missing.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a constructive theory of Gröbner bases for finitely generated submodules of a free module over a multivariate polynomial ring whose coefficient ring is a discrete coherent ring, or a strongly discrete coherent ring. It proves (Theorem 4.11) that the module of leading terms of such a module is countably generated and provides an explicit algorithm, via iterated S-lists, for producing a generating set. Under the stronger hypothesis that the base ring is strongly discrete coherent, it states a Buchberger criterion and a Buchberger algorithm (Theorem 6.1), claiming convergence if and only if the leading term module is finitely generated. It then gives Schreyer's algorithm for computing a Gröbner basis of the first syzygy module of a Gröbner basis (Theorem 7.4) and a constructive Hilbert syzygy theorem (Theorem 7.5) with resolution length at most n+1. Most technical proofs are provided; the main exception is Theorem 6.1, whose proof is only cited to Adams–Loustaunau.","tokens_in":19482,"tokens_out":15839,"duration_ms":146871,"significance":"If correct, these results extend Gröbner basis theory and Schreyer's syzygy method beyond the classical noetherian setting to a broad class of rings with strong algorithmic structure. The countable generation theorem and the iterated S-list algorithm are fully proved and are of independent interest, especially for non-noetherian valuation domains and other coherent rings. The constructive Hilbert syzygy theorem gives explicit finite free resolutions of length at most n+1 over such rings, which is a substantial generalization. The paper is also transparent in disclosing an error in prior work and correcting it. However, the central Buchberger algorithm theorem is not proved in the manuscript, so the main convergence claim is not established.","major_comments":[{"comment":"The claim that Algorithm 6.2 converges whenever MLT(M) is finitely generated is one of the central results of the paper, but the proof is not given: the text says it 'parallels exactly' Adams–Loustaunau's Theorem 4.2.3. This is not sufficient, because the termination argument in Adams–Loustaunau's setting may use noetherianity: Comment 4.12 explicitly notes that their Theorem 4.2.8 assumes the base ring is noetherian, and noetherianity provides the ascending chain condition on submodules of a finitely generated module. For a non-noetherian strongly discrete coherent ring, a finitely generated module can contain infinite strictly ascending chains of submodules, so the chain of leading-term modules produced by Algorithm 6.2 need not stabilize merely because MLT(M) is finitely generated. The manuscript supplies no argument (e.g., a well-founded measure on the leading terms of the added remainders) showing that this particular chain must terminate. Therefore the 'if' direction of the claimed equivalence is not established.","section":"Theorem 6.1(2), Algorithm 6.2, Comment 4.12"},{"comment":"The Buchberger criterion is also stated without proof. The 'only if' direction follows from the definition of a Gröbner basis and the division algorithm, but the 'if' direction requires a substantial argument: one must show that the reduction of every S-polynomial to zero implies that every leading term of an element of M lies in <LT(G)>, using the fact that the S-list generates all syzygies of the leading terms (Proposition 4.4). This is non-obvious when the coefficient ring has nontrivial syzygies, especially for position-level sets E of size greater than 2. The citation to Adams–Loustaunau is not enough, as their proof may rely on hypotheses that are not present here; a self-contained proof or a precise indication of which steps are unchanged is needed.","section":"Theorem 6.1(1)"}],"minor_comments":[{"comment":"The for loop that removes elements from S and adds new elements to S within the same loop makes the control flow ambiguous; presenting it as a worklist algorithm with an explicit pending set would improve clarity.","section":"Algorithm 6.2"},{"comment":"The expression sE_1 = 1/3(-15,6) is not an equality in Z; the generator of Syz(6,15) should be given directly as (-5,2) (or (5,-2)) to avoid confusion about division in the base ring.","section":"Example 4.7"},{"comment":"There are typographical errors: 'multi variate' should be 'multivariate', and 'Bes ançon' should be 'Besançon'.","section":"Abstract and affiliations"},{"comment":"The notation <LT(S0(f1,f2)> is missing a closing parenthesis; it should be <LT(S0(f1,f2))>.","section":"Example 4.14(2)"}],"recommendation":"major_revision","confidential_remarks":"The paper is a valuable contribution to constructive commutative algebra, and the provided proofs of Theorems 4.11, 7.4, and 7.5 are detailed and convincing. The main concern is the unproved Fundamental Theorem 6.1, which is load-bearing for the abstract's central claim. If the authors can provide a complete proof (or a full adaptation of Adams–Loustaunau's proof that does not rely on noetherianity), I would recommend acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the short version. The paper has a genuinely new result—Theorem 4.11, the countable generation of the leading term module for any discrete coherent ring—and the Schreyer/Hilbert syzygy material in Section 7 is worked out in detail. But the main Buchberger claim (Theorem 6.1(2)) is not proved. The text says the proof 'parallels exactly' Adams–Loustaunau, yet their theorem is for strongly discrete coherent rings that are also noetherian. The paper supplies no argument that the coefficient ideals stabilize in the non-noetherian case even when MLT is finitely generated. So the iff in the abstract is unsupported as written.\n\nWhat's good: the constructive syzygy machinery in Sections 4 and 5 is careful and genuinely useful. Proposition 4.4 and the iterated S-list construction are fully proved. The Schreyer order basis in Theorem 7.4 is proved in detail, and the Hilbert syzygy theorem in 7.5 follows from it cleanly—except that its first step assumes a Gröbner basis, which is supposed to come from Theorem 6.1(2). So the gap propagates.\n\nOn the soft spot: this is not a minor omission. It is the central termination theorem, and the paper's own Comment 4.12 explicitly notes that Adams–Loustaunau assume noetherianity, which makes the 'parallels exactly' handwave particularly suspicious. The proof is probably repairable—Dickson's lemma bounds the new leading monomials, and finite generation of MLT gives finite generation of each coefficient ideal, so the ascending chains should stabilize—but the authors need to actually write that out. As it stands, the paper claims more than it proves.\n\nThe reader's report underplays this; it calls the gap a 'completeness issue rather than a correctness flaw.' I think it is a correctness flaw in the current version because the main theorem statement is not established.\n\nWho this is for: constructive and computational commutative algebraists interested in Gröbner bases over general rings. The countable generation result and the syzygy algorithms are worth a serious look. I would send this to a knowledgeable referee, but the verdict should be major revision, not acceptance. The authors should either prove Theorem 6.1(2) in the non-noetherian setting or soften the claim to match what is actually shown.","headline":"The countable generation theorem and the Schreyer/Hilbert syzygy results are real, but the paper's headline Buchberger termination claim is delegated to a noetherian proof and is not actually proved in the stated generality.","tokens_in":20037,"tokens_out":9721,"would_cite":false,"duration_ms":89836,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["13D02","13P10","13C10","13P20","14Q20"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proves that over a strongly discrete coherent base ring, the generalized Buchberger algorithm computes a Gröbner basis for a module exactly when the module of leading terms is finitely generated, and gives a constructive…","keywords":["generalised Buchberger algorithm","syzygy theory","free resolution","monomial order","Schreyer's syzygy algorithm","constructive mathematics","coherent rings","Gröbner bases"],"falsifier":"Take a nonarchimedean valuation domain $V$ with elements $a,b$ such that $a^q$ divides $b$ for every $q$, and run Algorithm 6.2 on $f_1=aX+1$, $f_2=b$ in $V[X]$. The theorem predicts the S-lists generate $\\langle aX, b, b/a, \\dots, b/a^q\\rangle$ at stage $q$ and that the algorithm never terminates because $MLT$ is not finitely generated; if the run did terminate, or if the union of the stage submodules failed to equal the true $MLT$, the main equivalence would be false.","tokens_in":19084,"feed_emoji":"🧮","tokens_out":9952,"duration_ms":83459,"temperature":0.7,"pith_summary":"The paper works in constructive algebra and asks when Gröbner basis computations are possible for modules over polynomial rings whose coefficient ring is not a field. Its first main result is that, for a finitely generated submodule of a free module over $R[X_1,\\ldots,X_n]$ with $R$ a discrete coherent ring, the module $MLT(M)$ of leading terms is countably generated, with an explicit algorithm enumerating generators via iterated S-lists. When $R$ is strongly discrete coherent, the paper proves Buchberger's criterion and algorithm remain valid: the generalized Buchberger algorithm terminates and yields a Gröbner basis if and only if $MLT(M)$ is finitely generated. It then proves Schreyer's algorithm computes a Gröbner basis for the first syzygy module under the induced order, giving a constructive Hilbert syzygy theorem with finite free resolutions of length at most $n+1$. The upshot is that the classical Buchberger and Schreyer methods extend to a broad class of non-noetherian coefficient rings.","feed_headline":"Gröbner bases now reach non-noetherian rings","feed_subtitle":"Generalized Buchberger algorithm stops exactly when leading terms are finitely generated.","key_machinery":"The central object is the iterated S-list $S^q(f_1,\\ldots,f_p)$: starting with $S^0=(f_1,\\ldots,f_p)$, each step appends the S-list $S(G)$ of the current list, whose elements are combinations $\\sum_j S_{i,j}f_j$ formed from syzygies of the leading coefficients at each position level set $E$, lifted by multiplying each component by $\\operatorname{lcm}(M_j)/M_j$. Since $R$ is coherent, each syzygy module of coefficients is finitely generated, so each S-list is finite; iterating provides the countable enumeration of leading terms. The rewriting algorithm based on these S-lists lowers the leading monomial of any linear combination with the same total leading monomial, which is what makes the Buchberger criterion and Schreyer's construction go through.","core_discovery":"Over a strongly discrete coherent base ring—a ring with decidable equality, membership tests with witnesses, and computable syzygy modules—the classical Buchberger and Schreyer constructions are not tied to noetherianness. For any $f_1,\\ldots,f_p$, the iterated S-lists $S^q(f_1,\\ldots,f_p)$ generate an increasing chain of leading-term submodules whose union is exactly $MLT(\\langle f_1,\\ldots,f_p\\rangle)$, so the leading-term module is countably generated with an explicit enumeration. From this, the generalized Buchberger algorithm terminates exactly when $MLT$ is finitely generated, and the generalized Schreyer algorithm yields a Gröbner basis for the first syzygy module with respect to Schreyer's monomial order. Consequently every finitely generated submodule with finitely generated leading-term module has a finite free resolution of length at most $n+1$, constructively, with the leading terms of iterated syzygies successively independent of the indeterminates.","pith_inferences":["A reader may infer that when $MLT(M)$ is not finitely generated, the explicit enumeration still gives a semi-decision procedure: membership of a term in $MLT(M)$ can be confirmed by searching successively through $S^0, S^1, S^2, \\dots$, although it cannot be refuted in finite time.","The same machinery suggests a uniform treatment of ideal membership and syzygy computation for 'division with remainder' coefficient rings beyond the strongly discrete case, as sketched in Remark 2.4.","If the constructive Hilbert syzygy bound $q\\le n+1$ is independent of the base ring's complexity, then any coherent ring satisfying the algorithmic oracles yields resolutions of the same length as over a field, which is strong evidence that noetherianness is not the essential hypothesis for the theorem."],"forward_implications":["If $MLT(M)$ is finitely generated, the generalized Buchberger algorithm produces a Gröbner basis for $M$, so Gröbner bases become constructively available for all such modules over strongly discrete coherent rings.","If $MLT(M)$ is not finitely generated, the algorithm cannot terminate; the equivalence gives a computable witness for nontermination, since the increasing chain of leading-term submodules never stabilizes.","Schreyer's algorithm computes a Gröbner basis for the first syzygy module of any Gröbner basis, so syzygy modules inherit explicit Gröbner bases under the induced monomial order.","Every finitely generated submodule $U$ with $MLT(U)$ finitely generated admits a finite free resolution of length at most $n+1$, with the syzygy generators' leading terms independent of $X_n$, then $X_{n-1}$, and so on.","For Bézout and Prüfer coefficient rings, the S-list reduces to ordinary S-pairs and annihilator syzygies, recovering and unifying earlier syzygy theorems for such rings."],"supporting_citations":[{"why":"Provides the classical Gröbner basis theory over strongly discrete noetherian rings that this paper generalises, including the Buchberger criterion and leading-term module results.","marker":"Adams and Loustaunau 1994"},{"why":"Introduces the syzygy theorem for Bézout rings and the S-list method that the present iterated S-list construction extends.","marker":"Gamanda, Lombardi, Neuwirth, and Yengui 2020"},{"why":"Supplies the constructive framework and the division algorithm on which the generalized division algorithm 5.2 is modelled.","marker":"Yengui 2015"},{"why":"Contains the Schreyer proof that is adapted here to strongly discrete coherent rings.","marker":"Ene and Herzog 2012"},{"why":"Original Buchberger algorithm and S-polynomial criterion that the paper generalises.","marker":"Buchberger 1965"},{"why":"Original Schreyer syzygy algorithm producing Gröbner bases of syzygy modules, here generalised.","marker":"Schreyer 1980"},{"why":"Supplies constructive algebra background, especially Bézout and valuation ring facts used in examples and Proposition 3.3.","marker":"Lombardi and Quitté 2015"}],"fun_headline_variants":["Gröbner bases generalize beyond Noetherian rings","Buchberger algorithm now works on coherent rings","Termination tied to finitely generated leading terms","Schreyer syzygies for non-Noetherian rings","Noetherian not required for Gröbner bases"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The entire construction assumes the coefficient ring comes with algorithms that decide equality, test membership in finitely generated ideals with explicit witnesses, and compute finite generating sets for every syzygy module of a finite tuple; without these oracles the S-lists, division steps, and termination argument cannot be run.","fun_headline_variants_meta":{"raw":{"variants":["Gröbner bases generalize beyond Noetherian rings","Buchberger algorithm now works on coherent rings","Termination tied to finitely generated leading terms","Schreyer syzygies for non-Noetherian rings","Noetherian not required for Gröbner bases"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000196,"raw_usage":{"total_tokens":1311,"prompt_tokens":848,"completion_tokens":463,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":464,"completion_tokens_details":{"reasoning_tokens":385}},"tokens_in":464,"tokens_out":463,"duration_ms":4515,"temperature":1.0,"reasoning_tokens":385,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T13:07:13.402758+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a nonarchimedean valuation domain $V$ with elements $a,b$ such that $a^q$ divides $b$ for every $q$, and run Algorithm 6.2 on $f_1=aX+1$, $f_2=b$ in $V[X]$. The theorem predicts the S-lists generate $\\langle aX, b, b/a, \\dots, b/a^q\\rangle$ at stage $q$ and that the algorithm never terminates because $MLT$ is not finitely generated; if the run did terminate, or if the union of the stage submodules failed to equal the true $MLT$, the main equivalence would be false.","supporting_citations":[{"cited_title":"u rgen Herzog. Gr \\","cited_arxiv_id":null,"evidence_quote":"Contains the Schreyer proof that is adapted here to strongly discrete coherent rings."},{"cited_title":"The syzygy theorem for B\\'ezout rings","cited_arxiv_id":null,"evidence_quote":"Introduces the syzygy theorem for Bézout rings and the S-list method that the present iterated S-list construction extends."},{"cited_title":"Constructive commutative algebra: projective modules over polynomial rings and dynamical Gr \\\"o bner bases","cited_arxiv_id":null,"evidence_quote":"Supplies the constructive framework and the division algorithm on which the generalized division algorithm 5.2 is modelled."},{"cited_title":"a t . Master's thesis, german Universit \\","cited_arxiv_id":null,"evidence_quote":"Original Schreyer syzygy algorithm producing Gröbner bases of syzygy modules, here generalised."},{"cited_title":"Commutative algebra: constructive methods","cited_arxiv_id":null,"evidence_quote":"Supplies constructive algebra background, especially Bézout and valuation ring facts used in examples and Proposition 3.3."}],"review_version":1}