The comparison H1Tail D ≃ₗ Cech.H1 D (laurent-tails, design §4.3/§5)

Unit: laurent-tails (docs/design/laurent-tails.md).

Status (honest, full account in the file-end note; this is a FINISHER-pass update — three of the unit's four original deferrals are now closed):

• tailToH1 : T D →ₗ[ℂ] Cech.H1 D — fully built (zero sorries), constructed from scratch via a per-point Mittag-Leffler class mlClassAt D p ψ : H1 D (a 2-member cover {V, X∖{p}} realizing ψ on a clean neighbourhood V), proved independent of every choice involved (mlClassAtOf_agree), then assembled via Submodule.liftQ/DFinsupp.lsum.
• tailToH1_alpha (tailToH1 D (alphaL D f) = 0) — CLOSED. The needed multi-point combination is built via mlSumCochain/alphaPatch/alphaAuxD (an (|S|+1)-member adapted cover realizing a global f's restriction at each of its finitely many "bad" points, 0 on background) plus a Finset.induction_on combination (CLAIM1 relates each point's mlClassAt to the big cover via a pairCover-to-𝒱 refinement, mlClass_add combines two at a time); the whole sum vanishes via mlClass_eq_zero_of_exists with the global witness f itself, using that off-diagonal cover overlaps never meet the marked-point Finset S (pure adaptedness).
• H1Tail.toH1 : H1Tail D →ₗ[ℂ] Cech.H1 D (Submodule.liftQ off tailToH1_alpha) and H1Tail.toH1_injective — CLOSED (both). Injectivity needed a second, independent multi-point construction (injG/injPatch/injD', this time realizing an arbitrary tail datum z : T D via chosen representatives ψ p rather than one global function — no global f is available a priori, that is exactly what injectivity produces), then Cech.mlClass_eq_zero_iff's ⇒ half (Forster 12.4, confirmed landed) extracts a global witness φ : LinSys D' realizing z pointwise, i.e. z = alpha D φ.
• H1Tail.equivOfSurjective — a genuine, honestly-parametrized (CONVENTIONS.md rule 3) conditional equivalence: Function.Surjective (tailToH1 D) → H1Tail D ≃ₗ[ℂ] Cech.H1 D, built from the now-unconditional H1Tail.toH1_injective. Surjectivity itself is NOT proved — see the file-end note for a full account of why (this is now a proven-hard fact, not a bookkeeping gap: it requires resolving an arbitrary Čech cohomology class into a sum of Mittag-Leffler local data, which after dolbeault-comparison's Leray theorem gives cocycle-on-a-good-cover representatives but does not by itself resolve the "collapse an arbitrary good-cover cocycle to marked-point-supported data" step — genuinely new complex analysis, comparable in depth to a Mittag-Leffler/Cousin-I existence theorem, well beyond a single finisher session; the file-end note records the full risk analysis for whoever picks this up next).

An important build-engineering lesson recorded here for future large proofs in this codebase (see the file-end note's "gotchas" section): composing an Opens X-level ≤ with a Set X-level ⊆ via bare .trans (relying on the automatic coercion) causes catastrophic isDefEq/whnf slowdowns (confirmed: a single lemma this way took >4,000,000 heartbeats and did not finish in 7+ minutes; converting the Opens-level term to an explicit Set-level inclusion first, then using plain Set.Subset.trans, fixed it in under 10 seconds). Likewise, a single tactic proof accumulating ~25 have/set steps hits a severe elaboration performance wall regardless of maxHeartbeats; factoring the construction into separate top-level def/theorem declarations (each against an explicit variable/include list) — mirroring how tailToH1_alpha's own helpers (alphaPatch/mlSumCochain/…) were already structured — restores normal compile times.

Small helper lemmas towards the construction

theorem RS.LaurentTail.exists_clean_nhds {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] {U : Set X} (hU : IsOpen U) (φ : MeroGermOn X U) {p : X} (hp : p ∈ U) : ∃ (V : TopologicalSpace.Opens X), p ∈ V ∧ ↑V ⊆ U ∧ ∀ x ∈ ↑V, x ≠ p → 0 ≤ φ.ord x

Isolated-singularity fact for a general (not necessarily connected/global) germ: away from p, φ is regular (order ≥ 0) on some open neighbourhood of p inside its domain.

theorem RS.LaurentTail.resC1_retype {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : Cech.FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : Cech.IsRefIdx 𝒰 𝒱 τ) (f : Cech.C1 D' 𝒰) (hf : f.MemLD D) (hf' : ((Cech.resC1 D' τ hτ) f).MemLD D) : (Cech.resC1 D τ hτ) (f.retype hf) = ((Cech.resC1 D' τ hτ) f).retype hf'

C1.retype commutes with restriction along a refinement index (both sides are literally the same restriction of the same underlying germ).

theorem RS.LaurentTail.mlClass_res {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} {𝒰 𝒱 : Cech.FinCover ⊤} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : Cech.IsRefIdx 𝒰 𝒱 τ) (g : Cech.C0 D' 𝒰) (hg : ((Cech.d0 D' 𝒰) g).MemLD D) (hg' : ((Cech.d0 D' 𝒱) ((Cech.resC0 D' τ hτ) g)).MemLD D) : Cech.mlClass 𝒰 g hg = Cech.mlClass 𝒱 ((Cech.resC0 D' τ hτ) g) hg'

mlClass is compatible with refining the underlying cover: pulling the realizing 0-cochain back along a refinement index gives the same class in H1 D.

The per-point construction: realizing a clean representative

@[reducible]

noncomputable def RS.LaurentTail.pairCover {X : Type u_1} [TopologicalSpace X] [T1Space X] [DecidableEq X] (p : X) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) : Cech.FinCover ⊤

The 2-member cover {V, X ∖ {p}}, used to realize a single tail datum at p.

Equations

• RS.LaurentTail.pairCover p V hpV = { n := 2, U := ![V, { carrier := {p}ᶜ, is_open' := ⋯ }], le_base := ⋯, covers := ⋯ }

theorem RS.LaurentTail.pairCover_U_zero {X : Type u_1} [TopologicalSpace X] [T1Space X] [DecidableEq X] (p : X) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) : (pairCover p V hpV).U 0 = V

theorem RS.LaurentTail.pairCover_U_one {X : Type u_1} [TopologicalSpace X] [T1Space X] [DecidableEq X] (p : X) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) : (pairCover p V hpV).U 1 = { carrier := {p}ᶜ, is_open' := ⋯ }

noncomputable def RS.LaurentTail.gOf {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] (p : X) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) (D' : Divisor X) (ψV : ↥(LinSysOn D' ↑V)) : Cech.C0 D' (pairCover p V hpV)

The 0-cochain realizing ψV on V, 0 on the background X ∖ {p}.

Equations

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

noncomputable def RS.LaurentTail.bumpDivisor {X : Type u_1} [TopologicalSpace X] [DecidableEq X] (p : X) (n : ℤ) : Divisor X

The bump divisor supported only at p, covering -(ψ.ord p) there.

Equations

• RS.LaurentTail.bumpDivisor p n = Function.locallyFinsuppWithin.single p n

@[simp]

theorem RS.LaurentTail.bumpDivisor_apply_self {X : Type u_1} [TopologicalSpace X] [DecidableEq X] (p : X) (n : ℤ) : (bumpDivisor p n) p = n

theorem RS.LaurentTail.bumpDivisor_apply_of_ne {X : Type u_1} [TopologicalSpace X] [DecidableEq X] {p x : X} (hx : x ≠ p) (n : ℤ) : (bumpDivisor p n) x = 0

theorem RS.LaurentTail.d0_pairCover_diag {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] {D' : Divisor X} (p : X) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) (g : Cech.C0 D' (pairCover p V hpV)) (i : Fin 2) : (Cech.d0 D' (pairCover p V hpV)) g (i, i) = 0

mlClass invariance under raising the auxiliary divisor D' (from

`scratch_ltails2.lean`) 

theorem RS.LaurentTail.d0_inclC0_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} {𝒰 : Cech.FinCover Ω} {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) (g : Cech.C0 D₁ 𝒰) (p : Fin 𝒰.n × Fin 𝒰.n) : ↑((Cech.d0 D₂ 𝒰) ((Cech.inclC0 D₁ 𝒰 h) g) p) = ↑((Cech.d0 D₁ 𝒰) g p)

