Discreteness of the period subgroup (Forster 21.4(a)+(b))

Unit: period-lattice-rank (docs/design/period-lattice-rank.md §6.3). The local Jacobi map (via the inverse function theorem on ℂ^g) plus the Abel k-point sufficiency direction plus the residue theorem show Λ ∩ W ⊆ {0} for an explicit neighborhood W of 0, hence Λ is discrete.

GATED: on RS.Abel.WeakSolutionUpgradeFinset X ↥S (Abel's own remaining hypothesis, for every S : Finset (Fin (genus X)) that can arise as the "moved-coordinates" index set) — every theorem here threads it explicitly, exactly as Jacobian.Abel does for its own gated exports; it discharges automatically once that unit's sibling pass proves it unconditionally.

Main declarations: RS.exists_isolating_nhds_periodSubgroup, RS.discreteTopology_periodSubgroup, RS.periodSubgroup_topologicalClosure_eq, RS.discreteTopology_periodSubgroup_topologicalClosure.

@[reducible, inline]

abbrev RS.DiscretenessHyp (X : Type u_2) [TopologicalSpace X] [T2Space X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Prop

The upgrade hypothesis this unit consumes, universally over every Finset-indexed shape that can arise (the k-point Abel sufficiency direction, threaded exactly as Jacobian.Abel states it).

Equations

• RS.DiscretenessHyp X = ∀ (S : Finset (Fin (genus X))), RS.Abel.WeakSolutionUpgradeFinset X ↥S

theorem RS.exists_isolating_nhds_periodSubgroup {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hg : 1 ≤ genus X) (hupgrade : DiscretenessHyp X) : ∃ W ∈ nhds 0, ∀ t ∈ periodSubgroup X, t ∈ W → t = 0

Forster 21.4(a)+(b): the local Jacobi map (inverse function theorem) plus the Abel k-point sufficiency direction plus the residue theorem isolate 0 in the period subgroup.

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

Discreteness discharge: genus X = 0 handled by the subsingleton argument; genus X ≥ 1 via exists_isolating_nhds_periodSubgroup.

theorem RS.periodSubgroup_topologicalClosure_eq {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hupgrade : DiscretenessHyp X) : (periodSubgroup X).topologicalClosure = periodSubgroup X

The closure of periodSubgroup X is itself, once it is discrete: discreteness implies closedness (AddSubgroup.isClosed_of_discrete).

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

The gated DiscreteTopology instance for the closure, the shape jacobian-construction's ledger needs directly.