🤖 Propose jacobian-fable: the Jacobian of a compact Riemann surface (Abel-Jacobi, Riemann-Roch, Serre duality)

[rkirov]

🤖 Proposes jacobian-fable (rkirov/jacobian-fable, Apache-2.0) for the pool: a from-scratch construction of the Jacobian of a compact Riemann surface, answering Kevin Buzzard's "Jacobian challenge".

213 files, ~46.8k lines of Lean, ~30 units. The development builds J(X) = ℂ^g / Λ honestly — no vacuous carriers — and proves the surrounding theory it needs along the way:

• genus X as dim Ω¹(X), with genus_eq_zero_iff_homeo: genus 0 iff X is homeomorphic to S²;
• the period lattice Λ, proved discrete of rank 2g, giving J(X) its AddCommGroup, ChartedSpace, IsManifold, LieAddGroup, T2Space and CompactSpace instances;
• the Abel–Jacobi map Jacobian.ofCurve and Abel's theorem in the form ofCurve_inj;
• functoriality: pushforward/pullback with their identity and composition laws, ContMDiff.degree, and the projection formula pushforward_pullback;
• the supporting theory, which is the bulk of it: Riemann–Roch, Serre duality via Miranda's Laurent tails (no Hodge theory), the residue theorem ∑ Res = 0 through the trace to ℙ¹, Dolbeault/Čech comparison, finite-dimensionality of H¹(X, 𝒪_D) via Schwartz/Montel, and a Čech counting argument giving h¹(0) ≤ g.

Status against the pool's gates

Already met: sorry-free; axioms exactly propext, Classical.choice, Quot.sound on every headline result; no unsafe/partial/opaque/axiom/@[extern]; no diagnostic commands in library code; targeted Mathlib.* imports (no broad import Mathlib); largest file 1,496 code lines. Provenance is AI — produced by an autonomous orchestrator with ~70 design/build/fix agents (Fable 5 designing and finishing, Sonnet building), with no human mathematical input; the reference texts were Forster, Miranda and Griffiths–Harris.

An external check exists for the headline statements: the same library is the accepted solution to the jacobian_challenge_diffgeo problem in leanprover/lean-eval, where leanprover/comparator verifies that the 24 challenge declarations match Buzzard's trusted statements, that the axioms are within the permitted set, and replays the proofs through the kernel and through nanoda. So the statements being proved are Buzzard's, not ours — which should settle the usual vacuity question.

Known gaps for an import, measured, not guessed:

• 70 set_options — 41 maxHeartbeats, 15 backward.isDefEq.respectTransparency, 7 synthInstance.maxHeartbeats, 7 linter.* disables. This is the substantive one, since dropping the heartbeat raises means those proofs have to close inside the default budget.
• 14 declarations over the 200-line proof cap, the largest 407 lines; they need splitting into named lemmas.
• 301 build warnings, dominated by 197 unused-section-variable notices (each of which prints its own omit … in fix), plus 36 unused variable names, 12 unused simp arguments, 7 overlapping instance parameters, and some deprecations.
• No four-line file headers on any of the 213 files, and 140 lines over 100 characters.
• Currently pinned to v4.32.2 / Mathlib 905b9581, so it needs a bump to the pool's v4.33.0-rc1 / 79d0395a.

I am working through that list regardless of the outcome here, since it is a straight improvement to the repository. The question for you is whether the project is one you want in the pool — if so I can open the content PR under LeanPool/JacobianDiffgeo/ once the gates are clean, or leave the import to a maintainer, whichever you prefer. Reservoir does not index the repo, so it would need a candidates/manual.txt entry either way.

[rkirov]

👨 let me know if this is a good fit to open PR. I am improving the quality to match in the meantime, don't see any blockers.