Documentation

LeanPool.JacobianDiffgeo.Abel

abel-theorem: Abel's theorem (Forster 20.7, dissection-free), ofCurve_inj #

Unit: abel-theorem (docs/design/abel-theorem.md). Blueprint #29: "Abel's theorem (Forster 20.7, dissection-free): the two-point Abel–Jacobi value is nonzero for distinct points on g ≥ 1, hence ofCurve is injective." Namespace RS.Abel for the internal proof pipeline; Jacobian for the challenge-shaped final exports. No fundamental-polygon/cut-surface machinery anywhere (the blueprint's ⚠ is honored); no Jacobian.Monodromy/Jacobian.FormTrace import anywhere in this unit (confirmed at build time, matching the design's DAG audit §3).

Status: design steps 5-7 (the WeakSolutionUpgrade/WeakSolutionUpgradeFinset content — packaging a weak solution's chart-local dbarlog f data into a global Form01 X, the vanishing pairing, the dbar-correction, and the CR-promotion/order bookkeeping) are now DISCHARGED (AreaPairing.lean + SerreFunctional.lean + ChartSupported.lean + LogPiece.lean + LinkData.lean + UpgradeDischarge.lean, this pass), gated ONLY on serre-duality-tails's one remaining external fact Function.Surjective (RS.LaurentTail.tailToH1 (0 : RS.Divisor X)) — the SAME single gate DolbeaultBridge.lean already carries, so the unit's total gate set has SHRUNK to that one fact (plus period-lattice-rank's [DiscreteTopology] instance, that unit's job): RS.Abel.weakSolutionUpgrade_of_surjective : (surjectivity) → WeakSolutionUpgrade X and RS.Abel.weakSolutionUpgradeFinset_of_surjective (the k-point form), consumed by the new Jacobian.ofCurve_inj_of_surjective'/ofCurve_inj_of_surjective. The blueprint's routing decision #2 "honest integration atom" — the Dolbeault-side Serre functional (σ, θ) ↦ ∫∫_X σ ∧ θ — is BUILT (RS.Abel.pairing), with the compact-surface Stokes vanishing (pairing_dbar_eq_zero, unconditional), the conjugate-form positivity injection (pairingDual_injective, unconditional, Hodge-free), and the integral-pairing bridge (exists_dbar_of_forall_pairing_eq_zero, same single gate). scripts/check.sh Jacobian/Abel reports zero sorries.

The AbelWeak gap closure (authorized edit, not part of this unit's own files) #

This unit's design (docs/design/abel-theorem.md §2.1) needs the FULLY GENERAL two-point weak solution RS.AbelWeak.exists_weakSolutionOfPair (for an arbitrary connecting path, not confined to one chart) — abel-weak-solutions' own build pass had explicitly left this as a documented gap (a missing "rechart" lemma for IsWeakSolutionAt across chart transitions). This builder closed it, as authorized, inside Jacobian/AbelWeak/ (Rechart.lean + GeneralChain.lean, zero sorries, scripts/check.sh Jacobian/AbelWeak passes) — see that unit's own root docstring for the full mathematical account (the removable-singularity-theorem rechart lemma, the general order-additive IsWeakSolutionAt.mul, and the chain induction gluing SingleChart pieces at every breakpoint, including the case where the path revisits its own basepoint).

API summary #

Notes for period-lattice-rank (#31), the primary consumer #

  1. The k-point sufficiency direction IS now exported (RS.Abel.exists_mero_of_ periodVector_mem, design §4.1/§6 — this design's own finding, §1.4, is that Forster 21.4(b)'s own proof needs this general form, not just the two-point case), gated on RS.Abel.WeakSolutionUpgradeFinset X ι (the Finset analogue of WeakSolutionUpgrade, same remaining content, see Sufficiency.lean's docstring).
  2. Once period-lattice-rank proves discreteness (Forster 21.4(b), which itself CITES this unit's sufficiency direction — see the design's §1.2 ordering-resolution account), please register both instance : DiscreteTopology (RS.periodSubgroup X) (feeds ofCurve_inj' directly) and instance : DiscreteTopology (RS.periodSubgroup X).topologicalClosure (feeds jacobian-construction's existing gates) — both are cheap corollaries of the same discreteness proof via AddSubgroup.isClosed_of_discrete (§4.4/§9 of the design).
  3. Final assembly discharge shape: once (1) RS.Abel.WeakSolutionUpgrade/ WeakSolutionUpgradeFinset are proved (design steps 5+7 — serre-duality-tails's own external blocker has already cleared, see DolbeaultBridge.lean) and (2) the DiscreteTopology (RS.periodSubgroup X) instance above is registered globally, Jacobian.ofCurve_inj becomes literally callable with NO explicit hypothesis/instance argument — the exact statement at docs/Jacobian_challenge.lean:99 is already what ofCurve_inj''s conclusion states verbatim, so final assembly is a zero-content rewrap, not new proof work.
  4. Exact k-point export signature (for direct citation):
    theorem RS.Abel.exists_mero_of_periodVector_mem {ι : Type*} [Fintype ι] [DecidableEq ι]
    (hupgradeFinset : RS.Abel.WeakSolutionUpgradeFinset X ι)
    (a x : ι → X) (ha : Function.Injective a) (hx : Function.Injective x)
    (hax : ∀ i j, a i ≠ x j) (γ : (i : ι) → Path (a i) (x i))
    (hmem : (fun k => ∑ i, RS.pathIntegral (γ i) (RS.basis X k)) ∈ RS.periodSubgroup X) :
    ∃ F : RS.Mero X, F ≠ 0 ∧ (∀ i, F.ord (x i) = 1) ∧ (∀ i, F.ord (a i) = -1) ∧
      ∀ z, (∀ i, z ≠ a i) → (∀ i, z ≠ x i) → F.ord z = 0