abel-theorem: the Serre area-pairing infrastructure (design §4.3, routing decision #2)

Unit: abel-theorem. Namespace RS.Abel.

The blueprint's routing decision #2 budgeted ONE "honest integration atom" for the whole challenge: the Dolbeault-side Serre functional (σ, ω) ↦ ∫∫_X σ ∧ ω pairing a smooth (0,1)-form σ : Form01 X against a holomorphic 1-form ω : Form1 X. This file builds its foundation:

• SurfPoU X — a finite smooth partition of unity subordinate to preferred-chart sources (from RS.exists_smoothPartitionOfUnity + compactness; SurfPoU.nonempty).
• planar helpers — the indicator-extension smoothness gadget (contDiff_indicator_of_eq_zero_off, hasCompactSupport_indicator_of_eq_zero_off), the chart-inverse ContDiffOn bridges (contDiffOn_comp_symm_of_contMDiffOn, contDiffOn_comp_symm_real), the holomorphic-Jacobian determinant identity (det_fderiv_restrictScalars_eq_normSq, the residue-theorem design's spike-verified fact), and the biholomorphic change-of-variables atom integral_eq_integral_transition: a planar integrand supported on the image of a chart overlap can be transported to the other chart at the cost of the (1,1)-density factor Complex.normSq (deriv τ) — exactly how σ ∧ ω transforms (Form01.compat's conj (deriv τ) times coeffIn_trans's deriv τ).
• pairing PU σ θ — the pairing itself, ∑ i, ∫ z, ψ_i(z) · σ_i(z) · ω_i(z) dA over the fixed partition PU, with integrability (integrable_pairingTerm) and bilinearity (pairing_add_left/pairing_smul_left/pairing_add_right/pairing_smul_right).

SerreFunctional.lean proves the two analytic properties (dbar-exact forms pair to zero; positivity against the conjugate form); ChartSupported.lean localizes the pairing for single-chart-supported (0,1)-data. No independence-of-PU statement is ever needed: every downstream conclusion is a Prop quantified over a single fixed PU.

Planar helpers

theorem RS.Abel.contDiff_indicator_of_eq_zero_off {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℂ → E} {T K : Set ℂ} (hT : IsOpen T) (hK : IsCompact K) (hKT : K ⊆ T) (hF : ContDiffOn ℝ (↑⊤) F T) (h0 : ∀ z ∈ T, z ∉ K → F z = 0) : ContDiff ℝ (↑⊤) (T.indicator F)

Indicator-extension smoothness gadget: if F is smooth on the open set T and vanishes on T \ K for a compact K ⊆ T, then the indicator extension of F by 0 is globally smooth.

theorem RS.Abel.hasCompactSupport_indicator_of_eq_zero_off {E : Type u_2} [NormedAddCommGroup E] {F : ℂ → E} {T K : Set ℂ} (hK : IsCompact K) (h0 : ∀ z ∈ T, z ∉ K → F z = 0) : HasCompactSupport (T.indicator F)

Companion to contDiff_indicator_of_eq_zero_off: the indicator extension has compact support (inside K).

theorem RS.Abel.integrable_indicator_of_eq_zero_off {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℂ → E} {T K : Set ℂ} (hT : IsOpen T) (hK : IsCompact K) (hKT : K ⊆ T) (hF : ContDiffOn ℝ (↑⊤) F T) (h0 : ∀ z ∈ T, z ∉ K → F z = 0) : MeasureTheory.Integrable (T.indicator F) MeasureTheory.volume

Integrability of the indicator-extension gadget.

Chart-inverse smoothness bridges

theorem RS.Abel.contDiffOn_comp_symm_of_contMDiffOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℂ} {s : Set X} (hu : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) u s) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) : ContDiffOn ℝ (↑⊤) (u ∘ ↑e.symm) (↑e '' (s ∩ e.source))

ContMDiffOn data on X reads as planar ContDiffOn data through the inverse of any maximal-atlas chart (the "any-chart" analogue of SmoothC.contDiffOn_comp_chartAt_symm).

