The tail-χ ledger: chiT additivity (serre-duality-tails, chiT-ledger closure)

Unit: serre-duality-tails (docs/design/serre-duality-tails.md §4/§9, orchestrator addendum 2026-07-08's "prove the TAIL-level six-term fragment + tail-chi ledger internally" instruction). This file discharges the ONE honest gap Duality.lean's docstring flagged: chiT's additivity (chiT D = chiT 0 + deg D), which is genuinely independent content from Serre duality (Miranda §2.3/2.6's own six-term exactness, not §3).

The construction. Exactly Finiteness/Chi.lean's own recipe (sixterm_rank1/2/3 → chi_of_le → chi_eq_chi_zero_add_degree), transposed to the tail level by replacing Čech's H1 D/windowConnect/H1Incl with the tail-level analogues built here:

• H1TailIncl (h : D ≤ D') : H1Tail D →ₗ H1Tail D': the descent of truncT h through the alphaL-quotients (well-defined by truncT_alpha); surjective because truncT h already is.
• windowConnectT (h : D ≤ D') : Window D D' →ₗ H1Tail D := H1Tail.mk D ∘ₗ windowToT D D' h (windowToT is laurent-tails' already-built embedding of Čech's finite window into the tail space, Jacobian/LaurentTail/TailSpace.lean).

The two hard exactness facts (ker windowConnectT = range windowMap, ker H1TailIncl = range windowConnectT) are proved entirely elementarily, at the tail level, with NO reference to Čech's own H1/mlClass/cochain machinery: H1Tail D being literally T D ⧸ range(alphaL D) (a coker, not a colimit of cochain complexes) makes both a matter of DFinsupp/Submodule bookkeeping + one witness-representative choice per point, exactly as the orchestrator's routing note anticipated ("H1Tail = coker(alphaL) makes the connecting/exactness elementary"). In particular this file does not wait on H1Tail.toH1's surjectivity (still out of scope, per Comparison.lean/the root docstring) — it is not used here at all.

Exports

• H1TailIncl, H1TailIncl_mk, H1TailIncl_surjective.
• windowConnectT, windowConnectT_apply.
• exact_windowMap_windowConnectT : Function.Exact (RS.Cech.windowMap h) (windowConnectT h).
• exact_windowConnectT_H1TailIncl : Function.Exact (windowConnectT h) (H1TailIncl h).
• chiT_of_le (h : D ≤ D') : chiT D' = chiT D + (D' - D).degree — the ledger step.
• chiT_single_add (D) (P) : chiT (D + single P 1) = chiT D + 1 — the task's headline additivity statement.
• chiT_eq_chiT_zero_add_degree (D) : chiT D = chiT 0 + D.degree — the primary deliverable.

H1TailIncl: the truncation map descended to H1Tail

noncomputable def RS.TailDuality.H1TailIncl {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') : LaurentTail.H1Tail D →ₗ[ℂ] LaurentTail.H1Tail D'

The truncation t^{D}_{D'} descends to H¹Tail, since it carries range(α_D) into range(α_{D'}) (truncT_alpha).

Equations

• RS.TailDuality.H1TailIncl h = (RS.LaurentTail.alphaL D).range.mapQ (RS.LaurentTail.alphaL D').range (RS.TailDuality.truncT h) ⋯

theorem RS.TailDuality.H1TailIncl_mk {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') (τ : LaurentTail.T D) : (H1TailIncl h) ((LaurentTail.H1Tail.mk D) τ) = (LaurentTail.H1Tail.mk D') ((truncT h) τ)

theorem RS.TailDuality.H1TailIncl_surjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') : Function.Surjective ⇑(H1TailIncl h)

windowConnectT: the connecting map Window D D' → H1Tail D

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

The tail-level connecting map: embed the finite Čech window into the tail space (windowToT), then project to H1Tail D.

Equations

• RS.TailDuality.windowConnectT h = RS.LaurentTail.H1Tail.mk D ∘ₗ RS.LaurentTail.windowToT D D' h

theorem RS.TailDuality.windowConnectT_apply {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') (w : Cech.Window D D') : (windowConnectT h) w = (LaurentTail.H1Tail.mk D) ((LaurentTail.windowToT D D' h) w)

theorem RS.TailDuality.windowToT_apply_of_not_mem {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [CompactSpace X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') (w : Cech.Window D D') {p : X} (hp : p ∉ Cech.diffSupp D D') : ((LaurentTail.windowToT D D' h) w) p = 0

windowToT's value off the witness Finset is 0 (unfolds T.mk).

Exactness at Window D D': ker (windowConnectT h) = range (windowMap h)

theorem RS.TailDuality.windowToT_windowMap {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') (φ : ↥(LinSys D')) : (LaurentTail.windowToT D D' h) ((Cech.windowMap h) φ) = (LaurentTail.alphaL D) ↑φ

The key identity: windowMap's image, embedded via windowToT, is exactly alphaL D of the same global section — the tail-level shadow of Čech's own Realizes/mlClass machinery, but here a direct pointwise computation (no cochains).

theorem RS.TailDuality.windowConnectT_windowMap {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') (φ : ↥(LinSys D')) : (windowConnectT h) ((Cech.windowMap h) φ) = 0

theorem RS.TailDuality.windowConnectT_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') (w : Cech.Window D D') : (windowConnectT h) w = 0 ↔ w ∈ (Cech.windowMap h).range

The harder half: a window class killed by windowConnectT already comes from L(D') via windowMap — an entirely elementary reconstruction (choose a representative per marked point, show the resulting global section lands in L(D') by a two-term order estimate).

theorem RS.TailDuality.exact_windowMap_windowConnectT {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') : Function.Exact ⇑(Cech.windowMap h) ⇑(windowConnectT h)

Exactness at Window D D': ker (windowConnectT h) = range (windowMap h).

Exactness at H1Tail D: ker (H1TailIncl h) = range (windowConnectT h)

theorem RS.TailDuality.truncT_windowToT_eq_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [CompactSpace X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') (w : Cech.Window D D') : (truncT h) ((LaurentTail.windowToT D D' h) w) = 0

The window's image, truncated one step further, vanishes IDENTICALLY (not merely mod range(alphaL D')) — the tail-level shadow of Čech's H1Incl_windowConnect, but here a direct computation: a window representative already has order ≥ -(D' p) at its marked point, so truncating to T D' kills it outright.

theorem RS.TailDuality.H1TailIncl_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') (z : LaurentTail.H1Tail D) : (H1TailIncl h) z = 0 ↔ z ∈ (windowConnectT h).range

The harder half: a class killed by H1TailIncl already comes from windowConnectT — an elementary reconstruction via a per-point representative choice (H1Tail being a genuine coker, not a colimit of cochain complexes, makes this a DFinsupp bookkeeping exercise, no cohomological machinery).

theorem RS.TailDuality.exact_windowConnectT_H1TailIncl {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') : Function.Exact ⇑(windowConnectT h) ⇑(H1TailIncl h)

Exactness at H1Tail D: ker (H1TailIncl h) = range (windowConnectT h).

The rank ledger, and chiT's additivity

theorem RS.TailDuality.sixterm_ranksT {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') : ∃ (p : ℕ) (q : ℕ), l D' = l D + p ∧ Module.finrank ℂ (Cech.Window D D') = p + q ∧ h1T D = q + h1T D'

theorem RS.TailDuality.chiT_of_le {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D D' : Divisor X} (h : D ≤ D') : chiT D' = chiT D + Function.locallyFinsuppWithin.degree (D' - D)

The tail ledger step: χT(D') = χT(D) + deg(D' − D) for D ≤ D'.

theorem RS.TailDuality.chiT_single_add {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (P : X) : chiT (D + Function.locallyFinsuppWithin.single P 1) = chiT D + 1

The task's headline additivity statement: adding a single point of multiplicity 1 raises χT by exactly 1.

theorem RS.TailDuality.chiT_eq_chiT_zero_add_degree {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : chiT D = chiT 0 + Function.locallyFinsuppWithin.degree D

The primary deliverable: χT(D) = χT(0) + deg D for every D (D' := D ⊔ 0, two applications of chiT_of_le, exactly Finiteness.chi_eq_chi_zero_add_degree's own recipe).