CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Riemann inequality

Statement

Assume the Axiom of Choice, inherited from the Riemann-Roch and finiteness suppliers below. Let $k$ be a field, let $C$ be a smooth proper geometrically integral curve over $k$ (Curves over a field) with genus $g = h^{1} (C, O_{C}) = 1 - χ (C, O_{C})$ (Genus via the Euler characteristic), and let $D$ be a divisor on $C$ (Divisors on a smooth proper curve). Then $l (D) = h^{0} (D) \geq \deg_{k} (D) + 1 - g,$ where $l (D) = \dim_{k} L (D) = h^{0} (D)$ and $h^{i} (D) = \dim_{k} H^{i} (C, O_{C} (D))$ are the integers of The Riemann-Roch dimension l(D). The inequality is the Riemann inequality; it is generally strict, the excess being the index of speciality, and it is not used here to produce sections.

The attachment of $O_{C} (D)$ and the identification of $L (D)$ with $H^{0} (C, O_{C} (D))$ use the current interfaces Invertible sheaf of cartier divisor, Rational sections of line bundles are Cartier divisors and Cartier and Weil divisors agree on a smooth curve, inherited through Riemann-Roch for curves: the Euler-characteristic form.

Facts & Assumptions

Given: a field $k$ , a smooth proper geometrically integral curve $C$ over $k$ with genus $g = h^{1} (C, O_{C})$ , and a divisor $D$ on $C$ .

[F1]

The curve $C$ is proper, of finite type and of chain dimension one over the field $k$ ; a divisor on $C$ is a finite formal integral combination of closed points and $\deg_{k} : Div (C) \to Z$ is the $k$ -degree homomorphism (Curves over a field, Divisors on a smooth proper curve).

[F2]

The integers $l (D)$ and $h^{i} (D)$ : $l (D) = \dim_{k} L (D) = \dim_{k} H^{0} (C, O_{C} (D)) = h^{0} (D)$ is a nonnegative integer, and $h^{i} (D) = \dim_{k} H^{i} (C, O_{C} (D))$ for every $i \geq 0$ ; in particular $h^{1} (D)$ is the dimension of a $k$ -vector space (The Riemann-Roch dimension l(D), Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis).

[F3]

Riemann-Roch in Euler-characteristic form: for the genus $g = g (C) = h^{1} (C, O_{C})$ and every divisor $D$ on $C$ , $h^{0} (D) - h^{1} (D) = χ (C, O_{C} (D)) = \deg_{k} (D) + 1 - g$ ; no Serre duality is used (Riemann-Roch for curves: the Euler-characteristic form).

[F4]

The current interfaces Invertible sheaf of cartier divisor, Rational sections of line bundles are Cartier divisors and Cartier and Weil divisors agree on a smooth curve attach $O_{C} (D)$ and identify $L (D)$ with its global sections; this use is inherited from [F3].

[F5]

The Axiom of Choice is used exactly through the Riemann-Roch supplier [F3] and the finiteness supplier [F2], which inherit it from the proper-cohomology suppliers; no further selection is made below (The Axiom of Choice).

Proof

technique · direct; rearrange the Riemann-Roch identity into $h^0(D)=$ right-hand side $+$ $h^1(D)$ and use that a dimension is nonnegative

1.1F1F2F3

Set-up. By [F1] the curve $C$ is proper over $k$ and $D$ is a divisor on $C$ with $k$ -degree $\deg_{k} (D)$ . By [F2] the integer $l (D)$ equals $h^{0} (D) = \dim_{k} H^{0} (C, O_{C} (D))$ , and $h^{1} (D) = \dim_{k} H^{1} (C, O_{C} (D))$ is the dimension of a $k$ -vector space, hence nonnegative by [F2]. By [F3] the identity $h^{0} (D) - h^{1} (D) = \deg_{k} (D) + 1 - g$ holds for the divisor $D$ and the genus $g = h^{1} (C, O_{C})$ of the curve.

2.1F2step 1.1

The inequality. Adding $h^{1} (D)$ to both sides of the identity of step 1.1 gives $h^{0} (D) = \deg_{k} (D) + 1 - g + h^{1} (D)$ ; since $h^{1} (D) \geq 0$ , the right-hand side is at least $\deg_{k} (D) + 1 - g$ , so $h^{0} (D) \geq \deg_{k} (D) + 1 - g$ . As $l (D) = h^{0} (D)$ by [F2], this is exactly the asserted inequality $l (D) \geq \deg_{k} (D) + 1 - g$ .

3.1F2F3F4F5step 2.1∎

Conclusion and choice accounting. Step 2.1 proves $l (D) = h^{0} (D) \geq \deg_{k} (D) + 1 - g$ for every divisor $D$ on $C$ , the identity $l (D) = h^{0} (D)$ being the definitional identification of [F2]. The Axiom of Choice is used only through the suppliers recorded in [F5], namely the Riemann-Roch theorem [F3] and the finiteness supplier [F2]; the deduction itself makes no selection, and the flagged dictionary [F4] records the inherited obligation on $O_{C} (D)$ .

Depends on

Used by

Rational functions with poles bounded at one point Corollary
A negative right-hand side does not contradict Riemann-Roch Counterexample
A genus-zero curve with a degree-one divisor is the projective line Theorem

Dependency tree · two levels

76 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

William Fulton, Algebraic Curves (Internet Archive copy), Chs. 8 and 6 (standard reference, not scraped)
Michael Artin, MIT 18.721 Introduction to Algebraic Geometry (July 20, 2020 notes), Ch. 8 (standard reference, not scraped)
The Stacks Project, Algebraic Curves (tag 0BRV) (standard reference, not scraped)