theorem RRApplicationsAudit.audit_degK_derivation (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.degK = 2 * C.g - 2

Audit: derivation of deg K = 2g − 2 (Cor 31, Lec 24).

theorem RRApplicationsAudit.audit_riemann_inequality (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 d) : SD.h0 ≥ d + 1 - C.g

Audit: Riemann inequality h^0(L) ≥ d + 1 − g for line bundles.

theorem RRApplicationsAudit.audit_corollary_29 (C : CanonicalSheafCurves.SmoothCompleteCurve) (_hg : C.g ≥ 0) (h0_K h1_K : ℤ) (hchi_K : C.χ (1, C.degK) = h0_K - h1_K) (hSD_K : h1_K = 1) : h0_K = C.g

Audit of Cor 29 (Lec 24): h^0(K) = g.

theorem RRApplicationsAudit.audit_high_degree_exact (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 d) (h1_zero : SD.h1 = 0) : SD.h0 = d + 1 - C.g

Audit: vanishing of h^1 makes Riemann–Roch exact.

theorem RRApplicationsAudit.audit_genus_zero_sections (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 0) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 1) (h1_zero : SD.h1 = 0) : SD.h0 = 2

Audit: degree-1 line bundles on ℙ¹ have two global sections.

theorem RRApplicationsAudit.audit_serre_duality_chi (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) : C.χ (1, d) + C.χ (1, C.degK - d) = 0

Audit: Euler-characteristic form of Serre duality.

theorem RRApplicationsAudit.audit_P1_consistency (k : Type) [Field k] (n : ℤ) : (CanonicalSheafCurves.mkCurve 0).χ (1, n) = ↑(Module.finrank k (SheafCohomology.H0 k n)) - ↑(Module.finrank k (SheafCohomology.H1 k n))

Audit: consistency between the abstract Euler characteristic on mkCurve 0 and the concrete Čech computation on ℙ¹.

theorem RRApplicationsAudit.audit_dedekind_grounding {k : Type u_1} [Field k] (C : DedekindCurve k) : C.toSmoothCompleteCurve.g = ↑C.ddGenus

Audit: the genus of the smooth curve associated to a Dedekind curve C matches the Dedekind-theoretic genus C.ddGenus.

theorem RRApplicationsAudit.audit_dedekind_SD_O {k : Type u_1} [Field k] (C : DedekindCurve k) : (RiemannRochApplications.serreDualityO_fromDedekind C).h0 = 1 ∧ (RiemannRochApplications.serreDualityO_fromDedekind C).h1 = ↑C.ddGenus

Audit: the Serre-duality bundle for the structure sheaf of a Dedekind curve has h^0 = 1 and h^1 = g.

theorem RRApplicationsAudit.audit_full_pipeline_genus0 (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 0) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 1) (h1_zero : SD.h1 = 0) : SD.h0 = 2 ∧ C.degK = -2 ∧ C.χ (1, 0) = 1

Audit: full Riemann–Roch pipeline for genus 0 collects the three key facts (h^0 = 2 for 𝒪(1), deg K = −2, χ(𝒪) = 1).

theorem RRApplicationsAudit.audit_full_pipeline_general (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 d) : SD.h0 ≥ d + 1 - C.g ∧ C.χ (1, d) + C.χ (1, C.degK - d) = 0 ∧ C.degK = 2 * C.g - 2

Audit: full Riemann–Roch pipeline in general (Riemann inequality, Euler-characteristic Serre duality, deg K = 2g − 2).

theorem RRApplicationsAudit.audit_elliptic_pipeline (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 1) (SD3 : RiemannRochRiemannForm.SerreDualityCurve C 1 3) (h1_zero : SD3.h1 = 0) : C.χ (1, 0) = 0 ∧ C.degK = 0 ∧ SD3.h0 = 3

Audit: elliptic pipeline (χ(𝒪) = 0, K trivial, h^0(𝒪(3p)) = 3).