The trace–period relation (jacobian-functoriality §7, period-level form)

Unit: jacobian-functoriality. For a loop δ in Y running through regular values of f, the path integral of Tr_f η along δ decomposes as a finite sum of X-loop integrals of η — with loops independent of η — so the trace maps period vectors into periodSubgroup X.

Route (cheaper than the design's full FiberChain/monodromy construction, same conclusion):

• Over a regular value's canonical stack all sheets are unramified, so each branch chart pair gives a genuine local section RS.sectionAt S i of f on S.V.
• Segment lemma (RS.pathIntegral_traceForm_segment): for a path inside one traceChart source, ∫ Tr_f η = ∑ sheets ∫ (section∘path) η, by exhibiting the sum of per-sheet disc primitives as a primitive of the trace (its chart coefficient is literally the sum of the transported sheet coefficients at regular values).
• Chain (RS.TraceChain, Lebesgue-number subdivision) + telescoping of a fixed primitive over the subdivision (RS.pathIntegral_segMap).
• Loop closing without monodromy bookkeeping: conjugate each sheet segment by fixed connecting paths from a basepoint (PathConnectedSpace.somePath); the correction terms are fibre sums as sets, independent of the enumerating stack, and telescope to 0 around the loop. No cycle decomposition, no lifted-path concatenation.

Local sections of f over a regular stack

noncomputable def RS.sectionAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y₀ : Y} (S : FiberStack f y₀) (i : Fin S.n) (y : Y) : X

The i-th local section of f associated to a fibre stack (an honest section on S.V when the i-th sheet is unramified).

Equations

• RS.sectionAt S i y = ↑(S.A i).e.symm (↑(S.A i).e' y)

theorem RS.e'_mem_e_target_of_regular {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y₀ : Y} {S : FiberStack f y₀} {i : Fin S.n} (hm : multiplicity f (S.pt i) = 1) {y : Y} (hy : y ∈ S.V) : ↑(S.A i).e' y ∈ (S.A i).e.target

theorem RS.sectionAt_mem_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y₀ : Y} {S : FiberStack f y₀} {i : Fin S.n} (hm : multiplicity f (S.pt i) = 1) {y : Y} (hy : y ∈ S.V) : sectionAt S i y ∈ (S.A i).e.source

theorem RS.e_sectionAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y₀ : Y} {S : FiberStack f y₀} {i : Fin S.n} (hm : multiplicity f (S.pt i) = 1) {y : Y} (hy : y ∈ S.V) : ↑(S.A i).e (sectionAt S i y) = ↑(S.A i).e' y

theorem RS.f_sectionAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y₀ : Y} {S : FiberStack f y₀} {i : Fin S.n} (hm : multiplicity f (S.pt i) = 1) {y : Y} (hy : y ∈ S.V) : f (sectionAt S i y) = y

The sections are genuine sections: f ∘ sectionAt S i = id on S.V.

theorem RS.continuousOn_sectionAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y₀ : Y} {S : FiberStack f y₀} {i : Fin S.n} (hm : multiplicity f (S.pt i) = 1) : ContinuousOn (sectionAt S i) S.V

theorem RS.finsum_mem_fiber_eq_sum_sectionAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y₀ : Y} {S : FiberStack f y₀} (hm : ∀ (j : Fin S.n), multiplicity f (S.pt j) = 1) {y : Y} (hy : y ∈ S.V) (t : X → ℂ) : ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {y}), t x = ∑ j : Fin S.n, t (sectionAt S j y)

Fibre sums over any point of a regular stack's neighborhood enumerate along the sections.

noncomputable def RS.liftSeg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y₀ : Y} {S : FiberStack f y₀} {i : Fin S.n} (hm : multiplicity f (S.pt i) = 1) {a b : Y} (p : Path a b) (hV : ∀ (s : ↑unitInterval), p s ∈ S.V) : Path (sectionAt S i a) (sectionAt S i b)

The lift of a path through the i-th section of a regular stack.

Equations

• RS.liftSeg hm p hV = { toFun := fun (s : ↑unitInterval) => RS.sectionAt S i (p s), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem RS.liftSeg_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y₀ : Y} {S : FiberStack f y₀} {i : Fin S.n} (hm : multiplicity f (S.pt i) = 1) {a b : Y} (p : Path a b) (hV : ∀ (s : ↑unitInterval), p s ∈ S.V) : ⇑(liftSeg hm p hV) = fun (s : ↑unitInterval) => sectionAt S i (p s)

