The bridge to honest integrals (CC6)

Unit: paths-and-integrals (docs/design/paths-and-integrals.md §4). On a path contained in a single chart, pathIntegral is the classical interval integral of the chart coefficient against the derivative of the chart composite (single-chart, C¹ bridge). Also: the continuous-path FTC ∫_γ df = f(y) - f(x) for holomorphic f.

Ownership decision (design §4): this unit proves the abstract single-chart C¹ bridge only; circleIntegral/curveIntegral specializations belong to residue-calculus / planar-stokes-atoms.

Main declarations:

• RS.pathIntegral_eq_intervalIntegral — the single-chart bridge.
• RS.pathIntegral_mdifferential — FTC along a continuous path for d f.

theorem RS.pathIntegral_eq_intervalIntegral {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} {γ : Path x y} {η : Form1 X} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hγ : Set.range ⇑γ ⊆ e.source) {u' : ℝ → ℂ} (hu : ∀ t ∈ Set.Icc 0 1, HasDerivWithinAt (fun (s : ℝ) => ↑e (γ.extend s)) (u' t) (Set.Icc 0 1) t) (hu' : ContinuousOn u' (Set.Icc 0 1)) : pathIntegral γ η = ∫ (t : ℝ) in 0..1, coeffIn e η (↑e (γ.extend t)) * u' t

On a path contained in a single chart, pathIntegral is the classical integral ∫ coeff · (chart∘γ)'.

theorem RS.pathIntegral_mdifferential {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} {f : X → ℂ} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (γ : Path x y) : pathIntegral γ (mdifferential f hf) = f y - f x

FTC along a path: ∫_γ df = f(end) − f(start) (Forster 10.2, continuous-path version).