The homology Cauchy theorem, via Dixon's argument

Dixon's argument in DixonLiouville proves that the glued Dixon function vanishes for a closed null-homologous curve. CauchyIntegralFormula then extracts two algebraic consequences from pointwise vanishing. This file packages the direct null-homologous forms and assembles the summit:

• dixonH2_eq_windingNumber_mul_f_of_nullHomologous — Cauchy's integral formula at an off-curve point of the domain.
• homologyCauchyTheorem_of_point_off_curve — the contour integral of a holomorphic function around such a closed null-homologous curve is zero, assuming an off-curve point in the domain is supplied.
• homologyCauchyTheorem — the homology form of Cauchy's theorem (roadmap homologyCauchyTheorem, TauCetiRoadmap/ContourIntegration/Suggested.lean, Layer 3): for a closed piecewise-C¹ curve γ, null-homologous in an open Ω, and f holomorphic on Ω, the contour integral ∫ t in a..b, deriv γ t • f (γ t) vanishes. The piecewise-C¹ regularity discharges the integrand-level hypotheses via the IsPiecewiseC1On API, and the base point off the curve comes from exists_mem_off_curve.

Provenance

These are the final assembly steps of Dixon's proof, migrated from the AINTLIB LeanModularForms development (DixonTheorem.lean) and restated for the raw curve γ : ℝ → ℂ used by the contour-integration roadmap. See J. D. Dixon, A brief proof of Cauchy's integral theorem, Proc. Amer. Math. Soc. 29 (1971).

theorem TauCeti.Contour.dixonH2_eq_windingNumber_mul_f_of_nullHomologous {f : ℂ → ℂ} {U : Set ℂ} {γ : ℝ → ℂ} {a b : ℝ} {P : Set ℝ} {w : ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b) (hclosed : γ a = γ b) (hP : P.Countable) (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t) (h_null : IsNullHomologous γ a b U) (hwU : w ∈ U) (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ w) : dixonH2 f γ a b w = 2 * ↑Real.pi * Complex.I * windingNumber γ a b w * f w

Null-homologous Cauchy integral formula at an off-curve point. Let γ be a closed curve in an open set U, continuous on uIcc a b, differentiable off a countable set, with interval-integrable derivative, and null-homologous in U. If f is holomorphic on U and w ∈ U is not on the curve, then the Cauchy-type integral evaluates to 2πi · windingNumber γ a b w · f w.

This is the Cauchy-integral-formula output of Dixon's vanishing theorem. The off-curve point is kept as an explicit hypothesis; proving that such a point exists in the ambient domain is a separate geometric prerequisite for the full global homology Cauchy theorem.

theorem TauCeti.Contour.homologyCauchyTheorem_of_point_off_curve {f : ℂ → ℂ} {U : Set ℂ} {γ : ℝ → ℂ} {a b : ℝ} {P : Set ℝ} {w₀ : ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b) (hclosed : γ a = γ b) (hP : P.Countable) (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t) (h_null : IsNullHomologous γ a b U) (hw₀U : w₀ ∈ U) (hw₀off : ∀ t ∈ Set.uIcc a b, γ t ≠ w₀) : ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = 0

Homology Cauchy theorem with a supplied off-curve point. Let γ be a closed curve in an open set U, continuous on uIcc a b, differentiable off a countable set, with interval-integrable derivative, and null-homologous in U. If f is holomorphic on U and U contains a point w₀ not lying on the curve, then ∫ t in a..b, deriv γ t • f (γ t) = 0. The integrand-level form of the homology Cauchy theorem; homologyCauchyTheorem below supplies the off-curve point and discharges the regularity from IsPiecewiseC1On.

theorem TauCeti.Contour.homologyCauchyTheorem {f : ℂ → ℂ} {Ω : Set ℂ} (hΩ : IsOpen Ω) (γ : ℝ → ℂ) (a b : ℝ) (hγ_pc1 : IsPiecewiseC1On γ a b) (hγ : ∀ t ∈ Set.uIcc a b, γ t ∈ Ω) (hclosed : γ a = γ b) (hf : DifferentiableOn ℂ f Ω) (hnull : IsNullHomologous γ a b Ω) : ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = 0

The homology Cauchy theorem (roadmap homologyCauchyTheorem, Layer 3). Let γ be a closed piecewise-C¹ curve on [[a, b]], null-homologous in an open set Ω containing it, and let f be holomorphic on Ω. Then the contour integral of f along γ vanishes: ∫ t in a..b, deriv γ t • f (γ t) = 0.

Dixon's argument: the piecewise-C¹ regularity supplies continuity, differentiability off the finitely many breakpoints, and interval-integrability of deriv γ (the IsPiecewiseC1On API); the compact curve image cannot exhaust the open Ω, giving a base point w₀ ∈ Ω off the curve (exists_mem_off_curve); and homologyCauchyTheorem_of_point_off_curve — vanishing of the glued Dixon function by Liouville, then the Cauchy integral formula at w₀ — concludes.