feat: the divisors, Riemann-Roch spaces and genus of the rational function field

[roed-math]

This PR carries out the rational-function-field calculations of Layer 3 of the
AlgebraicCurves roadmap — the "The rational function field, at divisor level" bullet of
"Layer 3: divisors, L(D), Riemann's theorem, and the genus", which asks for div x = P_(X) − P_∞,
the pole-divisor degree max (natDegree f.num) (natDegree f.denom) = [k(x) : k(f)], the model
computation L(n·P_∞) = polynomials of degree ≤ n with ℓ(n·P_∞) = n + 1 "proved by hand, long
before Riemann–Roch", and hence g(k(x)) = 0 (Stichtenoth, Example 1.4.18). That bullet is the
milestone; it is Layer 3's named base case and first acceptance suite, and the genus-zero value it
produces is what Layer 5's genus-0 characterisation (Prop. 1.6.3) and Layer 7's normalisation
2g − 2 = −2[F : k(x)] + deg Diff(F/k(x)) (Cor. 3.4.14) both consume. Its prerequisites are all on
main: the classification of the places of k(x) (Layer 1), the divisor group and principal
divisors, L(D), ℓ(D), and Riemann's theorem with the genus (Layer 3). What remains in Layer 3
after this PR is the concrete sum form ∑_p natDegree p · ord_p(f) = intDegree f of the product
formula on ℙ¹; the rest of the layer's rational-function-field bullet is closed here.

New file TauCeti/FieldTheory/FunctionField/RiemannRoch/RatFunc.lean proves, in order:
TauCeti.Place.forall_ord_adicOfIrreducible_nonneg_iff, that a rational function is a polynomial
exactly when it has no pole at any finite place; TauCeti.Divisor.principal_X, that
div x = P_(X) − P_∞; TauCeti.mem_riemannRochSpace_nsmul_ofPoint_infty_iff and
TauCeti.riemannRochSpace_nsmul_ofPoint_infty, that L(n·P_∞) is the space of polynomials of
degree at most n; TauCeti.Divisor.dim_nsmul_ofPoint_infty, that ℓ(n·P_∞) = n + 1;
TauCeti.genus_ratFunc, that genus k (RatFunc k) = 0; and
TauCeti.Divisor.degree_poles_eq_max_natDegree, the pole-divisor degree of a nonconstant function.
The genus computation feeds ℓ(n·P_∞) = n + 1 and deg (n·P_∞) = n into the existing
TauCeti.exists_forall_dim_eq_degree_add_one_sub_genus, so Riemann's inequality is exhibited as
sharp at every n, exactly as Stichtenoth's Example 1.4.18 argues.

Three supporting lemmas go into their canonical home,
TauCeti/FieldTheory/FunctionField/Place/RatFunc/Basic.lean, rather than into the new file:
TauCeti.Place.ord_infty_algebraMap (ord_∞ p = −deg p, next to ord_infty),
TauCeti.Place.adicOfIrreducible_ne_infty and
TauCeti.Place.eq_infty_or_exists_eq_adicOfIrreducible (next to adic_ne_infty and
eq_infty_or_exists_eq_adic), and
TauCeti.Place.adicOfIrreducible_eq_adicOfIrreducible_iff (a finite place remembers exactly the
associate class of its polynomial, next to adicOfIrreducible). No declaration is renamed or
removed, and nothing is vendored.

Nothing is copied from an existing formalization; the mathematics follows Stichtenoth, Algebraic
Function Fields and Codes, 2nd ed., GTM 254, Example 1.4.18 and Proposition 1.2.1, cited in the
module docstring. The proofs consume rather than rebuild three central Mathlib results:
IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one (a Dedekind domain is the
intersection of its localizations at the height-one primes) for "no finite pole ⟹ polynomial",
RatFunc.finrank_eq_max_natDegree for the degree of a rational map, and Polynomial.degreeLT.basis
together with Polynomial.degreeLT_succ_eq_degreeLE for dim_k {p | deg p ≤ n} = n + 1.

Roadmap: AlgebraicCurves

🤖 Prepared with Claude Code

[sqrt-of-2]

✅ placement — now passing on e25e651.

