abel-theorem: the Serre functional (design §4.3, routing decision #2's "honest integration atom")

Unit: abel-theorem. Namespace RS.Abel.

The three analytic/linear-algebraic properties of the area pairing pairing PU σ θ built in AreaPairing.lean:

• pairing_dbar_eq_zero (Forster 19.6's Stokes half, PoU-globalized): dbar-exact (0,1)-forms pair to zero against every holomorphic 1-form. The proof is the compact-surface Stokes argument run entirely through the planar Atom 1 (integral_wirtingerDbar_eq_zero): per PoU chart, ψᵢ dbaru θᵢ = dbar(ψᵢ u θᵢ) - dbarψᵢ · u θᵢ, the first integral dies by compact-support Stokes, and the leftover ∑ᵢ ∫ dbarψᵢ · u θ dies after inserting ∑ⱼ ψⱼ = 1, transporting each (i,j) term into chart j by the (1,1)-density change of variables (integral_eq_integral_transition — the conj (deriv τ) · deriv τ = normSq (deriv τ) cancellation against Form01.compat-type conj-factors and coeffIn_trans), and summing ∑ᵢ dbarψᵢ = dbar1 = 0 in chart j.
• conjForm/pairingDual_injective (Forster 19.5's positivity, localized): the conjugate (0,1)-form theta-bar of a holomorphic 1-form pairs against θ to ∑ᵢ ∫ ψᵢ |θᵢ|² ≥ 0, zero only for θ = 0 — so θ ↦ pairing · θ is an INJECTION Form1 X ↪ Dual (H01 X). No Hodge theory: this is pointwise positivity of the integrand plus volume's open-positivity.
• exists_dbar_of_forall_pairing_eq_zero — the integral-pairing Dolbeault bridge: a (0,1)-form pairing to zero against EVERY holomorphic 1-form is dbar-exact. Gated (exactly like DolbeaultBridge.lean) only on serre-duality-tails's remaining external fact Function.Surjective (RS.LaurentTail.tailToH1 (0 : RS.Divisor X)): that surjectivity forces finrank (H01 X) = genus X (finrank_H01_eq_genus, via dolbeaultEquiv + H1Tail.equivOfSurjective + h1T_zero_eq_genus), whence the positivity injection is onto Dual (H01 X) by dimension count and Module.forall_dual_apply_eq_zero_iff closes.

This gives, for the Abel discharge, a bridge whose hypothesis (∫∫ η ∧ θ = 0 for all θ) is checkable against the weak-solution packaging (LogPiece.lean/UpgradeDischarge.lean) by concrete planar Stokes/residue computations — the shape DolbeaultBridge.lean's abstract residue-pairing hypothesis does not directly offer.

The Stokes vanishing: auxiliary integrands

Throughout, for a fixed u : SmoothC X and θ : Form1 X: stokesA PU u θ i is dbarψᵢ · u · θ read in chart i; stokesB PU u θ i j is its ψⱼ-weighted piece supported on the (i,j) overlap, still in chart i; stokesC PU u θ i j is the same piece transported to chart j.

theorem RS.Abel.pairing_dbar_eq_zero {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (u : SmoothC X) (θ : Form1 X) : pairing PU (dbar u) θ = 0

The compact-surface Stokes vanishing (Forster 19.6's exactness half): for every global smooth function u and holomorphic 1-form θ, ∫∫_X dbaru ∧ θ = 0. Fully unconditional.

The conjugate (0,1)-form and positivity

noncomputable def RS.Abel.conjForm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : Form1 X) : Form01 X

The conjugate (0,1)-form theta-bar of a holomorphic 1-form: chart coefficients conj (coeffIn e θ). The Form01.compat law is the conjugate of coeffIn_trans.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.Abel.conjForm_coeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : Form1 X) (x : X) {z : ℂ} (hz : z ∈ (chartAt ℂ x).target) : (conjForm θ).coeffAt x z = (starRingEnd ℂ) (coeffIn (chartAt ℂ x) θ z)

The chart coefficient of the conjugate form.

theorem RS.Abel.eq_zero_of_pairing_conjForm_eq_zero {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (θ : Form1 X) (h : pairing PU (conjForm θ) θ = 0) : θ = 0

The pairing of theta-bar against θ is the (complexified) integral of the nonnegative density ∑ᵢ ψᵢ |θᵢ|²; if it vanishes, θ = 0.

The pairing as a linear functional on H01 and the injection into the dual

noncomputable def RS.Abel.pairingFunctional {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (θ : Form1 X) : Form01 X →ₗ[ℂ] ℂ

The pairing against a fixed θ, as a linear functional on (0,1)-forms.

Equations

• RS.Abel.pairingFunctional PU θ = { toFun := fun (σ : RS.Form01 X) => RS.Abel.pairing PU σ θ, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def RS.Abel.pairingH01 {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (θ : Form1 X) : H01 X →ₗ[ℂ] ℂ

The pairing descends to the Dolbeault space H01 X (by pairing_dbar_eq_zero).

Equations

• RS.Abel.pairingH01 PU θ = RS.dbar.range.liftQ (RS.Abel.pairingFunctional PU θ) ⋯

@[simp]

theorem RS.Abel.pairingH01_mk {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (θ : Form1 X) (σ : Form01 X) : (pairingH01 PU θ) (H01.mk σ) = pairing PU σ θ

noncomputable def RS.Abel.pairingDual {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) : Form1 X →ₗ[ℂ] Module.Dual ℂ (H01 X)

The Serre functional θ ↦ ∫∫ · ∧ θ, as a linear map into the dual of H01 X.

Equations

• RS.Abel.pairingDual PU = { toFun := fun (θ : RS.Form1 X) => RS.Abel.pairingH01 PU θ, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.Abel.pairingDual_injective {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) : Function.Injective ⇑(pairingDual PU)

Positivity injection (Forster 19.5-19.6, Hodge-free): the Serre functional is injective on holomorphic 1-forms. Fully unconditional.

The gated dimension count and the integral-pairing bridge

theorem RS.Abel.finrank_H01_eq_genus {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] [DecidableEq X] (hsurj : Function.Surjective ⇑(LaurentTail.tailToH1 0)) : Module.finrank ℂ (H01 X) = genus X

Gated on serre-duality-tails's remaining external fact, the Dolbeault space has dimension exactly genus X (≥ is the unconditional tail injection; ≤ is the gate).

theorem RS.Abel.exists_dbar_of_forall_pairing_eq_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] [DecidableEq X] (PU : SurfPoU X) (hsurj : Function.Surjective ⇑(LaurentTail.tailToH1 0)) {η : Form01 X} (h : ∀ (θ : Form1 X), pairing PU η θ = 0) : ∃ (u : SmoothC X), dbar u = η

The integral-pairing Dolbeault bridge (the Serre-functional replacement for DolbeaultBridge.lean's abstract statement): if a smooth (0,1)-form pairs to zero against EVERY holomorphic 1-form, it is dbar-exact. Gated only on serre-duality-tails's remaining external fact (the same single gate as exists_dbar_eq_zero_of_forall_basis_pairing_eq_zero).

theorem RS.Abel.tailToH1_zero_surjective_iff_finrank_le {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] [DecidableEq X] : Function.Surjective ⇑(LaurentTail.tailToH1 0) ↔ Module.finrank ℂ (Cech.H1 0) ≤ genus X

The single remaining gate, reformulated as a pure dimension count: tailToH1 0 is surjective iff the Čech H¹(𝒪_X) has dimension at most genus X. (The ≥ inequality is the unconditional tail injection H1Tail.toH1_injective + h1T_zero_eq_genus; classically the ≤ direction is Forster §17.9's Serre-duality counting — the one fact of this challenge that remains open, everything else in Jacobian/Abel now being reduced to it.)