theorem RS.LaurentTail.memLD_inclC0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} {𝒰 : Cech.FinCover Ω} {D₁ D₂ D : Divisor X} (h : D₁ ≤ D₂) {g : Cech.C0 D₁ 𝒰} (hg : ((Cech.d0 D₁ 𝒰) g).MemLD D) : ((Cech.d0 D₂ 𝒰) ((Cech.inclC0 D₁ 𝒰 h) g)).MemLD D

theorem RS.LaurentTail.mlClass_inclC0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 : Cech.FinCover ⊤} {D₁ D₂ D : Divisor X} (h : D₁ ≤ D₂) {g : Cech.C0 D₁ 𝒰} (hg : ((Cech.d0 D₁ 𝒰) g).MemLD D) : Cech.mlClass 𝒰 ((Cech.inclC0 D₁ 𝒰 h) g) ⋯ = Cech.mlClass 𝒰 g hg

gOf algebra

theorem RS.LaurentTail.gOf_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] (p : X) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) (D' : Divisor X) (ψV ψV' : ↥(LinSysOn D' ↑V)) : gOf p V hpV D' (ψV + ψV') = gOf p V hpV D' ψV + gOf p V hpV D' ψV'

theorem RS.LaurentTail.gOf_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] (c : ℂ) (p : X) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) (D' : Divisor X) (ψV : ↥(LinSysOn D' ↑V)) : gOf p V hpV D' (c • ψV) = c • gOf p V hpV D' ψV

theorem RS.LaurentTail.gOf_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] (p : X) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) (D' : Divisor X) : gOf p V hpV D' 0 = 0

A clean neighborhood also avoiding D's other poles

noncomputable def RS.LaurentTail.cleanNbhd {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : TopologicalSpace.Opens X

A chart neighbourhood of p clean for ψ: small enough that ψ is the only departure from D on it.

Equations

• RS.LaurentTail.cleanNbhd D p ψ = ⋯.choose ⊓ RS.Cech.compOpens (⋯.toFinset.erase p)

theorem RS.LaurentTail.mem_cleanNbhd {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : p ∈ cleanNbhd D p ψ

theorem RS.LaurentTail.cleanNbhd_sub_source {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : ↑(cleanNbhd D p ψ) ⊆ (chartAt ℂ p).source

theorem RS.LaurentTail.cleanNbhd_ord_nonneg {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) (x : X) : x ∈ ↑(cleanNbhd D p ψ) → x ≠ p → 0 ≤ ψ.ord x

theorem RS.LaurentTail.cleanNbhd_D_eq_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) (x : X) : x ∈ ↑(cleanNbhd D p ψ) → x ≠ p → D x = 0

The auxiliary divisor D' bumped at p

noncomputable def RS.LaurentTail.nOf {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : ℤ

The order of the pole that ψ contributes at p.

Equations

• RS.LaurentTail.nOf D p ψ = max (D p) (-(ψ.ord p).untop₀)

theorem RS.LaurentTail.D_p_le_nOf {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : D p ≤ nOf D p ψ

theorem RS.LaurentTail.neg_nOf_le_ord {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : ↑(-nOf D p ψ) ≤ ψ.ord p

noncomputable def RS.LaurentTail.DPrimeOf {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : Divisor X

The auxiliary divisor admitting ψ at p on top of D.

Equations

• RS.LaurentTail.DPrimeOf D p ψ = D + RS.LaurentTail.bumpDivisor p (RS.LaurentTail.nOf D p ψ - D p)

theorem RS.LaurentTail.DPrimeOf_apply_self {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : (DPrimeOf D p ψ) p = nOf D p ψ

theorem RS.LaurentTail.DPrimeOf_apply_of_ne {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) {x : X} (hx : x ≠ p) : (DPrimeOf D p ψ) x = D x

theorem RS.LaurentTail.D_le_DPrimeOf {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : D ≤ DPrimeOf D p ψ

The membership witness for gOf's V-component

theorem RS.LaurentTail.restrict_ψ_mem_linSysOn {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : (MeroGermOn.restrict ⋯) ψ ∈ LinSysOn (DPrimeOf D p ψ) ↑(cleanNbhd D p ψ)

theorem RS.LaurentTail.gOf_apply_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] (p : X) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) (D' : Divisor X) (ψV : ↥(LinSysOn D' ↑V)) : gOf p V hpV D' ψV 0 = ψV

theorem RS.LaurentTail.gOf_apply_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] (p : X) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) (D' : Divisor X) (ψV : ↥(LinSysOn D' ↑V)) : gOf p V hpV D' ψV 1 = 0

noncomputable def RS.LaurentTail.ψVOf {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : ↥(LinSysOn (DPrimeOf D p ψ) ↑(cleanNbhd D p ψ))

ψ restricted to its clean neighbourhood, as a section of the auxiliary linear system.

Equations

• RS.LaurentTail.ψVOf D p ψ = ⟨(RS.MeroGermOn.restrict ⋯) ψ, ⋯⟩

theorem RS.LaurentTail.gOf_memLD_of_clean {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] (p : X) (D D' : Divisor X) (ψ : MeroGermOn X (chartAt ℂ p).source) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) (hVsub : ↑V ⊆ (chartAt ℂ p).source) (hVclean : ∀ x ∈ ↑V, x ≠ p → 0 ≤ ψ.ord x) (hVDzero : ∀ x ∈ ↑V, x ≠ p → D x = 0) (ψV : ↥(LinSysOn D' ↑V)) (hψV : ↑ψV = (MeroGermOn.restrict hVsub) ψ) : ((Cech.d0 D' (pairCover p V hpV)) (gOf p V hpV D' ψV)).MemLD D

Generic version: gOf's coboundary is D-bounded whenever V is clean for ψ away from p and avoids D's other poles, and D' agrees with D away from p. Stated with fully abstract V/ψV/D' (no unfolding of cleanNbhd/ψVOf/DPrimeOf needed inside the proof).

gOf commutes with inclC0 and with refinement (resC0)

theorem RS.LaurentTail.gOf_inclC0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] (p : X) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) {D'₁ D'₂ : Divisor X} (h : D'₁ ≤ D'₂) (ψV : ↥(LinSysOn D'₁ ↑V)) : (Cech.inclC0 D'₁ (pairCover p V hpV) h) (gOf p V hpV D'₁ ψV) = gOf p V hpV D'₂ ((Submodule.inclusion ⋯) ψV)

theorem RS.LaurentTail.pairCover_isRefIdx {X : Type u_1} [TopologicalSpace X] [T1Space X] [DecidableEq X] (p : X) (V W : TopologicalSpace.Opens X) (hpV : p ∈ V) (hpW : p ∈ W) (hWV : W ≤ V) : Cech.IsRefIdx (pairCover p V hpV) (pairCover p W hpW) id

theorem RS.LaurentTail.gOf_resC0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] (p : X) (V W : TopologicalSpace.Opens X) (hpV : p ∈ V) (hpW : p ∈ W) (hWV : W ≤ V) (D' : Divisor X) (ψV : ↥(LinSysOn D' ↑V)) : (Cech.resC0 D' id ⋯) (gOf p V hpV D' ψV) = gOf p W hpW D' ((Cech.LinSysOn.restrictL D' hWV) ψV)