[sqrt-of-2]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	agy/gemini-3.7-flash-high	The PR correctly and faithfully formalizes the principal divisors, Riemann–Roch spaces, genus computation, and pole-divisor degrees for the rational function field over an arbitrary field. All statements match the mathematical reference (Stichtenoth, Sections I.2 and I.4) without artificial hypotheses, placeholders, or vacuous claims.
✅	reuse	approved	agy/gemini-3.7-flash-high	The pull request adds genuinely new divisor and Riemann–Roch results for the rational function field without duplicating existing material. It reuses existing valuation theory, polynomial basis constructions, and function field results from Mathlib and TauCeti.
✅	scope	approved	agy/gemini-3.7-flash-high	This pull request directly implements the Layer 3 rational-function-field divisor and genus computations from the AlgebraicCurves roadmap as a single coherent topic. All prerequisites from Layer 1 and the general divisor theory of Layer 3 are present on main.
✅	attribution	approved	agy/gemini-3.7-flash-high	The PR thoroughly credits its mathematical and formal sources (Stichtenoth, Sections I.2 and I.4) in module docstrings and individual declaration docstrings. No uncredited, laundered, or vendored material is present.
✅	api-design	approved	agy/gemini-3.7-flash-high	The public API cleanly exposes the roadmap milestones and necessary supporting lemmas for the rational function field without obsolete compatibility layers. Simplification attributes are correctly placed and avoid linter conflicts.
✅	generality	approved	agy/gemini-3.7-flash-high	All declarations are stated at their natural level of generality over an arbitrary base field with minimal necessary hypotheses. General lemmas are proven first and specialized cleanly without proof duplication.
✅	placement	approved	agy/gemini-3.7-flash-high	All new declarations and files are placed in their canonical homes matching their subject matter and dependencies, and all imports are appropriately scoped.
✅	naming	approved	agy/gemini-3.7-flash-high	All newly introduced declarations follow standard Mathlib naming conventions, accurately describe their conclusions with appropriate statement strength and namespaces, and introduce no notation.
✅	documentation	approved	agy/gemini-3.7-flash-high	All new files and modified modules contain accurate, informative module docstrings and literature references. Every newly introduced declaration is documented with a clear mathematical description of the result.
✅	proof-quality	approved	agy/gemini-3.7-flash-high	The proofs are concise, robust, and readable, leveraging standard automation (omega, simp) and cleanly factored intermediate lemmas without undocumented definitional equality manipulations.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head e25e651. rubrics @ 94d131c. Review spend: $3.04.}

[roed-math]

🟡 reuse — request_changes claude/claude-opus-5

The new material is genuinely new — no existing genus, L(n·P_∞), or 'no finite pole ⟹ polynomial' declaration exists in TauCeti or Mathlib. Two proofs re-derive located in-repo API: the monic-generator argument that monicIrreducibleEquiv/ratFuncEquivMonicIrreducible already package, and the associate-class argument the PR's own new iff now packages.

• TauCeti/FieldTheory/FunctionField/Place/RatFunc/Basic.lean:329 — eq_infty_or_exists_eq_adicOfIrreducible re-derives "every height-one prime of k[X] is ofIrreducible hq" from existsUnique_monic_irreducible_span + HeightOneSpectrum.ext; the same three lines are repeated in RiemannRoch/RatFunc.lean:79-81 (obtain ⟨q, ⟨-, hqi, hspan⟩, -⟩ := v.existsUnique_monic_irreducible_span; show v = ofIrreducible hqi from HeightOneSpectrum.ext (hspan.trans (ofIrreducible_asIdeal hqi).symm)). Both are already provided by existing API. Fix: In RiemannRoch/RatFunc.lean:79-81 use IsDedekindDomain.HeightOneSpectrum.monicIrreducibleEquiv: with q := monicIrreducibleEquiv.symm v, monicIrreducibleEquiv_apply (rfl/simp) and Equiv.apply_symm_apply give ofIrreducible q.2.2 = v directly. Prove eq_infty_or_exists_eq_adicOfIrreducible from the existing classification equiv: obtain ⟨(_ | q), rfl⟩ := (ratFuncEquivMonicIrreducible k).surjective P then Or.inl rfl / Or.inr ⟨q, q.2.2, ratFuncEquivMonicIrreducible_some k q⟩.
• TauCeti/FieldTheory/FunctionField/Place/RatFunc/Basic.lean:405 — After this PR, adicOfIrreducible_X_sub_C_injective inlines exactly the argument the new adicOfIrreducible_eq_adicOfIrreducible_iff (line 266) packages: adic_injective, ofIrreducible_asIdeal twice, Ideal.span_singleton_eq_span_singleton. The same reasoning now lives twice in one file. Fix: Reprove it through the new lemma: fun a b h => by simpa using congrArg (fun p : k[X] => p.coeff 0) (eq_of_monic_of_associated (monic_X_sub_C a) (monic_X_sub_C b) ((adicOfIrreducible_eq_adicOfIrreducible_iff _ _).mp h)).

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 263s · 2.3k in / 19.6k out tokens · reviewing this diff · rubric}

