Function-field vocabulary and Riemann's inequality: a formal genus bound for the Weil input

[daira]

The cited Weil input at the branch covers (#29) takes its per-cover constant from a genus fact whose statement needs vocabulary that Mathlib does not have. #28 deliberately scopes that vocabulary out; this issue tracks it, on the route that stops short of exact genus.

The route — all commutative algebra and valuation theory; no schemes, no differentials:

• places of a function field F/K as discrete valuations trivial on K; place degrees; divisors;
• Riemann spaces L(D): finiteness, and the one-place growth bound ℓ(D + P) ≤ ℓ(D) + deg P;
• the pole divisor and the fundamental identity deg (x)_∞ = [F : K(x)] (Stichtenoth 1.4.11);
• the genus, well-defined via Riemann's theorem (sup_D (deg D + 1 - ℓ(D)) is finite — the finiteness proof is essentially the same counting as the next item);
• Riemann's inequality (Stichtenoth §3.11): for F = K(x, y), g ≤ ([F : K(x)] - 1)·([F : K(y)] - 1). At a branch cover F = F_q(u)(W) with W² = H(u) and deg H = 14, the 2r + 2 independent elements {uⁱ, uⁱ·W : i ≤ r} lie in L(r·(u)_∞ + (W)_∞), a divisor of degree 2r + 14; so g ≤ (2r + 14) + 1 - (2r + 2) = 13.

The payoff. The citation shrinks from "Weil/FFSTV Theorem 3 at covers of genus 6, computed on paper" to "Weil/FFSTV Theorem 3 at covers of formally bounded genus", leaving only the covering condition and Weil's theorem itself on paper. On constants: genus ≤ 13 gives the per-cover constant c = 2·13 - 2 = 24 (the parameter of weilBounded_zeroRepaired), so the recorded WeilBounded constant becomes C = c + 1/2 = 24.5, against the deployed C = 21/2 at c = 10. The chain is already parametric in c, so consumers change only at the final instantiation; the cost is (24.5/10.5)² ≈ 2^{2.44} in the regularity distance.

Out of scope here: exact genus 6 (the Riemann–Hurwitz tier), the no-unramified-subcover condition, and Weil's theorem itself (the Bombieri–Stepanov project).

🤖 Claude Fable 5

[daira]

A survey of the formalization landscape relevant to this route, with local verification of the headline claims. Conclusion first: the vocabulary-and-genus tier this issue tracks is no longer the long pole; the mathematics still uncovered by any existing effort is confined to the finite-constant-field layer (zeta rationality, the functional equation, the Riemann hypothesis for curves, and the character-sum transfer).

vaca22/riemann-roch-function-fields (Guanghao Li, Apache-2.0) is a complete function-field Riemann–Roch by the Stichtenoth route, and the claim survives verification: building the library from source (Lean v4.31.0) and running #print axioms over the headline declarations —riemann_roch in exactly the Thm 1.5.15 form, duality, clifford, exists_isCanonical, the chart↔intrinsic-place transport, finrank Ω_F = 1, and the genus-one applications— yields exactly [propext, Classical.choice, Quot.sound], with no sorry or native_decide anywhere in the library and the audit enforced in CI. One caveat: the headline theorems carry [Algebra.IsSeparable k⟮X⟯ K] alongside the full-constant-field hypothesis, so this is the separable slice of the theory — harmless for our covers, whose base fields are finite hence perfect and whose charts have degree 2 in odd characteristic. Parts are being upstreamed to Mathlib as open pull requests, including #41729 (the divisor-group core). Consequence for this issue: the route's statements —places, divisors, L(D) with the one-place growth bound, deg (x)_∞ = [F : K(x)], the genus via Riemann's theorem, and Riemann's inequality— could be stated against, or adapted from, this development today, subject to coordinating with its author.

TauCetiRoadmap/AlgebraicCurves is a written, reviewed roadmap for exactly this theory (function-field-first, following Stichtenoth). Its Layers 0 and 3 match this issue's route nearly item for item, and its later layers cover what this issue scopes out: tower multiplicativity of ramification and the Eisenstein/Kummer vocabulary for the no-unramified-subcover condition (Layer 6), Riemann–Hurwitz (Layer 7), and the hyperelliptic genus formula (Layer 10) — the exact-genus-6 tier. It explicitly defers zeta functions and everything over finite constant fields as such (Stichtenoth Ch. 5) to a future CurvesOverFiniteFields roadmap that no one has yet written. That unwritten roadmap is precisely where the remaining cited input (Weil's theorem in the form of FFSTV Lemma 1 and Theorem 3) lives, and proposing it —the Riemann hypothesis for curves by Bombieri's Riemann–Roch-only route, plus the character-sum transfer along abelian covers— looks like the highest-leverage next step; this issue and #28 are its natural named consumers.

The Hasse bound is done at genus 1. AINTLIB's HasseWeil project (Chris Birkbeck) proves the unconditional |#E(𝔽_q) − q − 1| ≤ 2√q with no hypotheses beyond finiteness of the field, and local verification agrees with the blueprint's sorry-free claim: the capstone hasse_bound audits to exactly the standard three axioms. The route is Silverman V.1 (Weil-pairing scalings, dual isogenies, the degree quadratic form), which is genus-1-specific —it does not shorten the higher-genus Weil input— but it is the g = 1 case of the needed theorem in verified form, and its elliptic infrastructure is reusable on the E′ side of the covers. AINTLIB's separate number-field Chebotarev development is worth noting for a different reason: the effective function-field Chebotarev shares its L-function engine with the character-sum input, so a CurvesOverFiniteFields development would serve both — and would incidentally allow the D₄ Frobenius-statistics cross-check in design/weil-constant-derivation.md to be upgraded from evidence to theorem, though the bound never needs it.

lean-pool is a maintained, CI-gated pool of sorry-free formalizations pinned to current Mathlib, with a kernel-judged challenge board. It is a plausible maintenance home for the Riemann–Roch development (its model is exactly the adoption of permissively-licensed sorry-free repos, kept building), and a venue where the CharSumBounded inputs could be posted as challenges once the vocabulary makes them statable.

Bottom line for this issue: verified function-field Riemann–Roch exists with Mathlib upstreaming in progress, and a reviewed roadmap covers everything through Riemann–Hurwitz and the hyperelliptic genus, so the tracked route could now be discharged by consumption and adaptation rather than greenfield work. What remains without any formalization effort behind it is exactly Stichtenoth Ch. 5 plus the character-sum transfer. The two concrete moves are to shape this issue's statements against the existing Riemann–Roch vocabulary in coordination with its author, and to propose the CurvesOverFiniteFields roadmap to Tau Ceti with #28 and this issue as named consumers.

Posted with the assistance of Claude Fable 5.