The segment lemma

theorem RS.stackAt_mult_eq_one {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) {y₀ : Y} (hy₀ : IsRegularValue f y₀) (i : Fin (stackAt hf hne y₀).n) : multiplicity f ((stackAt hf hne y₀).pt i) = 1

Multiplicities of the canonical stack at a regular value are all 1.

theorem RS.pathIntegral_traceForm_segment {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) {y₀ : Y} (hy₀ : IsRegularValue f y₀) {a b : Y} (p : Path a b) (hV : ∀ (s : ↑unitInterval), p s ∈ (stackAt hf hne y₀).V) (hsrc : ∀ (s : ↑unitInterval), p s ∈ (chartAt ℂ y₀).source) (η : Form1 X) : pathIntegral p (traceForm hf hne η) = ∑ i : Fin (stackAt hf hne y₀).n, pathIntegral (liftSeg ⋯ p hV) η

The segment lemma: over a single (regular-centered) trace chart, the integral of the trace is the sum of the per-sheet lifted integrals.

Affine segment reparametrizations and telescoping

noncomputable def RS.Path.segMap {Y : Type u_2} [TopologicalSpace Y] {a b : Y} (δ : Path a b) (t₀ t₁ : ℝ) : Path (δ.extend t₀) (δ.extend t₁)

The affine segment [t₀, t₁] of a path, as a path between the extended endpoints.

Equations