[roed-math]

Both duplications are gone, but by the route the proof-quality thread asked for rather than through monicIrreducibleEquiv/ratFuncEquivMonicIrreducible, because that route is not available at either site:

• Place.eq_infty_or_exists_eq_adicOfIrreducible sits above ratFuncEquivMonicIrreducible in Place/RatFunc/Basic.lean — that equiv is built from ratFuncEquiv, which is built from eq_infty_or_exists_eq_adic, so using it here would need the declaration moved past the whole classification block.
• monicIrreducibleEquiv's own surjectivity field (TauCeti/RingTheory/Polynomial/HeightOneSpectrum.lean:80-82) was the third copy of the same three lines, so it cannot be the shared home.

So the fact is now a single named lemma, IsDedekindDomain.HeightOneSpectrum.exists_monic_irreducible_eq_ofIrreducible (TauCeti/RingTheory/Polynomial/HeightOneSpectrum.lean), and all three sites consume it: monicIrreducibleEquiv, Place.eq_infty_or_exists_eq_adicOfIrreducible, and Place.forall_ord_adicOfIrreducible_nonneg_iff (which also moved to Place/RatFunc/Order.lean per the placement thread, and there closes its goal with the file's own valuation_ofIrreducible_le_one_iff and ord_adicOfIrreducible_neg_iff).

The second finding is fixed as suggested: adicOfIrreducible_X_sub_C_injective now goes through adicOfIrreducible_eq_adicOfIrreducible_iff.

lake build and lake exe axioms are green at dda1832.

[sqrt-of-2]

Re: your reply on reuse — re-reviewed on dda1832; this clears the finding ✅ — approved on dda1832.

_{agy/gemini-3.7-flash-high · addresses your replies through comment 3878430247.}

[CBirkbeck]

Re: your reply on reuse — re-reviewed on dda1832; this clears the finding ✅ — approved on dda1832.

_{codex/gpt-5.6-sol · addresses your replies through comment 3878430247.}

[roed-math]

🟡 api-design — request_changes claude/claude-opus-5

The surface is minimal and free of compatibility artifacts, but Divisor.degree_poles_eq_max_natDegree carries a transcendence hypothesis that the identity does not need, weakening the hypothesis-free Mathlib result it wraps, and two new public lemmas restate compositions of existing @[simp] lemmas.

• TauCeti/FieldTheory/FunctionField/RiemannRoch/RatFunc.lean:201 — Divisor.degree_poles_eq_max_natDegree requires hz : Transcendental k z, but the identity holds for every unit of RatFunc k: if z is algebraic then (by algebraicClosure_ratFunc) z = C c with c ≠ 0, so principal = 0 hence degree (poles ..) = 0, while max (C c).natDegree (1 : k[X]).natDegree = 0. The wrapper is thus strictly weaker than the Mathlib result it consumes, and the docstring itself has to tell the user to bridge via RatFunc.transcendental_of_ne_C. Fix: Drop hz and prove the unconditional statement: by_cases IsAlgebraic k (z : RatFunc k); in the algebraic branch use Divisor.principal_eq_zero_of_isAlgebraic (+ algebraicClosure_ratFunc, RatFunc.num_C, RatFunc.denom_C) and in the other branch the current rw.
• TauCeti/FieldTheory/FunctionField/Place/RatFunc/Basic.lean:132 — Place.ord_infty_algebraMap is exactly the composition of two existing @[simp] lemmas (ord_infty, RatFunc.intDegree_polynomial), so it adds a public name for something already in simp normal form. Same problem at RiemannRoch/RatFunc.lean:176: Divisor.degree_nsmul_ofPoint_infty is @[simp] yet is built only from the simp lemmas map_nsmul, Divisor.degree_ofPoint, Place.degree_infty, so it duplicates simp-set coverage. Fix: Delete ord_infty_algebraMap and close its two uses with simp; for degree_nsmul_ofPoint_infty either drop the declaration (its two uses in genus_ratFunc are simp-closable) or at least remove the redundant @[simp].

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 318s · 2.3k in / 23.6k out tokens · reviewing this diff · rubric}

[roed-math]

🟡 generality — request_changes claude/claude-opus-5

