7.6. Path.LoopOffBranch🔗

Jacobians.Path.LoopOffBranch — source

chartFrame_cancel_general

General chart-frame cancellation. For any path γ that stays in the chart source of Q₀ on a neighbourhood of t, and is chart-pullback-differentiable at t, the lineIntegral integrand of the i-th period basis form factors through the chart e := chartAt ℂ Q₀:

ωᵢ(γ t)(pathSpeed γ t) = chartFormCoeff Q₀ i (e (γ t)) · (fderiv ℝ (e ∘ γ) t 1).

This is OfCurveSkeleton.chartFrame_cancel generalised from ChartBallPath to an arbitrary path: the proof is the same chart-transition + ℂ-linearity computation, with the ChartBallPath-specific chart_ChartBallPath_eq step replaced by the local equality e ∘ γ (the chart coordinate) directly.

lemma chartFrame_cancel_general {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (Q₀ : X) (γ : ℝ → X)
    (i : Fin (genus X)) (t : ℝ)
    (h_source_nbhd : ∀ᶠ s : ℝ in nhds t, γ s ∈ (chartAt (H := ℂ) Q₀).source)
    (hγ_diff : DifferentiableAt ℝ ((chartAt (H := ℂ) Q₀).toFun ∘ γ) t) :
    (periodBasisForm X i).toFun (γ t) (pathSpeed γ t) =
      chartFormCoeff (X := X) Q₀ i ((chartAt (H := ℂ) Q₀) (γ t))
        * (fderiv ℝ ((chartAt (H := ℂ) Q₀).toFun ∘ γ) t 1)

intervalIntegral_form_pathSpeed_eq_primitive_diff_of_primitive

Sub-interval primitive-difference, with a GIVEN primitive F. Identical to intervalIntegral_form_pathSpeed_eq_primitive_diff_in_subball, but F (a primitive of chartFormCoeff Q₀ i on the ball) is *supplied as input* rather than produced existentially. This is what lets a *single* ball-k primitive F be reused across several confined paths (the original loop, the detour, and the connecting paths) so that their primitive-differences telescope — the line integral over each confined path is F(chart endpoint) − F(chart start) with the SAME F.

lemma intervalIntegral_form_pathSpeed_eq_primitive_diff_of_primitive {X : Type*}
    [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (Q₀ : X) (γ : ℝ → X) (i : Fin (genus X)) (c : ℂ) (r : ℝ) (a b : ℝ)
    (F : ℂ → ℂ) (hF : ∀ w ∈ Metric.ball c r, HasDerivAt F (chartFormCoeff (X := X) Q₀ i w) w)
    (hg_ball : ∀ t ∈ Set.uIcc a b, (chartAt (H := ℂ) Q₀) (γ t) ∈ Metric.ball c r)
    (hγ_in : ∀ t ∈ Set.uIcc a b, γ t ∈ (chartAt (H := ℂ) Q₀).source)
    (hγ_cont : Continuous γ)
    (hγ_diff : ∀ t ∈ Set.uIcc a b,
      DifferentiableAt ℝ ((chartAt (H := ℂ) Q₀).toFun ∘ γ) t)
    (hint : IntervalIntegrable
      (fun t => (periodBasisForm X i).toFun (γ t) (pathSpeed γ t)) volume a b) :
    (∫ t in a..b, (periodBasisForm X i).toFun (γ t) (pathSpeed γ t)) =
      F ((chartAt (H := ℂ) Q₀) (γ b)) - F ((chartAt (H := ℂ) Q₀) (γ a))

exists_relay_dodge_finite

Two-segment planar dodge, ball-confined. For a finite B ⊆ ℂ, an open ball and two points p, q of the ball off B, a relay m in the ball exists with [p,m] and [m,q] inside the ball and disjoint from B.

The argument is the ball-confined version of Mathlib's Set.Countable.isPathConnected_compl_of_one_lt_rank: writing p = cm - x, q = cm + x with cm the midpoint, pick a relay direction y linearly independent from x; the pencils of segments from p (resp. q) to cm + t·y are pairwise disjoint off their common vertex, so only countably many t let a segment meet the (countable) B. The midpoint cm lies in the convex ball, so a whole neighborhood of t = 0 keeps cm + t·y in the ball; intersecting with the cofinite good set (dense complement) yields a valid t.

lemma exists_relay_dodge_finite (B : Set ℂ) (hB : B.Finite) (c : ℂ) (r : ℝ)
    (p q : ℂ) (hp : p ∈ Metric.ball c r) (hq : q ∈ Metric.ball c r)
    (hpB : p ∉ B) (hqB : q ∉ B) :
    ∃ m ∈ Metric.ball c r,
      segment ℝ p m ⊆ Metric.ball c r ∧ segment ℝ m q ⊆ Metric.ball c r ∧
      Disjoint (segment ℝ p m) B ∧ Disjoint (segment ℝ m q) B

ChartBallPathSmooth3

Flat-ended chart-linear path P → Q in the chart at anchor w (smoothStep-reparametrized so both endpoint velocities vanish).

noncomputable def ChartBallPathSmooth3 {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (w P Q : X) : ℝ → X

ChartBallPathSmooth3_zero

ChartBallPathSmooth3 w P Q 0 = P when P is in the anchor chart's source.

@[simp] lemma ChartBallPathSmooth3_zero {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (w P Q : X) (hP : P ∈ (chartAt (H := ℂ) w).source) :
    ChartBallPathSmooth3 w P Q 0 = P

ChartBallPathSmooth3_one

ChartBallPathSmooth3 w P Q 1 = Q when Q is in the anchor chart's source.

@[simp] lemma ChartBallPathSmooth3_one {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (w P Q : X) (hQ : Q ∈ (chartAt (H := ℂ) w).source) :
    ChartBallPathSmooth3 w P Q 1 = Q

chart_ChartBallPathSmooth3_eq

The chart-w pullback of ChartBallPathSmooth3 w P Q is the affine interpolation reparametrized by smoothStep01 — used to read off the chart-coordinate endpoints for the splice.

lemma chart_ChartBallPathSmooth3_eq {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [ConnectedSpace X] (w P Q : X) (t : ℝ)
    (h_in_target : ((1 - (Jacobians.smoothStep01 t : ℂ)) * (chartAt (H := ℂ) w) P +
      (Jacobians.smoothStep01 t : ℂ) * (chartAt (H := ℂ) w) Q) ∈ (chartAt (H := ℂ) w).target) :
    (chartAt (H := ℂ) w) (ChartBallPathSmooth3 w P Q t) =
      (1 - (Jacobians.smoothStep01 t : ℂ)) * (chartAt (H := ℂ) w) P +
        (Jacobians.smoothStep01 t : ℂ) * (chartAt (H := ℂ) w) Q

ChartBallPathSmooth3_mem_source

ChartBallPathSmooth3 w P Q stays in the anchor chart source on [0,1] under the chart-ball hypothesis.

lemma ChartBallPathSmooth3_mem_source {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [ConnectedSpace X] (w P Q : X) (t : ℝ)
    (h_chart_ball : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (s : ℂ)) * (chartAt (H := ℂ) w) P + (s : ℂ) * (chartAt (H := ℂ) w) Q)
        ∈ (chartAt (H := ℂ) w).target) :
    ChartBallPathSmooth3 w P Q t ∈ (chartAt (H := ℂ) w).source

ChartBallPathSmooth3_continuous

Continuity of ChartBallPathSmooth3 w P Q under the chart-ball hypothesis on [0,1].

lemma ChartBallPathSmooth3_continuous {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X] (w P Q : X)
    (h_chart_ball : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (s : ℂ)) * (chartAt (H := ℂ) w) P + (s : ℂ) * (chartAt (H := ℂ) w) Q)
        ∈ (chartAt (H := ℂ) w).target) :
    Continuous (ChartBallPathSmooth3 w P Q)

ChartBallPathSmooth3_chart_at_differentiableAt

Moving-frame chart-pullback differentiability of ChartBallPathSmooth3 (the IsSmoothPath.diff field). Chain rule on (general-anchor ChartBallPath chart-pullback) ∘ smoothStep01.

lemma ChartBallPathSmooth3_chart_at_differentiableAt {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X] (w P Q : X) (t : ℝ)
    (h_chart_ball : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (s : ℂ)) * (chartAt (H := ℂ) w) P + (s : ℂ) * (chartAt (H := ℂ) w) Q)
        ∈ (chartAt (H := ℂ) w).target) :
    DifferentiableAt ℝ
      ((chartAt (H := ℂ) (ChartBallPathSmooth3 w P Q t)).toFun ∘ ChartBallPathSmooth3 w P Q) t

ChartBallPathSmooth3_velCont

Velocity-section continuity of ChartBallPathSmooth3 (the IsSmoothPath.velCont field). The path is (chartAt w).symm ∘ β with β the smoothStep-reparametrized affine chart-coord curve; push the model-space velocity continuity through the holomorphic chart inverse via velCont_compOn.

lemma ChartBallPathSmooth3_velCont {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (w P Q : X)
    (h_chart_ball : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (s : ℂ)) * (chartAt (H := ℂ) w) P + (s : ℂ) * (chartAt (H := ℂ) w) Q)
        ∈ (chartAt (H := ℂ) w).target) :
    ContinuousOn (fun s : ℝ =>
        Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := X))
          (ChartBallPathSmooth3 w P Q s) (Jacobians.pathSpeed (ChartBallPathSmooth3 w P Q) s))
      (Set.Icc 0 1)