theorem RS.LaurentTail.mlClass_congr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 : Cech.FinCover ⊤} {D D' : Divisor X} {g g' : Cech.C0 D' 𝒰} (heq : g = g') {hg : ((Cech.d0 D' 𝒰) g).MemLD D} : Cech.mlClass 𝒰 g hg = Cech.mlClass 𝒰 g' ⋯

Transport mlClass along an equality of the underlying 0-cochain (avoids the "motive is not type correct" failure of rw on mlClass's dependent hg argument).

The single-point Mittag-Leffler class, and its independence of choices

noncomputable def RS.LaurentTail.mlClassAtOf {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] (p : X) (D D' : Divisor X) (ψ : MeroGermOn X (chartAt ℂ p).source) (V : TopologicalSpace.Opens X) (hpV : p ∈ V) (hVsub : ↑V ⊆ (chartAt ℂ p).source) (hVclean : ∀ x ∈ ↑V, x ≠ p → 0 ≤ ψ.ord x) (hVDzero : ∀ x ∈ ↑V, x ≠ p → D x = 0) (ψV : ↥(LinSysOn D' ↑V)) (hψV : ↑ψV = (MeroGermOn.restrict hVsub) ψ) : Cech.H1 D

The Mittag-Leffler class of ψ at p, computed through a chosen clean neighbourhood V.

Equations

• RS.LaurentTail.mlClassAtOf p D D' ψ V hpV hVsub hVclean hVDzero ψV hψV = RS.Cech.mlClass (RS.LaurentTail.pairCover p V hpV) (RS.LaurentTail.gOf p V hpV D' ψV) ⋯

theorem RS.LaurentTail.mlClassAtOf_raise_res {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] (p : X) (D D' D'' : Divisor X) (ψ : MeroGermOn X (chartAt ℂ p).source) (V W : TopologicalSpace.Opens X) (hpV : p ∈ V) (hpW : p ∈ W) (hWV : W ≤ V) (hVsub : ↑V ⊆ (chartAt ℂ p).source) (hVclean : ∀ x ∈ ↑V, x ≠ p → 0 ≤ ψ.ord x) (hVDzero : ∀ x ∈ ↑V, x ≠ p → D x = 0) (hWsub : ↑W ⊆ (chartAt ℂ p).source) (hWclean : ∀ x ∈ ↑W, x ≠ p → 0 ≤ ψ.ord x) (hWDzero : ∀ x ∈ ↑W, x ≠ p → D x = 0) (h : D' ≤ D'') (ψV : ↥(LinSysOn D' ↑V)) (hψV : ↑ψV = (MeroGermOn.restrict hVsub) ψ) (ψW : ↥(LinSysOn D'' ↑W)) (hψW : ↑ψW = (MeroGermOn.restrict hWsub) ψ) : mlClassAtOf p D D' ψ V hpV hVsub hVclean hVDzero ψV hψV = mlClassAtOf p D D'' ψ W hpW hWsub hWclean hWDzero ψW hψW

Raise-then-refine identity: mlClassAtOf computed via (D',V) equals the one computed via (D'', W) for W ≤ V and D' ≤ D'', provided the D''-typed representative on W is again restrict ψ.

theorem RS.LaurentTail.mlClassAtOf_agree {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [DecidableEq X] (p : X) (D : Divisor X) (ψ : MeroGermOn X (chartAt ℂ p).source) {D'₁ D'₂ : Divisor X} {V₁ V₂ : TopologicalSpace.Opens X} (hpV₁ : p ∈ V₁) (hpV₂ : p ∈ V₂) (hV₁sub : ↑V₁ ⊆ (chartAt ℂ p).source) (hV₁clean : ∀ x ∈ ↑V₁, x ≠ p → 0 ≤ ψ.ord x) (hV₁Dzero : ∀ x ∈ ↑V₁, x ≠ p → D x = 0) (hV₂sub : ↑V₂ ⊆ (chartAt ℂ p).source) (hV₂clean : ∀ x ∈ ↑V₂, x ≠ p → 0 ≤ ψ.ord x) (hV₂Dzero : ∀ x ∈ ↑V₂, x ≠ p → D x = 0) (ψV₁ : ↥(LinSysOn D'₁ ↑V₁)) (hψV₁ : ↑ψV₁ = (MeroGermOn.restrict hV₁sub) ψ) (ψV₂ : ↥(LinSysOn D'₂ ↑V₂)) (hψV₂ : ↑ψV₂ = (MeroGermOn.restrict hV₂sub) ψ) : mlClassAtOf p D D'₁ ψ V₁ hpV₁ hV₁sub hV₁clean hV₁Dzero ψV₁ hψV₁ = mlClassAtOf p D D'₂ ψ V₂ hpV₂ hV₂sub hV₂clean hV₂Dzero ψV₂ hψV₂

Independence of choices. mlClassAtOf's value does not depend on which valid (V, D', ψV) data is used to represent the same ambient germ ψ.

mlClassAt (the canonical single-point construction)

noncomputable def RS.LaurentTail.mlClassAt {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : Cech.H1 D

The Mittag-Leffler class in H¹(D) of a germ ψ at the point p.

Equations

• RS.LaurentTail.mlClassAt D p ψ = RS.LaurentTail.mlClassAtOf p D (RS.LaurentTail.DPrimeOf D p ψ) ψ (RS.LaurentTail.cleanNbhd D p ψ) ⋯ ⋯ ⋯ ⋯ (RS.LaurentTail.ψVOf D p ψ) ⋯

theorem RS.LaurentTail.mlClassAt_eq_of_valid {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) {D' : Divisor X} {V : TopologicalSpace.Opens X} (hpV : p ∈ V) (hVsub : ↑V ⊆ (chartAt ℂ p).source) (hVclean : ∀ x ∈ ↑V, x ≠ p → 0 ≤ ψ.ord x) (hVDzero : ∀ x ∈ ↑V, x ≠ p → D x = 0) (ψV : ↥(LinSysOn D' ↑V)) (hψV : ↑ψV = (MeroGermOn.restrict hVsub) ψ) : mlClassAt D p ψ = mlClassAtOf p D D' ψ V hpV hVsub hVclean hVDzero ψV hψV

theorem RS.LaurentTail.mlClassAt_eq_zero_of_mem_ordGe {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) (hp : -↑(D p) ≤ ψ.ord p) : mlClassAt D p ψ = 0

mlClassAt is additive and ℂ-linear

theorem RS.LaurentTail.mlClassAt_add {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ ψ' : MeroGermOn X (chartAt ℂ p).source) : mlClassAt D p (ψ + ψ') = mlClassAt D p ψ + mlClassAt D p ψ'

theorem RS.LaurentTail.mlClassAt_smul {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (c : ℂ) (ψ : MeroGermOn X (chartAt ℂ p).source) : mlClassAt D p (c • ψ) = c • mlClassAt D p ψ

The ambient linear map, and its descent to TailAt p D / T D

@[instance_reducible]

noncomputable instance RS.LaurentTail.instAddCommGroupH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : AddCommGroup (Cech.H1 D)

AddCommGroup (H1 D), registered globally: Module.DirectLimit.addCommGroup is stated with G/f as leading explicit arguments (not instance-implicit), so plain inferInstance/typeclass search for AddCommGroup (H1 D) does not find it automatically through the H1 abbrev — needed explicitly here so Submodule.liftQ's own instance search (for its codomain) succeeds.

Equations

• RS.LaurentTail.instAddCommGroupH1 D = Module.DirectLimit.addCommGroup (fun (𝒰 : RS.Cech.FinCover ⊤) => RS.Cech.H1Cover D 𝒰) fun (x x_1 : RS.Cech.FinCover ⊤) (h : x ≤ x_1) => RS.Cech.resH1' D h

noncomputable def RS.LaurentTail.mlClassAtRaw {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) : MeroGermOn X (chartAt ℂ p).source →ₗ[ℂ] Cech.H1 D

mlClassAt packaged as a linear map on germs at p.

Equations

• RS.LaurentTail.mlClassAtRaw D p = { toFun := RS.LaurentTail.mlClassAt D p, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.LaurentTail.mlClassAtRaw_apply {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : (mlClassAtRaw D p) ψ = mlClassAt D p ψ

noncomputable def RS.LaurentTail.tailAtToH1 {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) : TailAt p D →ₗ[ℂ] Cech.H1 D

The tail-to-cohomology map at a single point.

Equations

• RS.LaurentTail.tailAtToH1 D p = (RS.Cech.ordGe p (-D p)).liftQ (RS.LaurentTail.mlClassAtRaw D p) ⋯

theorem RS.LaurentTail.tailAtToH1_mk {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : (tailAtToH1 D p) ((TailAt.mk p D) ψ) = mlClassAt D p ψ

noncomputable def RS.LaurentTail.tailToH1 {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : T D →ₗ[ℂ] Cech.H1 D

The tail-to-cohomology map on the whole tail space T D.

Equations

• RS.LaurentTail.tailToH1 D = (DFinsupp.lsum ℕ) fun (p : X) => RS.LaurentTail.tailAtToH1 D p

theorem RS.LaurentTail.tailToH1_apply_single {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (p : X) (τ : TailAt p D) : (tailToH1 D) (DFinsupp.single p τ) = (tailAtToH1 D p) τ

General helpers

theorem RS.LaurentTail.d0_diag_eq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} {𝒰 : Cech.FinCover Ω} {D' : Divisor X} (g : Cech.C0 D' 𝒰) (i : Fin 𝒰.n) : (Cech.d0 D' 𝒰) g (i, i) = 0

theorem RS.LaurentTail.mlClass_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 : Cech.FinCover ⊤} {D D' : Divisor X} (hg : ((Cech.d0 D' 𝒰) 0).MemLD D) : Cech.mlClass 𝒰 0 hg = 0

theorem RS.LaurentTail.restrict_mem_linSysOn_of_mem_linSys {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D' : Divisor X} {f : Mero X} (hf : f ∈ LinSys D') (V : Set X) (hV : IsOpen V) : (MeroGermOn.restrict ⋯) f ∈ LinSysOn D' V

noncomputable def RS.LaurentTail.alphaAuxD {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] (D : Divisor X) (f : Mero X) : Divisor X

The auxiliary divisor D ⊔ (-div f), which admits f.

Equations

• RS.LaurentTail.alphaAuxD D f = D ⊔ -RS.divisor f

theorem RS.LaurentTail.mem_linSys_alphaAuxD {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] [T1Space X] (D : Divisor X) {f : Mero X} (hf : f ≠ 0) : f ∈ LinSys (alphaAuxD D f)

The clean patch at a marked point, avoiding the other marked points

noncomputable def RS.LaurentTail.alphaPatch {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) (S : Finset X) (p : X) : TopologicalSpace.Opens X

A neighbourhood of p clean for f and meeting no other marked point of S.

Equations

• RS.LaurentTail.alphaPatch D f S p = RS.LaurentTail.cleanNbhd D p ((RS.MeroGermOn.restrict ⋯) f) ⊓ RS.Cech.compOpens (S.erase p)

theorem RS.LaurentTail.mem_alphaPatch {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) (S : Finset X) (p : X) : p ∈ alphaPatch D f S p

theorem RS.LaurentTail.alphaPatch_sub_source {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) (S : Finset X) (p : X) : ↑(alphaPatch D f S p) ⊆ (chartAt ℂ p).source

theorem RS.LaurentTail.alphaPatch_clean {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) (S : Finset X) (p x : X) : x ∈ ↑(alphaPatch D f S p) → x ≠ p → 0 ≤ ((MeroGermOn.restrict ⋯) f).ord x

theorem RS.LaurentTail.alphaPatch_D_eq_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) (S : Finset X) (p x : X) : x ∈ ↑(alphaPatch D f S p) → x ≠ p → D x = 0

theorem RS.LaurentTail.alphaPatch_excl {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) (S : Finset X) (p x : X) : x ∈ ↑(alphaPatch D f S p) → x ∉ S.erase p

The Finset-indexed Mittag-Leffler cochain

noncomputable def RS.LaurentTail.mlSumCochain {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒱 : Cech.FinCover ⊤} (D' : Divisor X) (f : Mero X) (hf : f ∈ LinSys D') (T : Finset X) : Cech.C0 D' 𝒱

The 0-cochain assembling f's local data over the marked points of T.

Equations

• RS.LaurentTail.mlSumCochain D' f hf T k = if _h : ∃ p ∈ T, p ∈ 𝒱.U k then ⟨(RS.MeroGermOn.restrict ⋯) f, ⋯⟩ else 0

theorem RS.LaurentTail.mlSumCochain_apply_of_mem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒱 : Cech.FinCover ⊤} (D' : Divisor X) (f : Mero X) (hf : f ∈ LinSys D') (T : Finset X) (k : Fin 𝒱.n) {p : X} (hpT : p ∈ T) (hpk : p ∈ 𝒱.U k) : mlSumCochain D' f hf T k = ⟨(MeroGermOn.restrict ⋯) f, ⋯⟩

theorem RS.LaurentTail.mlSumCochain_apply_of_not_mem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒱 : Cech.FinCover ⊤} (D' : Divisor X) (f : Mero X) (hf : f ∈ LinSys D') (T : Finset X) (k : Fin 𝒱.n) (hnot : ∀ p ∈ T, p ∉ 𝒱.U k) : mlSumCochain D' f hf T k = 0

theorem RS.LaurentTail.mlSumCochain_empty {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒱 : Cech.FinCover ⊤} (D' : Divisor X) (f : Mero X) (hf : f ∈ LinSys D') : mlSumCochain D' f hf ∅ = 0

Pieces of tailToH1_alpha

The theorem is assembled from these lemmas rather than written as one proof: as a single declaration it exceeded both the default heartbeat budget and the 200-line size we hold ourselves to. alphaFinset D f / alphaAuxD D f are spelled out rather than generalized over, because the proofs below use that definitional identity.

The main theorem

theorem RS.LaurentTail.tailToH1_alpha {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) : (tailToH1 D) ((alphaL D) f) = 0

H1Tail.toH1

noncomputable def RS.LaurentTail.H1Tail.toH1 {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : H1Tail D →ₗ[ℂ] Cech.H1 D

The induced map from the tail quotient to H¹(D).

Equations

• RS.LaurentTail.H1Tail.toH1 D = (RS.LaurentTail.alphaL D).range.liftQ (RS.LaurentTail.tailToH1 D) ⋯

theorem RS.LaurentTail.H1Tail.toH1_mk {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (z : T D) : (toH1 D) ((mk D) z) = (tailToH1 D) z

Injectivity: helper constructions, factored to top-level declarations for elaboration

speed (a single giant tactic proof accumulating ~25 haves/sets hits a severe performance wall: confirmed by direct experiment, set_option maxHeartbeats 20000000 still did not finish in 10 minutes of wall-clock time). Each piece below is proved against only the section variables it actually needs, mirroring tailToH1_alpha's own successful top-level-helper structure.

noncomputable def RS.LaurentTail.injPatch {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D : Divisor X) (p : X) : TopologicalSpace.Opens X

The clean patch at a marked point p, avoiding the other points of S (generalizes alphaPatch to an arbitrary per-point representative ψ, not tied to one global function).

Equations

• RS.LaurentTail.injPatch ψ S D p = RS.LaurentTail.cleanNbhd D p (ψ p) ⊓ RS.Cech.compOpens (S.erase p)

theorem RS.LaurentTail.mem_injPatch {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D : Divisor X) (p : X) : p ∈ injPatch ψ S D p

theorem RS.LaurentTail.injPatch_sub {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D : Divisor X) (p : X) : ↑(injPatch ψ S D p) ⊆ (chartAt ℂ p).source

theorem RS.LaurentTail.injPatch_excl {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D : Divisor X) (p x : X) : x ∈ ↑(injPatch ψ S D p) → x ∉ S.erase p

noncomputable def RS.LaurentTail.injD' {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D : Divisor X) (hSne : S.Nonempty) : Divisor X

A single auxiliary divisor dominating DPrimeOf at every point of S.

Equations

• RS.LaurentTail.injD' ψ S D hSne = S.sup' hSne fun (p : X) => RS.LaurentTail.DPrimeOf D p (ψ p)

theorem RS.LaurentTail.injD'_mem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D : Divisor X) (hSne : S.Nonempty) (p : X) : p ∈ S → DPrimeOf D p (ψ p) ≤ injD' ψ S D hSne

theorem RS.LaurentTail.injD'_ge {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D : Divisor X) (hSne : S.Nonempty) : D ≤ injD' ψ S D hSne

noncomputable def RS.LaurentTail.injψVD' {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D D' : Divisor X) (hD'mem : ∀ p ∈ S, DPrimeOf D p (ψ p) ≤ D') (p : X) (hp : p ∈ S) : ↥(LinSysOn D' ↑(injPatch ψ S D p))

The D'-typed representative at each marked point, restricted to its own patch.

Equations

• RS.LaurentTail.injψVD' ψ S D D' hD'mem p hp = (RS.Cech.LinSysOn.restrictL D' ⋯) ((Submodule.inclusion ⋯) (RS.LaurentTail.ψVOf D p (ψ p)))

theorem RS.LaurentTail.injψVD'_eq {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D D' : Divisor X) (hD'mem : ∀ p ∈ S, DPrimeOf D p (ψ p) ≤ D') (p : X) (hp : p ∈ S) : ↑(injψVD' ψ S D D' hD'mem p hp) = (MeroGermOn.restrict ⋯) (ψ p)

theorem RS.LaurentTail.inj_hoffdiag {X : Type u_1} [TopologicalSpace X] (S : Finset X) {𝒱 : Cech.FinCover ⊤} (h𝒱Adapted : 𝒱.IsAdapted S) (k l : Fin 𝒱.n) : k ≠ l → ∀ x ∈ 𝒱.U k ⊓ 𝒱.U l, x ∉ S

theorem RS.LaurentTail.inj_hexcl {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D : Divisor X) {𝒱 : Cech.FinCover ⊤} (hOclause : ∀ p ∈ S, ∀ (k : Fin 𝒱.n), p ∈ 𝒱.U k → 𝒱.U k ≤ injPatch ψ S D p) (q : X) : q ∈ S → ∀ (k : Fin 𝒱.n), q ∈ 𝒱.U k → ∀ p ∈ S, p ≠ q → p ∉ 𝒱.U k

theorem RS.LaurentTail.inj_hunique_S {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D : Divisor X) {𝒱 : Cech.FinCover ⊤} (hOclause : ∀ p ∈ S, ∀ (k : Fin 𝒱.n), p ∈ 𝒱.U k → 𝒱.U k ≤ injPatch ψ S D p) (p : X) : p ∈ S → ∀ q ∈ S, ∀ (k : Fin 𝒱.n), p ∈ 𝒱.U k → q ∈ 𝒱.U k → p = q

noncomputable def RS.LaurentTail.injG {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D D' : Divisor X) (hD'mem : ∀ p ∈ S, DPrimeOf D p (ψ p) ≤ D') {𝒱 : Cech.FinCover ⊤} (hOclause : ∀ p ∈ S, ∀ (k : Fin 𝒱.n), p ∈ 𝒱.U k → 𝒱.U k ≤ injPatch ψ S D p) (T : Finset X) : Cech.C0 D' 𝒱

The multi-point cochain, restricted to the marked points of T (intersected with S).

Equations

• RS.LaurentTail.injG ψ S D D' hD'mem hOclause T k = if h : ∃ p ∈ T ∩ S, p ∈ 𝒱.U k then (RS.Cech.LinSysOn.restrictL D' ⋯) (RS.LaurentTail.injψVD' ψ S D D' hD'mem h.choose ⋯) else 0

theorem RS.LaurentTail.injG_apply_of_mem {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D D' : Divisor X) (hD'mem : ∀ p ∈ S, DPrimeOf D p (ψ p) ≤ D') {𝒱 : Cech.FinCover ⊤} (hOclause : ∀ p ∈ S, ∀ (k : Fin 𝒱.n), p ∈ 𝒱.U k → 𝒱.U k ≤ injPatch ψ S D p) (T : Finset X) (k : Fin 𝒱.n) (p : X) (hpT : p ∈ T) (hpS : p ∈ S) (hpk : p ∈ 𝒱.U k) : injG ψ S D D' hD'mem hOclause T k = (Cech.LinSysOn.restrictL D' ⋯) (injψVD' ψ S D D' hD'mem p hpS)

theorem RS.LaurentTail.injG_apply_of_not_mem {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D D' : Divisor X) (hD'mem : ∀ p ∈ S, DPrimeOf D p (ψ p) ≤ D') {𝒱 : Cech.FinCover ⊤} (hOclause : ∀ p ∈ S, ∀ (k : Fin 𝒱.n), p ∈ 𝒱.U k → 𝒱.U k ≤ injPatch ψ S D p) (T : Finset X) (k : Fin 𝒱.n) (hnot : ∀ p ∈ T, p ∈ S → p ∉ 𝒱.U k) : injG ψ S D D' hD'mem hOclause T k = 0

theorem RS.LaurentTail.inj_hmember_ord {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D D' : Divisor X) (hD'mem : ∀ p ∈ S, DPrimeOf D p (ψ p) ≤ D') {𝒱 : Cech.FinCover ⊤} (hOclause : ∀ p ∈ S, ∀ (k : Fin 𝒱.n), p ∈ 𝒱.U k → 𝒱.U k ≤ injPatch ψ S D p) (T : Finset X) (k : Fin 𝒱.n) (x : X) (hx : x ∈ ↑(𝒱.U k)) (hxS : x ∉ S) : ↑(-D x) ≤ (↑(injG ψ S D D' hD'mem hOclause T k)).ord x

theorem RS.LaurentTail.inj_hg_MemLD {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D D' : Divisor X) (hD'mem : ∀ p ∈ S, DPrimeOf D p (ψ p) ≤ D') {𝒱 : Cech.FinCover ⊤} (h𝒱Adapted : 𝒱.IsAdapted S) (hOclause : ∀ p ∈ S, ∀ (k : Fin 𝒱.n), p ∈ 𝒱.U k → 𝒱.U k ≤ injPatch ψ S D p) (T : Finset X) : ((Cech.d0 D' 𝒱) (injG ψ S D D' hD'mem hOclause T)).MemLD D

theorem RS.LaurentTail.inj_CLAIM1 {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D D' : Divisor X) (hD'mem : ∀ p ∈ S, DPrimeOf D p (ψ p) ≤ D') {𝒱 : Cech.FinCover ⊤} (h𝒱Adapted : 𝒱.IsAdapted S) (hOclause : ∀ p ∈ S, ∀ (k : Fin 𝒱.n), p ∈ 𝒱.U k → 𝒱.U k ≤ injPatch ψ S D p) (p : X) (hp : p ∈ S) : mlClassAt D p (ψ p) = Cech.mlClass 𝒱 (injG ψ S D D' hD'mem hOclause {p}) ⋯

CLAIM1-analogue: a single marked point's mlClassAt equals the big cover's mlClass of the one-point cochain injG {p}.

theorem RS.LaurentTail.inj_main {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D D' : Divisor X) (hD'mem : ∀ p ∈ S, DPrimeOf D p (ψ p) ≤ D') {𝒱 : Cech.FinCover ⊤} (h𝒱Adapted : 𝒱.IsAdapted S) (hOclause : ∀ p ∈ S, ∀ (k : Fin 𝒱.n), p ∈ 𝒱.U k → 𝒱.U k ≤ injPatch ψ S D p) (T : Finset X) : T ⊆ S → ∑ q ∈ T, mlClassAt D q (ψ q) = Cech.mlClass 𝒱 (injG ψ S D D' hD'mem hOclause T) ⋯

The multi-point induction: sum of individual mlClassAts over any T ⊆ S equals the big cover's mlClass of injG T.

theorem RS.LaurentTail.inj_hcoe {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [T1Space X] [DecidableEq X] (ψ : (p : X) → MeroGermOn X (chartAt ℂ p).source) (S : Finset X) (D D' : Divisor X) (hD'mem : ∀ p ∈ S, DPrimeOf D p (ψ p) ≤ D') {𝒱 : Cech.FinCover ⊤} (hOclause : ∀ p ∈ S, ∀ (k : Fin 𝒱.n), p ∈ 𝒱.U k → 𝒱.U k ≤ injPatch ψ S D p) (φ : ↥(LinSys D')) (q : X) (hq : q ∈ S) (k : Fin 𝒱.n) (hqk : q ∈ 𝒱.U k) (x : X) (hx : x ∈ ↑(𝒱.U k)) : (↑((Cech.LinSysOn.restrictL D' ⋯) (injψVD' ψ S D D' hD'mem q hq)) - (MeroGermOn.restrict ⋯) ↑φ).ord x = (ψ q - (MeroGermOn.restrict ⋯) ↑φ).ord x

The coboundary/order identity used to read φ's bound back into ψ q's tail data.

theorem RS.LaurentTail.H1Tail.toH1_injective {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : Function.Injective ⇑(toH1 D)

H1Tail.equiv, conditional on surjectivity (§8 R1's own fallback: an honest

explicit-hypothesis statement, not a vacuous one, per CONVENTIONS.md rule 3)

theorem RS.LaurentTail.H1Tail.toH1_surjective_of_tailToH1_surjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (hsurj : Function.Surjective ⇑(tailToH1 D)) : Function.Surjective ⇑(toH1 D)

noncomputable def RS.LaurentTail.H1Tail.equivOfSurjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (hsurj : Function.Surjective ⇑(tailToH1 D)) : H1Tail D ≃ₗ[ℂ] Cech.H1 D

CC8's mandate, conditional on tailToH1's surjectivity (item 3 of the four deferrals, gated on dolbeault-comparison's Leray/Mittag-Leffler-existence machinery — see this file's file-end note for the exact obstruction). Injectivity (H1Tail.toH1_injective) is unconditional and fully proved above; this is the one remaining hypothesis.

Equations

• RS.LaurentTail.H1Tail.equivOfSurjective D hsurj = LinearEquiv.ofBijective (RS.LaurentTail.H1Tail.toH1 D) ⋯

File-end note (FINISHER pass): what closed, what's built, what's still deferred, and why

Closed this pass (three of the unit's four original deferrals):

1. tailToH1_alpha (tailToH1 D (alphaL D f) = 0). Built via a from-scratch multi-point Mittag-Leffler combination, specialized to the case where every local datum comes from restricting one global f : ℳ X (which is exactly alpha D f's shape):
   • alphaAuxD D f := D ⊔ (-(divisor f)) (a single auxiliary divisor bounding both D and f itself globally, f ≠ 0 case; f = 0 is handled first, trivially, via map_zero).
   • alphaPatch D f S p := cleanNbhd D p (restrict f) ⊓ compOpens (S.erase p) (S := alphaFinset D f): the per-point clean patch, now also excluding every other point of S.
   • An adapted cover 𝒱 for S via Cech.exists_adapted_refinement with O := alphaPatch D f S (reused verbatim from the concurrent SixTerm.lean builder's own "prescribed neighbourhood" idiom, per the interface note the earlier build recorded).
   • mlSumCochain D' f hf T: the cochain that is restrict f on T ∩ S's marked members, 0 elsewhere (a dite on ∃ p ∈ T ∩ S, p ∈ 𝒱.U k, well-defined regardless of which witness p is chosen because hunique_S/hexcl — themselves consequences of adaptedness and the compOpens (S.erase p) exclusion, not of adaptedness alone: a genuine subtlety — two different marked points sharing one cover member is not excluded by FinCover.IsAdapted's bare definition, only by this file's own choice of O shrinking each patch away from the rest of S).
   • Off-diagonal cover overlaps never meet S (hoffdiag, pure consequence of the ∃! in IsAdapted, no O-shrinking needed): this is what makes mlSumCochain's coboundary D-bounded everywhere (hg_MemLD) — diagonal is 0 trivially, off-diagonal points are automatically outside S, where f is regular and D = 0 (not_mem_alphaFinset).
   • CLAIM1: each point's own mlClassAt D p (restrict f) equals mlClass 𝒱 (mlSumCochain {p}) via a pairCover p (alphaPatch …) → 𝒱 refinement (mlClass_res), packaged through the same mlClassAt_eq_of_valid used for mlClassAt's original construction.
   • main (Finset.induction_on): combines CLAIM1's individual classes across all of S via two-argument mlClass_add, giving ∑ p ∈ S, mlClassAt D p (restrict f) = mlClass 𝒱 (mlSumCochain S).
   • Finally mlClass 𝒱 (mlSumCochain S) = 0 directly via mlClass_eq_zero_of_exists with the global witness f itself (the difference mlSumCochain S i - restrict f is 0 exactly on marked members, D-bounded via off-S regularity elsewhere) — this is the "genuinely the same direct application" the design doc's §5.2(a) always expected, now unlocked.
2. H1Tail.toH1/H1Tail.toH1_injective — closed via Submodule.liftQ off (1), then a second, independent multi-point construction (injPatch/injD'/injψVD'/injG, inj_CLAIM1/inj_main/inj_hcoe), this time for an arbitrary z : T D (no global function available a priori — representatives ψ p are chosen via TailAt.mk_surjective, and the auxiliary divisor D' := S.sup' hSne (fun p => DPrimeOf D p (ψ p)) needs a genuine Finset.sup' since RS.Divisor X has no OrderBot — confirmed by direct inspection of Function.locallyFinsuppWithin's instances: divisors can be arbitrarily negative, so Finset.sup (which needs ⊥) is unavailable; Finset.sup' with the Finset's own nonemptiness witness is the correct tool). Given tailToH1 D z = 0, the same "sum equals one big mlClass" machinery reduces this to Cech.mlClass_eq_zero_iff's ⇒ half (Forster 12.4, toH1_injective, confirmed landed at Injectivity.lean:247), which hands back a global φ : LinSys D' with ∀ i x ∈ 𝒰.U i, D-bounded mlSumCochain-analogue i - restrict φ; reading this bound off at each marked point p (x = p) gives TailAt.mk p D (ψ p) = TailAt.mk p D (restrict φ) directly via TailAt.mk_eq_zero_iff, i.e. z = alpha D φ. At non-marked points p ∉ S (where z p = 0 already), the same bound read off at a different point q ∈ S sharing p's cover member (or directly, if p's member is unmarked) gives φ's own order bound at p, via the sum-splitting trick restrict φ = ψ q + (-(ψ q - restrict φ)) and ord_add/ ord_neg (mirrors exactly how gOf_memLD_of_clean bounds a coboundary from two one-sided pieces, one level up).
3. H1Tail.equivOfSurjective: a conditional equivalence, parametrized by an explicit Function.Surjective (tailToH1 D) hypothesis (per CONVENTIONS.md rule 3 and the design's own R1 fallback plan) — an honest statement, not a vacuous one, ready the moment surjectivity lands.

NOT closed: surjectivity of tailToH1 (item 3). This is the one item that resisted this finisher pass, and — contrary to the previous builder's framing (design doc §5.2(b), "gated on dolbeault-comparison's Leray theorem, not yet on disk") — it is not simply a citation away now that Jacobian/DolbeaultComparison/Leray.lean (677 lines, confirmed complete: exists_trade, toH1_surjective_of_isGood, h1CoverEquiv) has landed. A careful proof attempt (recorded here so the next builder does not have to redo this analysis) shows:

• toH1_surjective_of_isGood lets us represent any ξ : Cech.H1 D by a cocycle f on a good cover 𝒰₀ (all members chart disks). Refining 𝒰₀ to be also adapted to D's support (via exists_adapted_refinement, no extra work) gives a representative f' on a refinement 𝒱 — this refinement step is free (resZ1/toH1_resH1, no surjectivity needed).
• The genuinely hard step is showing f''s class is already of Mittag-Leffler shape (a sum of local mlClassAt-type contributions at D's finitely many marked points) modulo a coboundary on 𝒱. This is not implied by 𝒰₀ being good: the induced sub-cocycle on the "background" members (away from all marked points, where D = 0) is a bona fide Čech H¹(𝒪_X)-valued obstruction (dimension = genus), and there is no elementary reason it vanishes — indeed it should generically not vanish; what Mittag-Leffler theory guarantees is that the marked-point tail data can absorb it, which is a genuinely analytic fact (classically proved via dbar-solving with prescribed principal parts, i.e. subtracting a local singular correction then solving a smooth dbar-problem for the remainder) — not a fact this unit's editable surface (Jacobian/LaurentTail/ only, per the task's hard rules) has the machinery to prove: it would need a genuinely new result in Jacobian/Dbar//Jacobian/DolbeaultComparison/ (a meromorphic, not smooth, dbar-existence theorem), which is out of scope for this unit to build even if time permitted, since those directories are not in this unit's edit surface.
• An inductive bootstrap from the D = 0 case (dolbeaultEquiv/cechToH01, PDE-based, is built in DolbeaultComparison/Comparison.lean) via the six-term sequence's H1Incl_surjective was also considered: raising D one point at a time via H1Incl only transports surjectivity forward (from smaller to larger D), and a divisor with mixed-sign values can't be reached from 0 by a monotone chain in one direction only — this route does not close either without additional (unbuilt) input.
• Recommendation for whoever picks this up: either (a) prove a bespoke local statement in Jacobian/Dbar/ (a meromorphic dbar-existence lemma: given a smooth (0,1)-form and finitely many prescribed principal parts, solve dbar u = η away from the marked points with u having exactly those principal parts — the classical route), filed as a docs/requests/dolbeault-comparison.md or docs/requests/dbar-solvability.md ask since it is outside this unit's own surface, or (b) accept H1Tail.equivOfSurjective's conditional form as the unit's final deliverable on this point, matching the design's own R1 fallback plan exactly.

Two build-engineering gotchas hit and fixed this pass (recorded so no one repeats the slow path):

• Opens X-level ≤ composed with a Set X-level ⊆ via bare .trans (relying on the automatic Opens → Set coercion to make the composition typecheck) causes catastrophic isDefEq/whnf slowdown once the surrounding terms are sufficiently abstract (fully generic 𝒱/D/q, no concrete instantiation to short-circuit unification): confirmed by direct isolation, a single lemma (inj_hcoe) this way did not finish in 4,000,000 heartbeats / 7+ minutes wall-clock, whereas rewriting it to first coerce to an explicit (𝒱.U k : Set X) ⊆ (patch : Set X) term and then .trans (now a plain Set.Subset.trans, monomorphic, fast to resolve) closes in under 10 seconds. Grep for this pattern ().trans ( immediately after an Opens-typed term) if a similar slowdown resurfaces elsewhere in this codebase.
• A single tactic proof accumulating ~25 have/set steps hits a severe elaboration performance wall regardless of maxHeartbeats (confirmed: 20,000,000 heartbeats, 10+ minutes wall-clock, still did not finish) — not the same issue as the .trans one above (it persisted after that fix was applied in isolation). The fix is architectural: factor the construction into separate top-level noncomputable def/theorem declarations, each stated against an explicit variable (…) := … block plus include … in (Lean 4 does not auto-include a section variable into a declaration just because the declaration's tactic proof references it — only variables appearing in the stated type are auto-included; anything used only in the proof needs an explicit include, confirmed by direct experiment). This mirrors exactly how tailToH1_alpha's own helpers (alphaPatch/mlSumCochain/…) were already structured, and is now the pattern used throughout injPatch/injG/inj_* as well.

RiemannRoch.lean: Jacobian/Finiteness/Chi.lean has landed (confirmed, Finiteness.lean's own root docstring: "Unit COMPLETE, all 7 design files, zero sorries") — that gate is now open. The sole remaining gate for RiemannRoch.lean is H1Tail.equiv itself (unconditional surjectivity, item 3 above); see that file for the exact transport recipe, unchanged and ready to apply verbatim the moment surjectivity lands.