Two level problems: Divisor.principal_X is proved only for X although the identical proof gives div p = P_(p) − (deg p)·P_∞ for every irreducible p with lemmas already present, and Divisor.degree_poles_eq_max_natDegree carries a Transcendental hypothesis that Mathlib's counterpart deliberately does without.

• TauCeti/FieldTheory/FunctionField/RiemannRoch/RatFunc.lean:95 — Divisor.principal_X is the p = X case of div p = P_(p) − (deg p) • P_∞ for an arbitrary irreducible p; the proof given is already the general one with X hardcoded. Fix: State Divisor.principal_irreducible {p : k[X]} (hp : Irreducible p) : principal (IsFunctionField.ratFunc k) (Units.mk0 (algebraMap k[X] (RatFunc k) p) _) = WeilDivisor.ofPoint (Place.adicOfIrreducible hp) - p.natDegree • WeilDivisor.ofPoint (Place.infty k) and derive principal_X from it via RatFunc.algebraMap_X, natDegree_X, one_nsmul.
• TauCeti/FieldTheory/FunctionField/RiemannRoch/RatFunc.lean:201 — Divisor.degree_poles_eq_max_natDegree assumes Transcendental k z, but the statement holds for every unit z : (RatFunc k)ˣ: for z algebraic over k both sides are 0. Fix: Drop hz and case-split: if IsAlgebraic k z, Divisor.principal_eq_zero_of_isAlgebraic gives poles = 0 hence degree 0, and algebraicClosure_ratFunc puts z = C c, so max z.num.natDegree z.denom.natDegree = 0.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 240s · 2.3k in / 17.3k out tokens · reviewing this diff · rubric}

[roed-math]

🟡 placement — request_changes claude/claude-opus-5

Directory choice, the four relocated Place lemmas, and both Mathlib imports are correct. One declaration is in the wrong home: a Place-level lemma about orders at the finite places of k(x) lives in the RiemannRoch file instead of Place/RatFunc/Order.lean.

• TauCeti/FieldTheory/FunctionField/RiemannRoch/RatFunc.lean:72 — TauCeti.Place.forall_ord_adicOfIrreducible_nonneg_iff is a pure statement about ord at the finite places of k(x) — no divisor, L(D) or genus content — but sits in a file importing RiemannRoch/Genus. Its canonical home is the earlier Place/RatFunc/Order.lean, whose docstring is "Orders at the finite places of the rational function field" and which already collects the ord_adicOfIrreducible_* family. As it stands, any future Place-level file needing "regular at every finite place ⟹ polynomial" must import the whole Riemann–Roch stack. Fix: Move the theorem (and its Place namespace block) into TauCeti/FieldTheory/FunctionField/Place/RatFunc/Order.lean, listing it in that file's ## Main results, and drop it from the new file's ## Main results.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 159s · 2.3k in / 11.6k out tokens · reviewing this diff · rubric}

[roed-math]

🟡 proof-quality — request_changes claude/claude-opus-5

Proofs are short and mostly robust, but the PR inlines the same three-line "every height-one prime of k[X] is ofIrreducible hq" derivation twice instead of factoring it, and Divisor.principal_X re-does an ite case split that two existing dedicated simp lemmas already close.

• TauCeti/FieldTheory/FunctionField/RiemannRoch/RatFunc.lean:79 — The step obtain ⟨q, ⟨-, hqi, hspan⟩, -⟩ := v.existsUnique_monic_irreducible_span followed by HeightOneSpectrum.ext (hspan.trans (ofIrreducible_asIdeal hqi).symm) to conclude v = ofIrreducible hqi is inlined here and again verbatim at TauCeti/FieldTheory/FunctionField/Place/RatFunc/Basic.lean:329-331 (and already exists inside monicIrreducibleEquiv, TauCeti/RingTheory/Polynomial/HeightOneSpectrum.lean:81-82). It is a reusable fact, not a one-off, and here it is buried in a rw [show v = ... from ...]. Fix: Add IsDedekindDomain.HeightOneSpectrum.exists_irreducible_eq_ofIrreducible (p : HeightOneSpectrum k[X]) : ∃ (q : k[X]) (hq : Irreducible q), p = ofIrreducible hq to TauCeti/RingTheory/Polynomial/HeightOneSpectrum.lean and use it at both new sites (and in monicIrreducibleEquiv's surjectivity).
• TauCeti/FieldTheory/FunctionField/RiemannRoch/RatFunc.lean:107 — Divisor.principal_X rewrites with the raw Place.ord_adicOfIrreducible_X and then hand-discharges the ite with ite_eq_left hqX / ite_eq_right hqX (forcing the leading classical), although Place.ord_adicOfIrreducible_X_self and Place.ord_adicOfIrreducible_X_of_not_associated are @[simp] lemmas stating exactly the two branches the proof takes. Fix: In the ¬Associated q X branch use Place.ord_adicOfIrreducible_X_of_not_associated hq hqX; in the other branch rewrite the place with hplace first and close with simp via Place.ord_adicOfIrreducible_X_self. Then classical and the ite_eq_* bookkeeping can go.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 251s · 2.3k in / 19.2k out tokens · reviewing this diff · rubric}

