The in-chart segment path (shared helper for §6.3/§6.5)

Unit: period-lattice-rank. The straight-segment path inside a chart-ball, pulled back through the chart: used by both Nondegeneracy.lean (§5.1 step 2) and Discreteness.lean (Stage C.2) to compute a path integral of η as the difference of a local primitive's values. Factored out once since both sites need exactly the same construction (design §6.5's segmentPath note).

Main declarations: RS.segmentPath, RS.pathIntegral_segmentPath.

noncomputable def RS.segmentPath {X : Type u_1} [TopologicalSpace X] {e : OpenPartialHomeomorph X ℂ} {c : ℂ} {r : ℝ} (hballsub : Metric.ball c r ⊆ e.target) {p q : X} (hp_src : p ∈ e.source) (hq_src : q ∈ e.source) (hp : ↑e p ∈ Metric.ball c r) (hq : ↑e q ∈ Metric.ball c r) : Path p q

The straight segment from e p to e q inside ball c r ⊆ e.target, pulled back through the chart e — a genuine continuous path p ⤳ q (the whole segment stays inside the ball by convexity, where e.symm is continuous). Needs p, q inside the chart's source so the endpoints come out right.

Equations

• RS.segmentPath hballsub hp_src hq_src hp hq = { toFun := fun (t : ↑unitInterval) => ↑e.symm ((AffineMap.lineMap (↑e p) (↑e q)) ↑t), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

theorem RS.pathIntegral_segmentPath {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {η : Form1 X} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {c : ℂ} {r : ℝ} (hballsub : Metric.ball c r ⊆ e.target) {p q : X} (hp_src : p ∈ e.source) (hq_src : q ∈ e.source) (hp : ↑e p ∈ Metric.ball c r) (hq : ↑e q ∈ Metric.ball c r) {g : ℂ → ℂ} (hg : ∀ z ∈ Metric.ball c r, HasDerivAt g (coeffIn e η z) z) : pathIntegral (segmentPath hballsub hp_src hq_src hp hq) η = g (↑e q) - g (↑e p)

The path integral of η along segmentPath is the difference of a local primitive's values, via the constant-chart cell primitive (isPrimitiveAlongMap_of_ball) and well-definedness (IsPrimitiveAlong.pathIntegral_eq).