The final gate, closed: ungated exports (cechcount unit)

Count.lean's RS.cechCount (dim H¹(𝒪_X) ≤ genus X) discharges — through the BUILT equivalence RS.Abel.tailToH1_zero_surjective_iff_finrank_le — the single fact every remaining gate of the project was reduced to. This file records the ungated finals:

• RS.tailToH1_zero_surjective — surjectivity of the Laurent-tail comparison at D = 0 (the surjectivity half of Serre duality for 𝒪_X).
• RS.finrank_H1_zero_eq_genus — dim_ℂ H¹(X, 𝒪_X) = genus X (the Čech identity the cech-h1-genus unit deferred).
• RS.Abel.weakSolutionUpgrade_final : WeakSolutionUpgrade X and RS.Abel.weakSolutionUpgradeFinset_final (via the built …_of_surjective discharges).
• RS.discretenessHyp_final : RS.DiscretenessHyp X — the period-lattice gate.
• The global instances DiscreteTopology (RS.periodSubgroup X), DiscreteTopology (RS.periodSubgroup X).topologicalClosure and IsZLattice ℝ (RS.periodSubgroup X).topologicalClosure.toIntSubmodule (the exact recorded final-assembly shapes from Jacobian/PeriodLattice.lean).
• RS.finrank_int_periodSubgroup_final — the period lattice has ℤ-rank 2·genus X.
• Jacobian.ofCurve_inj — the Abel–Jacobi map is injective for 0 < genus X, with no remaining hypotheses (the challenge's ofCurve_inj, ungated).

theorem RS.tailToH1_zero_surjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] : Function.Surjective ⇑(LaurentTail.tailToH1 0)

The single remaining gate of the project, closed: the Laurent-tail comparison map into Čech H¹ is surjective at D = 0 (surjectivity half of Serre duality for 𝒪_X), by RS.cechCount through the built dimension-count equivalence.

theorem RS.finrank_H1_zero_eq_genus {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Module.finrank ℂ (Cech.H1 0) = genus X

The Čech identity dim_ℂ H¹(X, 𝒪_X) = genus X (the fact the cech-h1-genus unit had to defer), now unconditional.

theorem RS.Abel.weakSolutionUpgrade_final {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : WeakSolutionUpgrade X

The weak-solution upgrade, ungated (Forster §20's Abel-necessity input).

theorem RS.Abel.weakSolutionUpgradeFinset_final {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} [Fintype ι] : WeakSolutionUpgradeFinset X ι

The Finset weak-solution upgrade, ungated (the k-point Abel sufficiency input).

theorem RS.discretenessHyp_final {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : DiscretenessHyp X

The period-lattice discreteness gate, discharged.

instance RS.instDiscreteTopologySubtypeForallFinGenusComplexMemAddSubgroupPeriodSubgroup {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : DiscreteTopology ↥(periodSubgroup X)

The period subgroup is discrete (Forster 21.4), globally as an instance.

instance RS.instDiscreteTopologySubtypeForallFinGenusComplexMemAddSubgroupTopologicalClosurePeriodSubgroup {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : DiscreteTopology ↥(periodSubgroup X).topologicalClosure

The recorded final-assembly instance (Jacobian/PeriodLattice.lean discharge shape).

instance RS.instIsZLatticeRealForallFinGenusComplexCoeOrderIsoAddSubgroupSubmoduleIntToIntSubmoduleTopologicalClosurePeriodSubgroup {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : IsZLattice ℝ (AddSubgroup.toIntSubmodule (periodSubgroup X).topologicalClosure)

The recorded final-assembly instance (Jacobian/PeriodLattice.lean discharge shape): the closed period subgroup is a genuine ℤ-lattice in ℂ^g.

theorem RS.finrank_int_periodSubgroup_final {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Module.finrank ℤ ↥(AddSubgroup.toIntSubmodule (periodSubgroup X).topologicalClosure) = 2 * genus X

The period lattice has ℤ-rank 2·genus X (Forster 21.4's "real basis of rank 2g"), ungated.

theorem Jacobian.ofCurve_inj {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (P : X) (h : 0 < genus X) : Function.Injective (ofCurve P)

The Abel–Jacobi map is injective for positive genus — the challenge's ofCurve_inj, with every gate discharged (no upgrade hypothesis, no discreteness instance argument).