[roed-math]

Both findings are addressed, the second with one deliberate deviation.

1. The three-line derivation is now IsDedekindDomain.HeightOneSpectrum.exists_monic_irreducible_eq_ofIrreducible in TauCeti/RingTheory/Polynomial/HeightOneSpectrum.lean, exactly as suggested, and it is consumed at all three sites: monicIrreducibleEquiv's surjectivity, Place.eq_infty_or_exists_eq_adicOfIrreducible, and Place.forall_ord_adicOfIrreducible_nonneg_iff. It carries the monicity as well, since monicIrreducibleEquiv needs it; the two consumers that do not discard it with -. No rw [show v = … from …] remains.

2. The classical and the ite_eq_left/ite_eq_right bookkeeping are gone, but not by rewriting with ord_adicOfIrreducible_X_self/ord_adicOfIrreducible_X_of_not_associated: the generality thread (finding at RiemannRoch/RatFunc.lean:95) required principal_X to be replaced by Divisor.principal_irreducible for an arbitrary irreducible p, so the X-specific simp lemmas no longer apply. The general lemma rewrites once with Place.ord_adicOfIrreducible_algebraMap_irreducible and discharges each branch with simp [hqp] (hqp : Associated q p or its negation), which needs no classical and no ite_eq_*. Divisor.principal_X is now a two-line corollary via RatFunc.algebraMap_X, natDegree_X, one_nsmul and contains no case split at all.

lake build and lake exe axioms are green at dda1832.

[sqrt-of-2]

Re: your reply on proof-quality — re-reviewed on dda1832; this clears the finding ✅ — approved on dda1832.

_{agy/gemini-3.7-flash-high · addresses your replies through comment 3878431211.}

[CBirkbeck]

Re: your reply on proof-quality — re-reviewed on dda1832; this clears the finding ✅ — approved on dda1832.

_{codex/gpt-5.6-sol · addresses your replies through comment 3878431211.}

[roed-math]