theorem RS.Abel.contDiffOn_comp_symm_real {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {ψ : X → ℝ} (hψ : ContMDiff (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℝ) (↑⊤) ψ) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) : ContDiffOn ℝ (↑⊤) (ψ ∘ ↑e.symm) e.target

The real-valued global version: a ContMDiff real function on X reads as planar ContDiffOn data on any maximal-atlas chart target.

theorem RS.Abel.contDiffOn_coeffIn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : Form1 X) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) : ContDiffOn ℝ (↑⊤) (coeffIn e θ) e.target

Holomorphic-coefficient smoothness: the chart coefficient of a holomorphic 1-form is real-smooth on the chart target.

The holomorphic Jacobian determinant (residue-theorem design §1.6, spike-verified)

theorem RS.Abel.det_fderiv_eq_normSq_deriv {τ : ℂ → ℂ} {ζ : ℂ} (hτ : DifferentiableAt ℂ τ ζ) : (fderiv ℝ τ ζ).det = Complex.normSq (deriv τ ζ)

The planar real Jacobian determinant of a holomorphic map is normSq of its complex derivative.

The biholomorphic change-of-variables atom

theorem RS.Abel.integral_eq_integral_transition {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {F G : ℂ → ℂ} (hF0 : ∀ z ∉ ↑e '' (e.source ∩ e'.source), F z = 0) (hG0 : ∀ w ∉ ↑e' '' (e.source ∩ e'.source), G w = 0) (hFG : ∀ w ∈ ↑e' '' (e.source ∩ e'.source), G w = Complex.normSq (deriv (↑e ∘ ↑e'.symm) w) • F (↑e (↑e'.symm w))) : ∫ (z : ℂ), F z = ∫ (w : ℂ), G w

The (1,1)-density change of variables between charts (the "honest integration atom"'s transport step): if F vanishes off e '' (e.source ∩ e'.source), G vanishes off e' '' (e.source ∩ e'.source), and on that overlap image G is the normSq (deriv τ)-weighted transport of F along the transition τ = e ∘ e'.symm, then the two plane integrals agree.

The finite subordinate partition of unity

structure RS.Abel.SurfPoU (X : Type u_1) [TopologicalSpace X] [ChartedSpace ℂ X] : Type u_1

A finite smooth partition of unity on the compact surface X, subordinate to preferred-chart sources: the fixed auxiliary datum the Serre pairing is built over.

• n : ℕ

  The number of members.

• pt : Fin self.n → X

  The chart centers.

• ψ : Fin self.n → X → ℝ

  The partition functions.

• contMDiff (i : Fin self.n) : ContMDiff (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℝ) (↑⊤) (self.ψ i)
• nonneg (i : Fin self.n) (x : X) : 0 ≤ self.ψ i x
• sum_eq_one (x : X) : ∑ i : Fin self.n, self.ψ i x = 1
• tsupport_subset (i : Fin self.n) : tsupport (self.ψ i) ⊆ (chartAt ℂ (self.pt i)).source

theorem RS.Abel.SurfPoU.nonempty {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] : Nonempty (SurfPoU X)

Existence of a SurfPoU on a compact surface.

@[reducible, inline]

noncomputable abbrev RS.Abel.SurfPoU.chart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (PU : SurfPoU X) (i : Fin PU.n) : OpenPartialHomeomorph X ℂ

The i-th chart of the partition datum.

Equations

• PU.chart i = chartAt ℂ (PU.pt i)

theorem RS.Abel.SurfPoU.chart_mem_maximalAtlas {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (i : Fin PU.n) : PU.chart i ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X

def RS.Abel.SurfPoU.K {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (PU : SurfPoU X) (i : Fin PU.n) : Set ℂ

The compact planar carrier of the i-th partition member.

Equations

• PU.K i = ↑(PU.chart i) '' tsupport (PU.ψ i)

theorem RS.Abel.SurfPoU.isCompact_K {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [CompactSpace X] (PU : SurfPoU X) (i : Fin PU.n) : IsCompact (PU.K i)

theorem RS.Abel.SurfPoU.K_subset_target {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (PU : SurfPoU X) (i : Fin PU.n) : PU.K i ⊆ (PU.chart i).target

theorem RS.Abel.SurfPoU.psi_symm_eq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (PU : SurfPoU X) (i : Fin PU.n) {z : ℂ} (hz : z ∈ (PU.chart i).target) (hzK : z ∉ PU.K i) : PU.ψ i (↑(PU.chart i).symm z) = 0

Off the compact carrier, the transported partition function vanishes.

theorem RS.Abel.SurfPoU.psi_symm_eventually_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [CompactSpace X] (PU : SurfPoU X) (i : Fin PU.n) {z : ℂ} (hzK : z ∉ PU.K i) : ∀ᶠ (w : ℂ) in nhds z, (PU.chart i).target.indicator (fun (w : ℂ) => PU.ψ i (↑(PU.chart i).symm w)) w = 0

The transported partition function vanishes on a whole neighborhood of any point outside the compact carrier (including points outside the chart target).

noncomputable def RS.Abel.SurfPoU.psiC {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (PU : SurfPoU X) (i : Fin PU.n) (e : OpenPartialHomeomorph X ℂ) : ℂ → ℂ

The complexified partition function read through an arbitrary chart.

Equations

• PU.psiC i e w = ↑(PU.ψ i (↑e.symm w))

theorem RS.Abel.SurfPoU.contDiffOn_psiC {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (PU : SurfPoU X) (i : Fin PU.n) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) : ContDiffOn ℝ (↑⊤) (PU.psiC i e) e.target

theorem RS.Abel.SurfPoU.psiC_eventuallyEq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (PU : SurfPoU X) (i : Fin PU.n) {e : OpenPartialHomeomorph X ℂ} {z : ℂ} (hz : z ∈ e.target) (hy : ↑e.symm z ∉ tsupport (PU.ψ i)) : PU.psiC i e =ᶠ[nhds z] 0

The complexified partition function vanishes near any target point whose source point is outside the support.

theorem RS.Abel.SurfPoU.wirtingerDbar_psiC_eq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (PU : SurfPoU X) (i : Fin PU.n) {e : OpenPartialHomeomorph X ℂ} {z : ℂ} (hz : z ∈ e.target) (hy : ↑e.symm z ∉ tsupport (PU.ψ i)) : wirtingerDbar (PU.psiC i e) z = 0

theorem RS.Abel.SurfPoU.differentiableAt_psiC {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (PU : SurfPoU X) (i : Fin PU.n) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {z : ℂ} (hz : z ∈ e.target) : DifferentiableAt ℝ (PU.psiC i e) z

theorem RS.Abel.SurfPoU.sum_psiC_eventuallyEq_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (PU : SurfPoU X) {e : OpenPartialHomeomorph X ℂ} {z : ℂ} (hz : z ∈ e.target) : (fun (w : ℂ) => ∑ i : Fin PU.n, PU.psiC i e w) =ᶠ[nhds z] fun (x : ℂ) => 1

On a chart target, the complexified partition functions sum to 1 near every point.

Planar sum rule for dbar and eventual-vanishing helpers

theorem RS.Abel.wirtingerDbar_finset_sum {ι' : Type u_2} (s : Finset ι') {f : ι' → ℂ → ℂ} {z : ℂ} (hf : ∀ i ∈ s, DifferentiableAt ℝ (f i) z) : wirtingerDbar (fun (w : ℂ) => ∑ i ∈ s, f i w) z = ∑ i ∈ s, wirtingerDbar (f i) z

theorem RS.Abel.indicator_eventuallyEq_zero_of_notMem {E : Type u_2} [Zero E] {F : ℂ → E} {T K : Set ℂ} (hK : IsCompact K) (h0 : ∀ z ∈ T, z ∉ K → F z = 0) {z : ℂ} (hz : z ∉ K) : T.indicator F =ᶠ[nhds z] 0

Indicator functions vanishing off a compact carrier vanish on a neighborhood of any point outside the carrier.

The pairing

noncomputable def RS.Abel.pairingTerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (σ : Form01 X) (θ : Form1 X) (i : Fin PU.n) : ℂ → ℂ

The i-th planar integrand of the Serre pairing: ψ_i · σ_i · ω_i read in the i-th chart, extended by 0 off the chart target.

Equations

• RS.Abel.pairingTerm PU σ θ i = (PU.chart i).target.indicator fun (z : ℂ) => PU.ψ i (↑(PU.chart i).symm z) • (σ.coeffAt (PU.pt i) z * RS.coeffIn (PU.chart i) θ z)

theorem RS.Abel.pairingTerm_core_eq_zero_off {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (σ : Form01 X) (θ : Form1 X) (i : Fin PU.n) (z : ℂ) : z ∈ (PU.chart i).target → z ∉ PU.K i → PU.ψ i (↑(PU.chart i).symm z) • (σ.coeffAt (PU.pt i) z * coeffIn (PU.chart i) θ z) = 0

The core of the pairing integrand vanishes on the chart target off the compact carrier.

theorem RS.Abel.contDiffOn_pairingTerm_core {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (σ : Form01 X) (θ : Form1 X) (i : Fin PU.n) : ContDiffOn ℝ (↑⊤) (fun (z : ℂ) => PU.ψ i (↑(PU.chart i).symm z) • (σ.coeffAt (PU.pt i) z * coeffIn (PU.chart i) θ z)) (PU.chart i).target

Smoothness of the pairing integrand core on the chart target.

theorem RS.Abel.contDiff_pairingTerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] (PU : SurfPoU X) (σ : Form01 X) (θ : Form1 X) (i : Fin PU.n) : ContDiff ℝ (↑⊤) (pairingTerm PU σ θ i)

theorem RS.Abel.hasCompactSupport_pairingTerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] (PU : SurfPoU X) (σ : Form01 X) (θ : Form1 X) (i : Fin PU.n) : HasCompactSupport (pairingTerm PU σ θ i)

theorem RS.Abel.integrable_pairingTerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] (PU : SurfPoU X) (σ : Form01 X) (θ : Form1 X) (i : Fin PU.n) : MeasureTheory.Integrable (pairingTerm PU σ θ i) MeasureTheory.volume

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

The Serre area pairing over the fixed partition datum PU: ∑ i, ∫ z, ψ_i(z) σ_i(z) ω_i(z) dA(z).

Equations

• RS.Abel.pairing PU σ θ = ∑ i : Fin PU.n, ∫ (z : ℂ), RS.Abel.pairingTerm PU σ θ i z

Bilinearity

theorem RS.Abel.pairingTerm_add_left {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (σ σ' : Form01 X) (θ : Form1 X) (i : Fin PU.n) : pairingTerm PU (σ + σ') θ i = fun (z : ℂ) => pairingTerm PU σ θ i z + pairingTerm PU σ' θ i z

theorem RS.Abel.pairingTerm_smul_left {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (c : ℂ) (σ : Form01 X) (θ : Form1 X) (i : Fin PU.n) : pairingTerm PU (c • σ) θ i = fun (z : ℂ) => c * pairingTerm PU σ θ i z

theorem RS.Abel.pairingTerm_add_right {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (σ : Form01 X) (θ θ' : Form1 X) (i : Fin PU.n) : pairingTerm PU σ (θ + θ') i = fun (z : ℂ) => pairingTerm PU σ θ i z + pairingTerm PU σ θ' i z

theorem RS.Abel.pairingTerm_smul_right {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (c : ℂ) (σ : Form01 X) (θ : Form1 X) (i : Fin PU.n) : pairingTerm PU σ (c • θ) i = fun (z : ℂ) => c * pairingTerm PU σ θ i z

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

theorem RS.Abel.pairing_smul_left {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (c : ℂ) (σ : Form01 X) (θ : Form1 X) : pairing PU (c • σ) θ = c * pairing PU σ θ

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

theorem RS.Abel.pairing_smul_right {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (c : ℂ) (σ : Form01 X) (θ : Form1 X) : pairing PU σ (c • θ) = c * pairing PU σ θ