isSmoothPath_ChartBallPathSmooth3

IsSmoothPath for the general-anchor flat-ended chart path. Assembled from the fields above; this is the per-piece building block of the off-branch detour.

lemma isSmoothPath_ChartBallPathSmooth3 {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (w P Q : X)
    (hP : P ∈ (chartAt (H := ℂ) w).source) (hQ : Q ∈ (chartAt (H := ℂ) w).source)
    (h_chart_ball : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (s : ℂ)) * (chartAt (H := ℂ) w) P + (s : ℂ) * (chartAt (H := ℂ) w) Q)
        ∈ (chartAt (H := ℂ) w).target) :
    Jacobians.IsSmoothPath P Q (ChartBallPathSmooth3 w P Q)

pathSpeed_ChartBallPathSmooth3_zero

Endpoint velocities of ChartBallPathSmooth3 vanish (smoothStep chain rule, as in A1).

lemma pathSpeed_ChartBallPathSmooth3_zero {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (w P Q : X)
    (h_chart_ball : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (s : ℂ)) * (chartAt (H := ℂ) w) P + (s : ℂ) * (chartAt (H := ℂ) w) Q)
        ∈ (chartAt (H := ℂ) w).target) :
    Jacobians.pathSpeed (ChartBallPathSmooth3 w P Q) 0 = 0