• RS.Path.segMap δ t₀ t₁ = { toFun := fun (s : ↑unitInterval) => δ.extend ((1 - ↑s) * t₀ + ↑s * t₁), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem RS.Path.segMap_coe {Y : Type u_2} [TopologicalSpace Y] {a b : Y} (δ : Path a b) (t₀ t₁ : ℝ) : ⇑(segMap δ t₀ t₁) = fun (s : ↑unitInterval) => δ.extend ((1 - ↑s) * t₀ + ↑s * t₁)

theorem RS.Path.segMap_mem_Icc {Y : Type u_2} [TopologicalSpace Y] {a b : Y} (_δ : Path a b) {t₀ t₁ : ℝ} (h : t₀ ≤ t₁) (s : ↑unitInterval) : (1 - ↑s) * t₀ + ↑s * t₁ ∈ Set.Icc t₀ t₁

theorem RS.pathIntegral_segMap {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {a b : Y} {δ : Path a b} {η₂ : Form1 Y} {F : ℝ → ℂ} (hF : IsPrimitiveAlong δ η₂ F) {t₀ t₁ : ℝ} (_h₀ : 0 ≤ t₀) (_h₁ : t₁ ≤ 1) : pathIntegral (Path.segMap δ t₀ t₁) η₂ = F t₁ - F t₀

The integral over an affine segment, computed by a primitive of the whole path.

The trace chain

structure RS.TraceChain {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) {a b : Y} (δ : Path a b) : Type u_2

A Lebesgue-number subdivision of a loop through regular values into pieces inside single (regular-centered) trace charts.

• n : ℕ

  The number of subdivision steps.

• t : ℕ → ℝ

  The subdivision times.

• ht0 : self.t 0 = 0
• ht1 (k : ℕ) : self.n ≤ k → self.t k = 1
• mono : Monotone self.t
• c : ℕ → Y

  The centre of each step's chart.

• hreg (k : ℕ) : IsRegularValue f (self.c k)
• maps (k : ℕ) (u : ℝ) : u ∈ Set.Icc (self.t k) (self.t (k + 1)) → δ.extend u ∈ (traceChart hf hne (self.c k)).source

theorem RS.exists_traceChain {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) {a b : Y} (δ : Path a b) (hδ : ∀ (s : ↑unitInterval), IsRegularValue f (δ s)) : Nonempty (TraceChain hf hne δ)

Existence of a trace chain along any path through regular values.

Assembly: the loop decomposition

theorem RS.TraceChain.t_le {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} {a₀ b₀ : Y} {δ : Path a₀ b₀} (C : TraceChain hf hne δ) (k : ℕ) : C.t k ≤ C.t (k + 1)

theorem RS.TraceChain.t_nonneg {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} {a₀ b₀ : Y} {δ : Path a₀ b₀} (C : TraceChain hf hne δ) (k : ℕ) : 0 ≤ C.t k

theorem RS.TraceChain.t_le_one {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} {a₀ b₀ : Y} {δ : Path a₀ b₀} (C : TraceChain hf hne δ) (k : ℕ) : C.t k ≤ 1

theorem RS.TraceChain.segMap_mem_source {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} {a₀ b₀ : Y} {δ : Path a₀ b₀} (C : TraceChain hf hne δ) (k : ℕ) (s : ↑unitInterval) : (Path.segMap δ (C.t k) (C.t (k + 1))) s ∈ (traceChart hf hne (C.c k)).source

theorem RS.TraceChain.segMap_mem_V {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} {a₀ b₀ : Y} {δ : Path a₀ b₀} (C : TraceChain hf hne δ) (k : ℕ) (s : ↑unitInterval) : (Path.segMap δ (C.t k) (C.t (k + 1))) s ∈ (stackAt hf hne (C.c k)).V

theorem RS.TraceChain.segMap_mem_chart_source {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} {a₀ b₀ : Y} {δ : Path a₀ b₀} (C : TraceChain hf hne δ) (k : ℕ) (s : ↑unitInterval) : (Path.segMap δ (C.t k) (C.t (k + 1))) s ∈ (chartAt ℂ (C.c k)).source

theorem RS.TraceChain.endpoint_mem_V₀ {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} {a₀ b₀ : Y} {δ : Path a₀ b₀} (C : TraceChain hf hne δ) (k : ℕ) : δ.extend (C.t k) ∈ (stackAt hf hne (C.c k)).V

theorem RS.TraceChain.endpoint_mem_V₁ {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} {a₀ b₀ : Y} {δ : Path a₀ b₀} (C : TraceChain hf hne δ) (k : ℕ) : δ.extend (C.t (k + 1)) ∈ (stackAt hf hne (C.c k)).V

noncomputable def RS.TraceChain.sheetPath {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} {a₀ b₀ : Y} {δ : Path a₀ b₀} (C : TraceChain hf hne δ) (k : ℕ) (i : Fin (stackAt hf hne (C.c k)).n) : Path (sectionAt (stackAt hf hne (C.c k)) i (δ.extend (C.t k))) (sectionAt (stackAt hf hne (C.c k)) i (δ.extend (C.t (k + 1))))

The i-th lifted sheet over the k-th piece of the chain.

Equations

• C.sheetPath k i = RS.liftSeg ⋯ (RS.Path.segMap δ (C.t k) (C.t (k + 1))) ⋯

noncomputable def RS.TraceChain.loop {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} {a₀ b₀ : Y} {δ : Path a₀ b₀} (C : TraceChain hf hne δ) (k : ℕ) (i : Fin (stackAt hf hne (C.c k)).n) : Path (Classical.arbitrary X) (Classical.arbitrary X)

The (k, i)-th sheet, closed into a based loop by fixed connecting paths.

Equations

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

theorem RS.TraceChain.pathIntegral_sheetPath {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} {a₀ b₀ : Y} {δ : Path a₀ b₀} (C : TraceChain hf hne δ) (k : ℕ) (i : Fin (stackAt hf hne (C.c k)).n) (η : Form1 X) : pathIntegral (C.sheetPath k i) η = pathIntegral (C.loop k i) η - pathIntegral (PathConnectedSpace.somePath (Classical.arbitrary X) (sectionAt (stackAt hf hne (C.c k)) i (δ.extend (C.t k)))) η + pathIntegral (PathConnectedSpace.somePath (Classical.arbitrary X) (sectionAt (stackAt hf hne (C.c k)) i (δ.extend (C.t (k + 1))))) η

theorem RS.pathIntegral_traceForm_eq_sum_loops {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} {y₀ : Y} {δ : Path y₀ y₀} (C : TraceChain hf hne δ) (η : Form1 X) : pathIntegral δ (traceForm hf hne η) = ∑ k ∈ Finset.range C.n, ∑ i : Fin (stackAt hf hne (C.c k)).n, pathIntegral (C.loop k i) η

The loop decomposition of the trace integral: along a loop through regular values, the integral of Tr_f η is the sum of the based-loop periods of η over the chain's closed sheets (loops independent of η).

theorem RS.periodVector_traceForm_mem {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} {y₀ : Y} (δ : Path y₀ y₀) (hδ : ∀ (s : ↑unitInterval), IsRegularValue f (δ s)) : (fun (i : Fin (genus X)) => pathIntegral δ (traceForm hf hne ((basis X) i))) ∈ periodSubgroup X

Period membership: the trace of the basis period vector along a regular-valued loop lies in the period subgroup of X (exact membership, not just closure).