AI review — changes requested

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5	All seven new statements match the intended mathematics: div X = P_(X) − P_∞, L(nP_∞) = polynomials of degree ≤ n, ℓ = n+1, genus 0, and deg(z)_∞ = max(deg num, deg denom). Junk values (ord 0, natDegree 0, degree ⊥) are handled consistently, hypotheses are neither too weak nor too strong, and the genus value is pinned by an honest equality rather than the truncated-sSup junk value.
🟡	reuse	changes requested	claude/claude-opus-5	The new material is genuinely new — no existing genus, L(n·P_∞), or 'no finite pole ⟹ polynomial' declaration exists in TauCeti or Mathlib. Two proofs re-derive located in-repo API: the monic-generator argument that monicIrreducibleEquiv/ratFuncEquivMonicIrreducible already package, and the associate-class argument the PR's own new iff now packages.
✅	scope	approved	claude/claude-opus-5	The PR is exactly the AlgebraicCurves Layer 3 bullet 'The rational function field, at divisor level' (roadmap README lines 502-510), and all its stated prerequisites (Layer 1 places of k(x), Layer 3 divisors, L(D), genus, Riemann's theorem) are on main. Single coherent topic; the supporting lemmas added to Place/RatFunc/Basic.lean are all consumed by the new file.
✅	attribution	approved	claude/claude-opus-5	Sources are credited where they matter: Stichtenoth Ex. 1.4.18, Thm. 1.2.2, Prop. 1.2.1(a) and Thm. 1.4.11 in the module and per-declaration docstrings, and the three central Mathlib declarations the arguments run on are named in the docstrings that use them. No vendored or closely-followed prior formalization; the roadmap's Coordination section records independence from the one overlapping repo.
🟡	api-design	changes requested	claude/claude-opus-5	The surface is minimal and free of compatibility artifacts, but Divisor.degree_poles_eq_max_natDegree carries a transcendence hypothesis that the identity does not need, weakening the hypothesis-free Mathlib result it wraps, and two new public lemmas restate compositions of existing @[simp] lemmas.
🟡	generality	changes requested	claude/claude-opus-5	Two level problems: Divisor.principal_X is proved only for X although the identical proof gives div p = P_(p) − (deg p)·P_∞ for every irreducible p with lemmas already present, and Divisor.degree_poles_eq_max_natDegree carries a Transcendental hypothesis that Mathlib's counterpart deliberately does without.
🟡	placement	changes requested	claude/claude-opus-5	Directory choice, the four relocated Place lemmas, and both Mathlib imports are correct. One declaration is in the wrong home: a Place-level lemma about orders at the finite places of k(x) lives in the RiemannRoch file instead of Place/RatFunc/Order.lean.
✅	naming	approved	claude/claude-opus-5	Names describe their conclusions in the vocabulary already used by the adjacent RatFunc place/divisor files, _iff/_eq suffixes match the statement strength, and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5	Every new declaration and the new file are documented, and the docstrings match the statements: the cited Mathlib names (RatFunc.transcendental_of_ne_C, RatFunc.finrank_eq_max_natDegree) and in-repo results (Divisor.degree_poles, exists_forall_dim_eq_degree_add_one_sub_genus, ord_adicOfIrreducible_X) all check out. No overclaiming or stale text found.
🟡	proof-quality	changes requested	claude/claude-opus-5	Proofs are short and mostly robust, but the PR inlines the same three-line "every height-one prime of k[X] is ofIrreducible hq" derivation twice instead of factoring it, and Divisor.principal_X re-does an ite case split that two existing dedicated simp lemmas already close.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 89d0b3a. rubrics @ 98e9b07. Review spend: $15.91.}

[sqrt-of-2]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	agy/gemini-3.7-flash-high	The PR faithfully and correctly formalizes the rational function field divisor calculations, Riemann–Roch spaces, genus determination, and pole divisor degrees from Stichtenoth Sections 1.2 and 1.4. All statements are mathematically accurate with appropriate hypotheses and no vacuity.
✅	reuse	approved	agy/gemini-3.7-flash-high	The PR adds the divisor, Riemann–Roch space, and genus calculations for the rational function field without duplicating existing material. It cleanly factors shared height-one spectrum scaffolding and reuses existing dimension, degree, and valuation APIs throughout.
✅	scope	approved	agy/gemini-3.7-flash-high	The PR advances the Layer 3 milestone for the rational function field in the AlgebraicCurves roadmap as a single coherent unit. All supporting lemmas are proximate prerequisites for the target results.
✅	attribution	approved	agy/gemini-3.7-flash-high	All central mathematical sources (Stichtenoth, Algebraic Function Fields and Codes, Sections I.2 and I.4, Example 1.4.18, and Theorem 1.4.11) and Mathlib foundations are properly credited in the module docstrings and declarations.
✅	api-design	approved	agy/gemini-3.7-flash-high	The public API cleanly exposes the rational function field divisor and Riemann–Roch results required by Layer 3 of the AlgebraicCurves roadmap. All declarations are placed in their canonical namespaces with appropriate simp attributes and no over-exposed implementation details.
✅	generality	approved	agy/gemini-3.7-flash-high	All new declarations and lemma formulations sit at the natural level of generality over an arbitrary base field, with general results proved first and specialized cleanly without duplication.
✅	placement	approved	agy/gemini-3.7-flash-high	All declarations are placed in their canonical modules across RingTheory/Polynomial/HeightOneSpectrum.lean, Place/RatFunc/Basic.lean, Place/RatFunc/Order.lean, and RiemannRoch/RatFunc.lean. Imports across all modified and new files are minimal, specific, and directly used.
✅	naming	approved	agy/gemini-3.7-flash-high	All introduced declarations follow standard Mathlib naming conventions and match existing repository patterns in naming, namespace choices, and statement strength. No custom or unscoped notation is introduced.
✅	documentation	approved	agy/gemini-3.7-flash-high	All new and modified files include accurate module docstrings with proper literature citations, and every public declaration is clearly documented describing the mathematical result.
✅	proof-quality	approved	agy/gemini-3.7-flash-high	The proofs are concise, well-structured, and make effective use of robust automation such as omega and simp. Factoring out exists_monic_irreducible_eq_ofIrreducible and adicOfIrreducible_eq_adicOfIrreducible_iff cleanly eliminates duplicated reasoning across multiple sites.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head dda1832. rubrics @ 94d131c. Review spend: $1.35.}

