Local constancy of fiberMultSum (heart, part 2)

Combines the planar count (RootCounting.lean) with the stack of adapted charts (LocalStructure.lean) to show fiberMultSum F is locally constant, hence constant on the connected Y — the well-definedness theorem for degree.

• RS.FiberStack.sum_multiplicity_inter_source — per-chart count: over y ∈ S.V, the part of the fiber inside the i-th chart source carries total multiplicity multiplicity F (S.pt i) (transported through the adapted chart bijection with the planar root set of RootCounting).
• RS.FiberStack.fiberMultSum_eq_sum — the fiber-sum is the same (∑ i, multiplicity F (S.pt i)) for every y ∈ S.V, via the disjoint decomposition FiberStack.fiber_eq_iUnion.
• RS.isLocallyConstant_fiberMultSum — fiberMultSum F is locally constant on all of Y.
• RS.fiberMultSum_const — THE well-definedness theorem: fiberMultSum F is the same at every y : Y (needs [ConnectedSpace Y]).

theorem RS.FiberStack.sum_multiplicity_inter_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {y₀ : Y} (S : FiberStack F y₀) (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) {y : Y} (hy : y ∈ S.V) (i : Fin S.n) : ∑ᶠ (x : X) (_ : x ∈ F ⁻¹' {y} ∩ (S.A i).e.source), multiplicity F x = multiplicity F (S.pt i)

Per-chart count (heart, part 2a): over y ∈ S.V, the part of the fiber inside the i-th chart source carries total multiplicity multiplicity F (S.pt i).

theorem RS.FiberStack.fiberMultSum_eq_sum {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {y₀ : Y} (S : FiberStack F y₀) (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) {y : Y} (hy : y ∈ S.V) : fiberMultSum F y = ∑ i : Fin S.n, multiplicity F (S.pt i)

Heart, part 2b: the fiber-sum is the same (∑ i, multiplicity F (S.pt i)) for every y ∈ S.V.

theorem RS.isLocallyConstant_fiberMultSum {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) : IsLocallyConstant (fiberMultSum F)

fiberMultSum F is locally constant on all of Y (including at branch values): at every y₀, the stack's neighborhood S.V witnesses constancy via fiberMultSum_eq_sum applied twice (at y and at y₀).

theorem RS.fiberMultSum_const {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} [ConnectedSpace Y] (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (y y' : Y) : fiberMultSum F y = fiberMultSum F y'

THE well-definedness theorem: fiberMultSum F takes the same value at every point of the connected Y.