abel-theorem: loop-cancellation algebra (docs/design/abel-theorem.md §4.2, D2, §2.1 steps 1-3)

Unit: abel-theorem. Namespace RS.Abel. Two deliverables:

• mem_periodSubgroup_iff_exists_loop — RS.periodSubgroup X's generating set (based-loop period vectors) is already closed under +/neg/0 (RS.periodVector_trans/_symm/_refl, BUILT), so AddSubgroup.closure of it adds nothing new: every element of the closure is already the periodVector of a SINGLE based loop. Proved via AddSubgroup.closure_induction, mirroring exactly how RS.periodVector_mem_periodSubgroup (BUILT, OfCurve.lean) proves the reverse inclusion via conjugation.
• exists_zeroPeriod_path — the loop-cancellation construction itself (§2.1 steps 1-3): given a path δ : Path Q P whose basis-period vector lies in RS.periodSubgroup X, produce ANOTHER path δ' : Path Q P (differing from δ by a based loop, conjugated to be based at Q) with exactly zero integral against every ω ∈ RS.Form1 X, not merely against the basis (Forster's own Remark: "only needs to be checked for a basis" — extended to all of Form1 X via linearity of RS.pathIntegralₗ and Module.Basis.ext).

theorem RS.Abel.mem_periodSubgroup_iff_exists_loop {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {v : Fin (genus X) → ℂ} : v ∈ periodSubgroup X ↔ ∃ (α : Path (Classical.arbitrary X) (Classical.arbitrary X)), periodVector (basis X) α = v

Compat (request filed to jacobian-construction's Periods.lean, built here as this unit's own D2 since it is small and self-contained): RS.periodSubgroup X's generating set is already closed under the loop operations, so the closure adds nothing — every element is the periodVector of a single based loop at the fixed basepoint Classical.arbitrary X.

theorem RS.Abel.exists_zeroPeriod_path {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Q P : X} (δ : Path Q P) (hmem : (fun (i : Fin (genus X)) => pathIntegral δ ((basis X) i)) ∈ periodSubgroup X) : ∃ (δ' : Path Q P), ∀ (η : Form1 X), pathIntegral δ' η = 0

The loop-cancellation construction (§2.1 steps 1-3): if δ's basis-period vector lies in RS.periodSubgroup X, there is another path δ' : Path Q P with EXACTLY zero integral against every ω ∈ RS.Form1 X.