[CBirkbeck]

🟡 api-design — request_changes codex/gpt-5.6-sol

The new canonical membership and finite-place characterization lemmas are missing normal-form automation annotations.

• TauCeti/FieldTheory/FunctionField/RiemannRoch/RatFunc.lean:104 — mem_riemannRochSpace_nsmul_ofPoint_infty_iff is the characteristic membership normal form for the computed space but is not tagged @[simp]. Fix: Add @[simp] so membership in this explicit Riemann–Roch space reduces to the polynomial degree condition.
• TauCeti/FieldTheory/FunctionField/Place/RatFunc/Basic.lean:261 — adicOfIrreducible_eq_adicOfIrreducible_iff and the companion disjointness theorem at line 302 are canonical constructor equality/disjointness rules but lack @[simp]. Fix: Mark both lemmas @[simp] so finite-place equalities normalize to Associated and finite-place/infinity contradictions close automatically.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 66s · 203.7k in / 1.9k out tokens · reviewing this diff · rubric}

[roed-math]

The second finding is fixed as suggested; the first one I have to contest, because the repo's simpNF lint rejects it.

Fixed: Place.adicOfIrreducible_eq_adicOfIrreducible_iff and Place.adicOfIrreducible_ne_infty (the disjointness theorem at Place/RatFunc/Basic.lean:302) are now both @[simp]. Both pass scripts/lint-env.sh and the build is green.

Contested: @[simp] on mem_riemannRochSpace_nsmul_ofPoint_infty_iff is not admissible. Its LHS is not in simp normal form: TauCeti.mem_riemannRochSpace_iff is already @[simp] and rewrites f ∈ riemannRochSpace D to the valuation condition, so the proposed @[simp] lemma can never fire. I tried it and scripts/lint-env.sh (Mathlib's #lint set, run in CI) fails with a new violation:

lint-env: NEW violation(s) not in the grandfathered baseline (as '<linter> <declaration>'):
  [simpNF]
  #check @TauCeti.mem_riemannRochSpace_nsmul_ofPoint_infty_iff /- Left-hand side simplifies from
    f ∈ TauCeti.riemannRochSpace (n • TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (TauCeti.Place.infty k))
  to
    ∀ (P : TauCeti.Place k (RatFunc k)),
      P.valuation f ≤ WithZero.exp (↑n * (TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (TauCeti.Place.infty k)).coeff P)
  using
    simp only [*, @TauCeti.mem_riemannRochSpace_iff, @TauCeti.AlgebraicGeometry.WeilDivisor.coeff_nsmul]
  Try to change the left-hand side to the simplified term! -/

LINT-ENV: FAIL — 1 new violation(s); see the list above

The only ways to land the tag would be a @[nolint simpNF] plus an entry in scripts/lint-nolints-allowlist.txt — scripts/ is human-owned and off-limits to this PR — or silencing the linter, which the repo forbids. Since the lemma is an explicit unfolding of a specific L(D) rather than a normal form, it is correct as a plain theorem; its two consumers (riemannRochSpace_nsmul_ofPoint_infty here) name it explicitly.

lake build, lake exe axioms and scripts/lint-env.sh are green at e25e651.

[sqrt-of-2]

Re: your reply on api-design — re-reviewed on e25e651; this clears the finding ✅ — approved on e25e651.

_{agy/gemini-3.7-flash-high · addresses your replies through comment 3879757968.}

[CBirkbeck]

🟡 placement — request_changes codex/gpt-5.6-sol

The new Riemann–Roch module contains independent divisor calculations that belong with divisor theory rather than Riemann–Roch.

• TauCeti/FieldTheory/FunctionField/RiemannRoch/RatFunc.lean:68 — Divisor.principal_irreducible, Divisor.principal_X, and Divisor.degree_poles_eq_max_natDegree (line 181) are standalone rational-function divisor/product-formula results and are not used by the Riemann–Roch or genus calculations in this file. Fix: Move all three declarations to a rational-function module under FieldTheory/FunctionField/Divisor and update imports; this also keeps the RatFunc.IntermediateField dependency out of the Riemann–Roch module.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 48s · 101.1k in / 1.4k out tokens · reviewing this diff · rubric}

[CBirkbeck]

