abel-theorem: the gated ofCurve_inj and final-assembly discharge (§4.4 D4)

Unit: abel-theorem. Namespace Jacobian. The challenge's ofCurve_inj (docs/Jacobian_challenge.lean:99), assembled from RS.Abel.genus_eq_zero_of_pathIntegral_mem (Sufficiency.lean) via the frozen ordering-resolution bridge (AddSubgroup.isClosed_of_discrete, §1.3/§9 of the design, spike-verified).

Both theorems below are stated exactly at their design shape and type-check; ofCurve_inj''s PROOF calls RS.Abel.genus_eq_zero_of_pathIntegral_mem, so it inherits that theorem's one remaining explicit hypothesis (RS.Abel.WeakSolutionUpgrade X, see Sufficiency.lean's own docstring for the precise account — the external serre-duality-tails blocker itself has CLEARED) transitively, as an explicit hypothesis argument here too (no NEW hypothesis is introduced in this file). ofCurve_inj is a one-line wrapper, discharged unconditionally the moment period-lattice-rank registers instance : DiscreteTopology (RS.periodSubgroup X) AND WeakSolutionUpgrade X is proved (see Sufficiency.lean for the precise remaining roadmap).

theorem Jacobian.ofCurve_inj' {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hupgrade : RS.Abel.WeakSolutionUpgrade X) (P : X) (h : 0 < genus X) [DiscreteTopology ↥(RS.periodSubgroup X)] : Function.Injective (ofCurve P)

The challenge lemma, gated on the literal (uncompleted) period subgroup's discreteness — Forster 21.4(i) exactly, NOT the .topologicalClosure variant jacobian-construction's other gated instances use (§4.4 reconciles the two shapes; period-lattice-rank is expected to register both, per the design's coordination note) — AND on RS.Abel.WeakSolutionUpgrade X (Sufficiency.lean), the one remaining, precisely-isolated non-external hypothesis.

theorem Jacobian.ofCurve_inj_of_upgrade {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hupgrade : RS.Abel.WeakSolutionUpgrade X) (P : X) (h : 0 < genus X) [DiscreteTopology ↥(RS.periodSubgroup X)] : Function.Injective (ofCurve P)

The literal challenge statement (docs/Jacobian_challenge.lean:99), discharged the moment period-lattice-rank registers instance : DiscreteTopology (RS.periodSubgroup X) for the real period subgroup (Forster 21.4(i)) AND RS.Abel.WeakSolutionUpgrade X is proved. A one-line wrapper, not new mathematics.

theorem Jacobian.ofCurve_inj_of_surjective' {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] (hsurj : Function.Surjective ⇑(RS.LaurentTail.tailToH1 0)) (P : X) (h : 0 < genus X) [DiscreteTopology ↥(RS.periodSubgroup X)] : Function.Injective (ofCurve P)

ofCurve_inj' with the WeakSolutionUpgrade hypothesis discharged (UpgradeDischarge.lean): the only remaining gates are period-lattice-rank's [DiscreteTopology (RS.periodSubgroup X)] and serre-duality-tails's single remaining external fact (Function.Surjective (tailToH1 0)).

theorem Jacobian.ofCurve_inj_of_surjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] (hsurj : Function.Surjective ⇑(RS.LaurentTail.tailToH1 0)) (P : X) (h : 0 < genus X) [DiscreteTopology ↥(RS.periodSubgroup X)] : Function.Injective (ofCurve P)

The literal challenge statement, gated on discreteness (period-lattice-rank's job) and the single serre-duality-tails fact only.