The χ ledger (finiteness-and-chi, gated file 3/3)

Unit: finiteness-and-chi (docs/design/finiteness-and-chi.md §8).

• finiteDimensional_linSys: FiniteDimensional ℂ (LinSys D) for ALL D (same six-term bookkeeping recipe as H1Finite.lean's all-D step, applied to windowMap instead of H1Incl).
• h1/chi: the χ ledger's frozen definitions (chi D := (l D : ℤ) − (h1 D : ℤ)).
• sixterm_ranks: the shared rank bookkeeping fact behind every monotonicity/ledger lemma — four rank-nullity applications along cech's six-term fragment 0 → L(D) → L(D') → Window D D' → H¹(D) → H¹(D') → 0, packaged as two witness naturals.
• chi_of_le/chi_eq_chi_zero_add_degree: the ledger identity chi D' = chi D + deg(D'−D) and its D = 0-anchored specialization.
• chi_zero_add_degree_le_l/exists_ne_zero_mem_linSys: the Riemann-inequality seed canonical-forms' Existence gate consumes (Forster 16.11 pattern), at the exact names/shapes docs/design/canonical-forms.md §D9 records.
• l_mono/l_le_l_add_degree/h1_le_of_le/h1_le_h1_add_degree: monotonicity corollaries.

All-D finiteness of L(D) (same recipe as H1Finite.lean's all-D step)

instance RS.Finiteness.finiteDimensional_linSys {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] (D : Divisor X) : FiniteDimensional ℂ ↥(LinSys D)

All-D finiteness of the linear system: L(D) is finite-dimensional for every D. With D' := D ⊔ 0: windowMap (0 ≤ D') : L(D') →ₗ Window 0 D' has finite-dimensional kernel (= range of the injective inclusion L(0) ↪ L(D'), cech's exact_inclusion_windowMap) and finite-dimensional codomain (Window 0 D'), so L(D') is finite; L(D) ≤ L(D') finishes it.

The χ ledger's frozen definitions

noncomputable def RS.Finiteness.h1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : ℕ

h¹(D): the dimension of the first Čech cohomology of 𝒪_D.

Equations

• RS.Finiteness.h1 D = Module.finrank ℂ (RS.Cech.H1 D)

noncomputable def RS.Finiteness.chi {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : ℤ

The Euler characteristic χ(D) = l(D) - h¹(D).

Equations

• RS.Finiteness.chi D = ↑(RS.l D) - ↑(RS.Finiteness.h1 D)

The shared six-term rank bookkeeping

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

theorem RS.Finiteness.l_mono {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] {D D' : Divisor X} (h : D ≤ D') : l D ≤ l D'

theorem RS.Finiteness.l_le_l_add_degree {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] {D D' : Divisor X} (h : D ≤ D') : l D' ≤ l D + (Function.locallyFinsuppWithin.degree (D' - D)).toNat

theorem RS.Finiteness.h1_le_of_le {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] {D D' : Divisor X} (h : D ≤ D') : h1 D' ≤ h1 D

theorem RS.Finiteness.h1_le_h1_add_degree {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] {D D' : Divisor X} (h : D ≤ D') : h1 D ≤ h1 D' + (Function.locallyFinsuppWithin.degree (D' - D)).toNat

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

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

Divisor.single bookkeeping (Compat: degree_single not upstreamed)

theorem RS.Finiteness.degree_single {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] (P : X) : Function.locallyFinsuppWithin.degree (Function.locallyFinsuppWithin.single P 1) = 1

theorem RS.Finiteness.chi_single_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] (D : Divisor X) (P : X) : chi (D + Function.locallyFinsuppWithin.single P 1) = chi D + 1

theorem RS.Finiteness.chi_eq_chi_zero_add_degree {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] (D : Divisor X) : chi D = chi 0 + Function.locallyFinsuppWithin.degree D

§8's anchor: χ(D) = χ(0) + deg D for every D (no induction — derive from chi_of_le twice at D' := D ⊔ 0).

theorem RS.Finiteness.chi_zero_add_degree_le_l {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] (D : Divisor X) : chi 0 + Function.locallyFinsuppWithin.degree D ≤ ↑(l D)

The Riemann-inequality seed (canonical-forms' workhorse): χ(0) + deg D ≤ l(D).

theorem RS.Finiteness.exists_ne_zero_mem_linSys {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] {D : Divisor X} (h : 0 < chi 0 + Function.locallyFinsuppWithin.degree D) : ∃ f ∈ LinSys D, f ≠ 0

The existence half (Forster 16.11 pattern): once χ(0) + deg D > 0, L(D) is nontrivial.