Gauge-chain and Bochner curve integrals

When the circulation integrand is genuinely Bochner integrable on every supported arc, the sum of the two gauge coordinate integrals agrees with the integer-weighted sum of Mathlib's existing curveIntegral. Gauge integrability of the individual coordinates is retained, so no conditional gauge value is replaced by a junk-valued Bochner integral.

theorem TauCeti.Green.BoundaryChain.integral_add_eq_curveIntegral {P Q : ℂ → ℝ} {c : BoundaryChain} (hP : Integrable Complex.reCLM P c) (hQ : Integrable Complex.imCLM Q c) (hc : ∀ γ ∈ c.support, IntervalIntegrable (circulationFun P Q ⇑γ.snd.snd.extend) MeasureTheory.volume 0 1) : (integral Complex.reCLM P) c + (integral Complex.imCLM Q) c = (Finsupp.linearCombination ℤ fun (γ : Arc) => curveIntegral (oneForm P Q) γ.snd.snd) c

Genuine arcwise Bochner integrability identifies gauge circulation with the sum of Mathlib curve integrals, even when only the combined circulation is Bochner integrable.