Full rank and the IsZLattice discharge (Forster 21.4(c) shell, §6.6)

Unit: period-lattice-rank (docs/design/period-lattice-rank.md §6.6). span_real_periodSubgroup is the linear-algebra shell around Nondegeneracy.lean's form1_eq_zero_of_re_period_eq_zero: if the period subgroup lay in a proper real subspace, a nonzero real linear functional vanishing on it would complexify (Forster: "every real linear form is the real part of a complex linear form") to a nonzero holomorphic form with vanishing real periods, contradicting nondegeneracy. Ungated (uses only Nondegeneracy.lean + mathlib).

The IsZLattice instance-shaped discharge is gated exactly as Discreteness.lean's DiscretenessHyp, since IsZLattice's class carries [DiscreteTopology L].

Main declarations: RS.span_real_periodSubgroup, RS.isZLattice_periodSubgroup_topologicalClosure, RS.finrank_int_periodSubgroup.

theorem RS.span_real_periodSubgroup {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Submodule.span ℝ ↑(periodSubgroup X) = ⊤

Forster 21.4(c): the period subgroup spans Fin (genus X) → ℂ over ℝ (nondegeneracy). Ungated: uses only form1_eq_zero_of_re_period_eq_zero (mathlib + built units).

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

The gated IsZLattice instance-shape the ledger needs, once discreteness discharges (DiscretenessHyp, exactly Discreteness.lean's gate).

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

Bonus (blueprint's "real basis of rank 2g"): free once the IsZLattice instance is discharged, via mathlib's ZLattice.rank.