AI review — changes requested

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	codex/gpt-5.6-sol	The new definitions and theorem statements faithfully capture the divisor, Riemann–Roch-space, dimension, genus, and pole-degree calculations for the rational function field, including zero, constant, and finite-place edge cases.
✅	reuse	approved	codex/gpt-5.6-sol	The new results are not already present in TauCeti or Mathlib, and the proofs reuse the relevant existing APIs rather than duplicating their implementations.
✅	scope	approved	codex/gpt-5.6-sol	The PR directly advances the AlgebraicCurves Layer 3 rational-function-field acceptance suite, and its supporting finite-place lemmas are proximate prerequisites within the same coherent topic.
✅	attribution	approved	codex/gpt-5.6-sol	The code credits Stichtenoth with specific theorem, proposition, example, and section references for the central constructions, and explicitly identifies the key Mathlib result underlying the finite-regularity argument.
🟡	api-design	changes requested	codex/gpt-5.6-sol	The new canonical membership and finite-place characterization lemmas are missing normal-form automation annotations.
✅	generality	approved	codex/gpt-5.6-sol	The new declarations use assumptions and abstraction levels natural to the rational-function-field calculations; no material generality issue was found.
🟡	placement	changes requested	codex/gpt-5.6-sol	The new Riemann–Roch module contains independent divisor calculations that belong with divisor theory rather than Riemann–Roch.
✅	naming	approved	codex/gpt-5.6-sol	The introduced declaration names accurately describe their conclusions, follow adjacent API terminology, and introduce no new notation.
✅	documentation	approved	codex/gpt-5.6-sol	The new substantive module has a clear module docstring, and every added public declaration is documented accurately in terms of its statement and purpose.
✅	proof-quality	approved	codex/gpt-5.6-sol	The added proofs are readable and appropriately factored, with no undocumented change/show, fragile definitional-equality tricks, or excessively long rewrite chains.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head dda1832. rubrics @ 98e9b07. Review spend: $2.77.}

[sqrt-of-2]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	agy/gemini-3.7-flash-high	All statements and definitions in this PR faithfully formalize the divisor and Riemann–Roch theory for the rational function field over an arbitrary base field, including the computation of principal divisors, Riemann–Roch spaces of multiples of the place at infinity, and the vanishing of the genus. The theorems match their mathematical counterparts without vacuous assumptions, missing hypotheses, or faked prerequisites.
✅	reuse	approved	agy/gemini-3.7-flash-high	The PR makes effective use of existing Mathlib and TauCeti infrastructure without duplicating existing definitions or scaffolding. Shared intermediate steps are cleanly factored into dedicated lemmas consumed across the relevant modules.
✅	scope	approved	agy/gemini-3.7-flash-high	The PR directly implements the Layer 3 target "The rational function field, at divisor level" of the AlgebraicCurves roadmap as a single coherent topic. All prerequisites are present on main, and the supporting lemmas directly serve the target's calculations.
✅	attribution	approved	agy/gemini-3.7-flash-high	All central mathematical sources (Stichtenoth, Sections I.2 and I.4, Theorem 1.4.11, and Example 1.4.18) and relevant Mathlib foundations are thoroughly credited in module and declaration docstrings.
✅	api-design	approved	agy/gemini-3.7-flash-high	The public API is clean, minimal, and complete, exposing the exact divisor, Riemann-Roch, and genus results required by the roadmap with correct automation annotations.
✅	generality	approved	agy/gemini-3.7-flash-high	All declarations are stated at their natural level of generality with minimal hypotheses, and special cases are cleanly derived from their general counterparts.
✅	placement	approved	agy/gemini-3.7-flash-high	All declarations are placed in their canonical modules across RingTheory/Polynomial, FunctionField/Place/RatFunc, FunctionField/Divisor, and FunctionField/RiemannRoch. Imports in both new and modified files are specific, minimal, and actively used.
✅	naming	approved	agy/gemini-3.7-flash-high	All introduced declarations follow standard Mathlib naming conventions, match their statement strengths and conclusions, and introduce no extraneous or unscoped notation.
✅	documentation	approved	agy/gemini-3.7-flash-high	All new files provide complete module docstrings with literature citations, and every added public declaration has an accurate docstring describing the mathematical result.
✅	proof-quality	approved	agy/gemini-3.7-flash-high	The proofs are concise, well-structured, and rely on robust automation and cleanly factored intermediate lemmas without fragile rewriting or undocumented definitional equality.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head e25e651. rubrics @ 94d131c. Review spend: $1.21.}