pathSpeed_ChartBallPathSmooth3_one

lemma pathSpeed_ChartBallPathSmooth3_one {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (w P Q : X)
    (h_chart_ball : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (s : ℂ)) * (chartAt (H := ℂ) w) P + (s : ℂ) * (chartAt (H := ℂ) w) Q)
        ∈ (chartAt (H := ℂ) w).target) :
    Jacobians.pathSpeed (ChartBallPathSmooth3 w P Q) 1 = 0

balancedGlue

Balanced binary concatenation of 2^d paths g 0, …, g (2^d-1) (split always at the midpoint, so pieces land on uniform dyadic sub-intervals).

noncomputable def balancedGlue {X : Type*} (g : ℕ → ℝ → X) : ℕ → ℝ → X
  | 0 => g 0
  | (d+1) => Jacobians.concat (balancedGlue g d) (balancedGlue (fun k => g (2^d + k)) d)
/-! ### A4'. Uniform `n`-piece glue
For the off-branch surgery the detour pieces must occupy the **uniform** sub-intervals
`[k/n,(k+1)/n]`
handed by `exists_subBallChartCover`, so the dyadic `balancedGlue` is not directly usable.
`uniformGlue g n` glues the `n` flat-ended pieces `g 0, …, g (n-1)` at the uniform breakpoints
`k/n`,
reading off the value on the `k`-th piece as `g k` affinely reparametrized by `t ↦ n·t − k`.
`uIdx n t = min ⌊n·t⌋₊-clamped (n-1)` is the piece index; the glue is the closed form
`g (uIdx n t) (n·t − uIdx n t)`. Every piece is flat-ended (zero endpoint velocity) and consecutive
pieces chain (`g k 1 = g (k+1) 0`), so each seam `t = k/n` is `C¹` for free — the same
`HasDerivWithinAt … 0` union argument as `IsSmoothPath.concat`, with split point `k/n` and
scale `n`.
-/
/-- **Moving-chart to fixed-anchor differentiability transfer.** If `γ` is continuous, `γ t` lies in
the source of a fixed anchor chart `chartAt Q₀`, and `γ` is chart-pullback-differentiable at `t` in
its own moving chart `chartAt (γ t)`, then it is also chart-pullback-differentiable in the fixed
anchor chart. (Composition with the smooth chart-transition `chartAt Q₀ ∘ (chartAt (γ t)).symm`.) -/

