Identity theorem for 1-form coefficients (§6.4) #
Unit: period-lattice-rank (docs/design/period-lattice-rank.md §6.4). A self-contained clopen
propagation argument: if η ∈ Form1 X's preferred-chart coefficient at some point vanishes on a
whole neighborhood, η = 0 identically. Needed by Nondegeneracy.lean's maximum-principle route
(the last step, replacing Forster's Thm 19.4).
Main declaration: RS.form1_eq_zero_of_eventually_coeffIn_zero.
theorem
RS.form1_eq_zero_of_eventually_coeffIn_zero
{X : Type u_1}
[TopologicalSpace X]
[ConnectedSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{η : Form1 X}
{x₀ : X}
(h : ∀ᶠ (z : ℂ) in nhds (↑(chartAt ℂ x₀) x₀), coeffIn (chartAt ℂ x₀) η z = 0)
:
The identity theorem: eventual vanishing of η's coefficient in one chart forces η = 0
everywhere.