Disk acyclicity of 𝒪_D (Jacobian/Dbar/DiskAcyclic.lean)

Unit: dbar-solvability (docs/design/dbar-solvability.md D9, §4.8, §7.4). Depends on the sibling units cech-cohomology (Jacobian.Cech.Cochains) and meromorphic-and-divisors (Jacobian.Meromorphic).

Main deliverable (D=0 case, the sheaf 𝒪 of holomorphic functions): Z¹(cover of a chart disk, 𝒪) = B¹, i.e. H¹(chart disk, 𝒪) = 0 — every additive holomorphic cocycle on a finite cover of a chart disk splits, via PlanarCousin.exists_holo_splitting_ball transported through the chart and cech's MeroGermOn/evalAt germ API for the pointwise bookkeeping.

DEVIATION (honestly reported): the general-divisor twist (subsingleton_h1Cover_of_isChartDisk, needing [T2Space X] [CompactSpace X] and a finite-product twisting germ q := ∏ a ∈ D.support ∩ V, (· - e a) ^ D (e.symm a)) is NOT included — it is a substantial independent construction (one-directional twisted cochain maps commuting with d0/d1/ restrictL) that did not fit the remaining time budget; see the final report. The D = 0 case below is a complete, self-contained, fully admitted-free proof of disk acyclicity for the structure sheaf, which is the piece the design flags as needed with "no compactness".

Compat helpers (holomorphic ⇒ meromorphic, candidates for upstreaming to mero)

theorem RS.meromorphicOnX_of_contMDiffOn_omega {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {U : Set X} (hU : IsOpen U) {u : X → ℂ} (hu : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ u U) : MeromorphicOnX u U

theorem RS.mk_mem_linSysOn_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {U : Set X} (hU : IsOpen U) {u : X → ℂ} (hu : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ u U) : MeroGermOn.mk u ⋯ ∈ LinSysOn 0 U

theorem RS.subsingleton_h1Cover_zero_of_isChartDisk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {V : TopologicalSpace.Opens X} (hV : Cech.IsChartDisk V) (𝒱 : Cech.FinCover V) : Subsingleton (Cech.H1Cover 0 𝒱)

Acyclicity for 𝒪 (no compactness needed): H¹ of a finite cover of a chart disk, with the structure sheaf's coefficients, vanishes.

General-divisor twist: subsingleton_h1Cover_of_isChartDisk

The remaining honestly-deferred piece from the DEVIATION note above (§D9(b) of docs/design/dbar-solvability.md): the general-divisor case, needed by dolbeault-comparison/Leray.lean's member-splitting step. Built here under that unit's SPECIAL AUTHORIZATION (the cross-unit dependencies were present, it was deferred on time, not difficulty). Route: a finite Weierstrass-factor germ t on V with ord t = D there (t w := ∏_{a ∈ S} (w - e a) ^ D a, S := D.support ∩ V, pulled back through the chart e := chartAt ℂ x₀); multiplying a D-cocycle by (restrictions of) t gives a 0-cocycle, reducing to subsingleton_h1Cover_zero_of_isChartDisk above; dividing a 0-splitting by t gives back a D-splitting.

theorem RS.subsingleton_h1Cover_of_isChartDisk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [T2Space X] [CompactSpace X] {V : TopologicalSpace.Opens X} (hV : Cech.IsChartDisk V) (D : Divisor X) (𝒱 : Cech.FinCover V) : Subsingleton (Cech.H1Cover D 𝒱)

MAIN deliverable (owed to cech §7 / consumed by dolbeault-comparison's Leray 12.8): disk acyclicity of the Čech complex of 𝒪_D on chart disks, for an ARBITRARY divisor D.