riemann-roch: Riemann–Roch, l(K) = g, deg K = 2g − 2, the Riemann inequality

Unit: riemann-roch (#28), per docs/design/serre-duality-tails.md §9.1 + the TailDuality root docstring's export bank / consumer notes. A thin assembly unit (per the blueprint's own framing): every proof below is omega-level ℤ-arithmetic combining TailDuality's tail-level ledger (chiT_eq_chiT_zero_add_degree, the primary deliverable of the prerequisite pass) with its Serre-duality export bank (l_sub_eq_h1T, h1T_zero_eq_genus, h1T_zero_eq_l_K) and RS.l_zero. No new mathematics; no reference to T D/pairT/chi's internals (the interface docs/design/serre-duality-tails.md §9.1 demands).

• chiT_zero : TailDuality.chiT 0 = 1 - g.
• riemannRoch {ω₀} (h₀) (D) : l D - l(K − D) = deg D + 1 - g — the headline theorem.
• l_K_eq_genus {ω₀} (h₀) : l K = g.
• deg_canonical {ω₀} (h₀) : deg K = 2 * g - 2.
• riemann_inequality (D) : deg D + 1 - g ≤ l D — the forward-headline seed genus-zero-headline (#30) consumes.

theorem RS.chiT_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] : TailDuality.chiT 0 = 1 - ↑(genus X)

χT(0) = 1 - g, from Liouville (RS.l_zero) and the tail-duality genus identification (h1T_zero_eq_genus).

theorem RS.riemannRoch {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] {ω₀ : MForm X} (h₀ : ω₀ ≠ 0) (D : Divisor X) : ↑(l D) - ↑(l (canonicalDivisorOf ω₀ - D)) = Function.locallyFinsuppWithin.degree D + 1 - ↑(genus X)

Riemann–Roch. l(D) − l(K − D) = deg D + 1 − g for any canonical divisor K (seeded by a nonzero reference form ω₀). Proof: the tail ledger chiT D = chiT 0 + deg D combined with Serre duality l(K − D) = h1T D and chiT 0 = 1 - g; pure ℤ-arithmetic.

theorem RS.l_K_eq_genus {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] {ω₀ : MForm X} (h₀ : ω₀ ≠ 0) : l (canonicalDivisorOf ω₀) = genus X

l(K) = g (Riemann–Roch's own dictionary at D = K, packaged directly from the tail-duality export bank).

theorem RS.deg_canonical {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] {ω₀ : MForm X} (h₀ : ω₀ ≠ 0) : Function.locallyFinsuppWithin.degree (canonicalDivisorOf ω₀) = 2 * ↑(genus X) - 2

deg K = 2g − 2 (Riemann–Roch applied at D := K, then l K = g/l 0 = 1).

theorem RS.riemann_inequality {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] (D : Divisor X) : Function.locallyFinsuppWithin.degree D + 1 - ↑(genus X) ≤ ↑(l D)

The Riemann inequality: deg D + 1 − g ≤ l D, unconditionally (no reference form needed — chiT's ledger plus h1T ≥ 0). The forward-headline seed genus-zero-headline (#30) uses at D := single P 1 in genus 0.