Nondegeneracy via the maximum principle (Forster 21.4(c), §5.1) #
Unit: period-lattice-rank (docs/design/period-lattice-rank.md §5.1, §6.5). The make-or-break
routing call: instead of Forster's L²-orthogonality chain (19.4–19.8, which needs a
chart-independent integral of smooth 2-forms this project does not have), we use the classical
"no nonconstant harmonic function on a compact surface" argument, localized to a single chart via
the complex open mapping theorem — no Hodge, no de Rham, no dissection, no 2-form integral.
Main declaration: RS.form1_eq_zero_of_re_period_eq_zero.
theorem
RS.form1_eq_zero_of_re_period_eq_zero
{X : Type u_1}
[TopologicalSpace X]
[CompactSpace X]
[ConnectedSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{η : Form1 X}
(h : ∀ (γ : Path (Classical.arbitrary X) (Classical.arbitrary X)), (period γ η).re = 0)
:
Nondegeneracy (Forster 21.4(c)): if every based loop's period has vanishing real part, the form is identically zero. Proof: the maximum principle (§5.1), replacing Forster's 19.4+19.5+19.7+10.15 chain.