differentiableAt_chart_anchor_of_self

Moving-chart to fixed-anchor differentiability transfer. If γ is continuous, γ t lies in the source of a fixed anchor chart chartAt Q₀, and γ is chart-pullback-differentiable at t in its own moving chart chartAt (γ t), then it is also chart-pullback-differentiable in the fixed anchor chart. (Composition with the smooth chart-transition chartAt Q₀ ∘ (chartAt (γ t)).symm.)

lemma differentiableAt_chart_anchor_of_self {X : Type*} [TopologicalSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (Q₀ : X) (γ : ℝ → X) (t : ℝ)
    (hγcont : Continuous γ)
    (hmem : γ t ∈ (chartAt (H := ℂ) Q₀).source)
    (hdiff : DifferentiableAt ℝ ((chartAt (H := ℂ) (γ t)).toFun ∘ γ) t) :
    DifferentiableAt ℝ ((chartAt (H := ℂ) Q₀).toFun ∘ γ) t

uIdx

Piece index of t among n uniform sub-intervals of [0,1], clamped to [0, n-1].

noncomputable def uIdx (n : ℕ) (t : ℝ) : ℕ

uniformGlue

Uniform n-piece glue of g 0, …, g (n-1): on [k/n,(k+1)/n] it is g k (n·t − k).

noncomputable def uniformGlue {X : Type*} (g : ℕ → ℝ → X) (n : ℕ) : ℝ → X

uIdx_eq

Piece index on the half-open k-th sub-interval. For k < n and t ∈ [k/n, (k+1)/n), uIdx n t = k.

lemma uIdx_eq (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : k < n) (t : ℝ)
    (h0 : (k:ℝ)/n ≤ t) (h1 : t < ((k:ℝ)+1)/n) : uIdx n t = k

uIdx_one

Piece index at the right endpoint t = 1. uIdx n 1 = n - 1.

lemma uIdx_one (n : ℕ) (hn : 0 < n) : uIdx n 1 = n - 1

uIdx_zero_of_nonpos

Piece index left of the loop (t ≤ 0): uIdx n t = 0.

lemma uIdx_zero_of_nonpos (n : ℕ) (t : ℝ) (ht : t ≤ 0) : uIdx n t = 0

uIdx_last_of_ge_one

Piece index right of the loop (t ≥ 1): uIdx n t = n - 1.

lemma uIdx_last_of_ge_one (n : ℕ) (hn : 0 < n) (t : ℝ) (ht : 1 ≤ t) : uIdx n t = n - 1

uniformGlue_apply_of_mem

Value of the uniform glue on the closed k-th sub-interval (for k < n, with the right endpoint resolved by chaining g k 1 = g (k+1) 0).

lemma uniformGlue_apply_of_mem {X : Type*} (g : ℕ → ℝ → X) (hchain : ∀ j, g j 1 = g (j+1) 0)
    (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : k < n) (t : ℝ)
    (h0 : (k:ℝ)/n ≤ t) (h1 : t ≤ ((k:ℝ)+1)/n) :
    uniformGlue g n t = g k ((n:ℝ) * t - k)

pathSpeed_affine_comp

General affine-reparametrization pathSpeed. pathSpeed (s ↦ γ (a·s+b)) t = a · pathSpeed γ (a·t+b), given the chart-pullback of γ is differentiable at a·t+b. The general-(a,b) analogue of pathSpeed_concat_left/right (a=2), used at uniform-glue seams (a=n).

lemma pathSpeed_affine_comp {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (γ : ℝ → X)
    (a b t : ℝ)
    (hdiff : DifferentiableAt ℝ ((chartAt (H := ℂ) (γ (a*t+b))).toFun ∘ γ) (a*t+b)) :
    Jacobians.pathSpeed (fun s => γ (a*s+b)) t = (a:ℂ) * Jacobians.pathSpeed γ (a*t+b)

uniformGlue_eqOn_piece

uniformGlue g n agrees with the affine reparametrization s ↦ g k (n·s − k) of piece k on the closed k-th sub-interval [k/n,(k+1)/n].

lemma uniformGlue_eqOn_piece {X : Type*} (g : ℕ → ℝ → X) (hchain : ∀ j, g j 1 = g (j+1) 0)
    (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : k < n) :
    Set.EqOn (uniformGlue g n) (fun s => g k ((n:ℝ) * s - k))
      (Set.Icc ((k:ℝ)/n) (((k:ℝ)+1)/n))

uniformGlue_eventuallyEq_piece

On the open k-th sub-interval, the glue locally equals the affine reparam of piece k.

lemma uniformGlue_eventuallyEq_piece {X : Type*} (g : ℕ → ℝ → X) (n : ℕ) (hn : 0 < n) (k : ℕ)
    (hk : k < n)
    (t : ℝ) (ht : t ∈ Set.Ioo ((k:ℝ)/n) (((k:ℝ)+1)/n)) :
    uniformGlue g n =ᶠ[nhds t] (fun s => g k ((n:ℝ)*s - k))

uniformGlue_seam

Seam C¹-junction of the uniform glue. At an interior breakpoint t₀ = j/n (0 < j < n) the glue's chart-pullback has derivative 0: both adjacent pieces are flat-ended, so each one-sided HasDerivWithinAt is 0, and the two Icc halves union to a neighborhood.

lemma uniformGlue_seam {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (g : ℕ → ℝ → X) (hchain : ∀ j, g j 1 = g (j+1) 0) (n : ℕ) (hn : 0 < n)
    (hpiece : ∀ k, k < n → Jacobians.IsSmoothPath (g k 0) (g k 1) (g k))
    (hv0 : ∀ k, k < n → Jacobians.pathSpeed (g k) 0 = 0)
    (hv1 : ∀ k, k < n → Jacobians.pathSpeed (g k) 1 = 0)
    (j : ℕ) (hj1 : 1 ≤ j) (hjn : j ≤ n - 1) (t₀ : ℝ) (ht₀ : (n:ℝ) * t₀ = j) :
    HasDerivAt ((chartAt (H := ℂ) (uniformGlue g n t₀)).toFun ∘ uniformGlue g n) 0 t₀

uniformGlue_eventuallyEq_zero

Near t = 0 the glue equals the affine reparam of piece 0 (clamped index).

lemma uniformGlue_eventuallyEq_zero {X : Type*} (g : ℕ → ℝ → X) (n : ℕ) (hn : 0 < n) :
    uniformGlue g n =ᶠ[nhds 0] (fun s => g 0 ((n:ℝ)*s - (0:ℕ)))

uniformGlue_eventuallyEq_one

Near t = 1 the glue equals the affine reparam of the last piece (clamped index).

lemma uniformGlue_eventuallyEq_one {X : Type*} (g : ℕ → ℝ → X) (n : ℕ) (hn : 0 < n) :
    uniformGlue g n =ᶠ[nhds 1] (fun s => g (n-1) ((n:ℝ)*s - (n-1:ℕ)))

pathSpeed_congr_nhds

pathSpeed is local: it agrees on functions equal near the point.

lemma pathSpeed_congr_nhds {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (γ γ' : ℝ → X)
    (t : ℝ) (h : γ =ᶠ[nhds t] γ') :
    Jacobians.pathSpeed γ t = Jacobians.pathSpeed γ' t

piece_pathSpeed_eq

The affine reparam of piece k has pathSpeed n · (pathSpeed of piece k at the rescaled arg).

lemma piece_pathSpeed_eq {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (g : ℕ → ℝ → X) (n : ℕ) (_hn : 0 < n)
    (hpiece : ∀ k, k < n → Jacobians.IsSmoothPath (g k 0) (g k 1) (g k))
    (k : ℕ) (hk : k < n) (s : ℝ) (hsmem : (n:ℝ)*s - k ∈ Icc (0:ℝ) 1) :
    Jacobians.pathSpeed (fun u => g k ((n:ℝ)*u - k)) s
      = (n:ℂ) * Jacobians.pathSpeed (g k) ((n:ℝ)*s - k)

uniformGlue_pathSpeed_eqOn_piece

The glue's pathSpeed equals the affine-reparam piece's pathSpeed on the closed k-th piece. On the open interior via locality; at the two endpoints both vanish (flat-ended seams / boundaries).

lemma uniformGlue_pathSpeed_eqOn_piece {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (g : ℕ → ℝ → X) (hchain : ∀ j, g j 1 = g (j+1) 0)
    (n : ℕ) (hn : 0 < n)
    (hpiece : ∀ k, k < n → Jacobians.IsSmoothPath (g k 0) (g k 1) (g k))
    (hv0 : ∀ k, k < n → Jacobians.pathSpeed (g k) 0 = 0)
    (hv1 : ∀ k, k < n → Jacobians.pathSpeed (g k) 1 = 0)
    (k : ℕ) (hk : k < n) :
    ∀ s ∈ Icc ((k:ℝ)/n) (((k:ℝ)+1)/n),
      Jacobians.pathSpeed (uniformGlue g n) s
        = Jacobians.pathSpeed (fun u => g k ((n:ℝ)*u - k)) s

isSmoothPath_uniformGlue

The uniform glue is a flat-ended smooth path. Given each piece g k (k < n) is an IsSmoothPath (g k 0) (g k 1) with vanishing endpoint velocities, and consecutive pieces chain, uniformGlue g n is an IsSmoothPath (g 0 0) (g (n-1) 1): continuity and velocity-continuity glue over the closed uniform cover via the affine-reparam machinery; chart-pullback differentiability is the per-point chain rule on open pieces, and the HasDerivWithinAt … 0 union at each seam (every piece flat-ended ⇒ both one-sided seam derivatives vanish).

lemma isSmoothPath_uniformGlue {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (g : ℕ → ℝ → X)
    (hchain : ∀ j, g j 1 = g (j+1) 0) (n : ℕ) (hn : 0 < n)
    (hpiece : ∀ k, k < n → Jacobians.IsSmoothPath (g k 0) (g k 1) (g k))
    (hv0 : ∀ k, k < n → Jacobians.pathSpeed (g k) 0 = 0)
    (hv1 : ∀ k, k < n → Jacobians.pathSpeed (g k) 1 = 0) :
    Jacobians.IsSmoothPath (g 0 0) (g (n-1) 1) (uniformGlue g n)

exists_subBallChartCover

Sub-ball chart cover. For a continuous γ : ℝ → X, there is a uniform partition into n pieces with, per piece k, a chart anchor x k, a center c k and radius r k > 0 such that Metric.ball (c k) (r k) ⊆ (chartAt ℂ (x k)).target, and for every s in the k-th piece [k/n, (k+1)/n] the point γ s lies in (chartAt ℂ (x k)).source with chart-image chartAt ℂ (x k) (γ s) ∈ Metric.ball (c k) (r k). This supplies the sub-ball confinement consumed by intervalIntegral_form_pathSpeed_eq_of_subball_endpoints.

theorem exists_subBallChartCover {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (γ : ℝ → X)
    (hγ : Continuous γ) :
    ∃ (n : ℕ) (_hn : 0 < n) (x : Fin n → X) (c : Fin n → ℂ) (r : Fin n → ℝ),
      (∀ k, 0 < r k) ∧
      ∀ (k : Fin n) (s : ℝ),
        (k : ℝ) / n ≤ s → s ≤ ((k : ℝ) + 1) / n →
          Metric.ball (c k) (r k) ⊆ (chartAt (H := ℂ) (x k)).target ∧
          γ s ∈ (chartAt (H := ℂ) (x k)).source ∧
          (chartAt (H := ℂ) (x k)) (γ s) ∈ Metric.ball (c k) (r k)

periodVec_eq_of_partition_integral_telescope

Period-vector telescoping with a per-piece correction term. Generalizes periodVec_eq_of_partition_integral_eq: instead of demanding the partial line integrals agree piece-by-piece, we allow a *correction* corr i : ℕ → ℂ so that on piece k ∫δ' = ∫δ + corr (k+1) − corr k. If the correction is periodic (corr i n = corr i 0) the correction terms telescope to corr i n − corr i 0 = 0, so periodVec δ' = periodVec δ.

This is the analytic core of period-preservation for the off-branch surgery once the breakpoints are *perturbed* (so the per-piece integrals no longer match exactly): corr i k is the intrinsic line integral of the period form along the short connecting path from δ(k/n) to the perturbed off-branch breakpoint p k. Because that connector lies in the overlap of the two adjacent sub-balls, the same corr i k value serves both piece k−1 (its right end) and piece k (its left end), and periodicity corr i n = corr i 0 holds because breakpoint n *is* breakpoint 0 (δ 1 = δ 0, p n = p 0).

theorem periodVec_eq_of_partition_integral_telescope (δ δ' : ℝ → X)
    (hδ : IsClosedSmoothLoop δ) (hδ' : IsClosedSmoothLoop δ')
    (s : ℕ → ℝ) (n : ℕ) (hs0 : s 0 = 0) (hsn : s n = 1)
    (hs_sub : ∀ k, k < n → Set.uIcc (s k) (s (k+1)) ⊆ Set.Icc (0:ℝ) 1)
    (corr : Fin (genus X) → ℕ → ℂ) (hcorr_per : ∀ i, corr i n = corr i 0)
    (hpiece : ∀ (i : Fin (genus X)) (k : ℕ), k < n →
      (∫ t in (s k)..(s (k+1)), (periodBasisForm X i).toFun (δ' t) (pathSpeed δ' t)) =
      (∫ t in (s k)..(s (k+1)), (periodBasisForm X i).toFun (δ t) (pathSpeed δ t))
        + corr i (k+1) - corr i k) :
    periodVec δ' = periodVec δ