periodSubgroup membership (Forster §21.2)

Unit: period-lattice-rank (docs/design/period-lattice-rank.md §6.1). periodSubgroup X is defined (jacobian-construction, Periods.lean) as the AddSubgroup.closure of the range of periodVector (basis X) over based loops at the fixed basepoint Classical.arbitrary X. Forster's Per(ω₁,…,ω_g) is literally this range (periods are additive under loop concatenation, so the range is already subgroup-closed); this file packages that range directly as an AddSubgroup and shows it equals periodSubgroup X, which is what Stage C of Discreteness.lean needs: a lattice element must come from a SINGLE based loop, not merely from the closure abstractly.

Main declarations: RS.periodRange X, RS.periodSubgroup_eq_periodRange, RS.mem_periodSubgroup_iff.

def RS.periodRange (X : Type u_1) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : AddSubgroup (Fin (genus X) → ℂ)

The range of period vectors of based loops at Classical.arbitrary X, packaged directly as an additive subgroup (Forster's Per(ω₁,…,ω_g), §21.2). Subgroup-closed by the loop algebra (periodVector_refl/_trans/_symm).

Equations

• One or more equations did not get rendered due to their size.

theorem RS.periodSubgroup_eq_periodRange (X : Type u_1) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : periodSubgroup X = periodRange X

The closure defining periodSubgroup is redundant: the generating set is already a subgroup (Forster's observation that Per is literally the range, not merely its span).

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

A vector lies in the period subgroup iff it is the period vector of a SINGLE based loop.