Finite graph-piece boundary arcs

A geometric certificate permits finitely many coordinate graph pieces, joined as actual paths. Continuous coordinate primitives prove gauge integrability and additivity even when the graph speed is unbounded and the coordinate integrand is only conditionally integrable.

structure TauCeti.Green.BoundaryChain.RegularReparam {p q : ℂ} (θ : ℝ → ℝ) (γ δ : Path p q) : Prop

Regular path reparametrization: countable fibers preserve exceptional-set countability, and fixed endpoints preserve orientation.

• continuousOn : ContinuousOn θ (Set.Icc 0 1)

  Continuity on the parameter interval.

• differentiable : ∃ (s : Set ℝ), s.Countable ∧ ∀ t ∈ Set.Ioo 0 1 \ s, DifferentiableAt ℝ θ t

  Differentiability away from a countable set.

• differentiable_path : ∃ (s : Set ℝ), s.Countable ∧ ∀ t ∈ Set.Ioo 0 1 \ s, DifferentiableAt ℝ (⇑δ.extend) t

  Regularity of the original extended path.

• countable_fibers (t : ℝ) : (θ ⁻¹' {t}).Countable

  Fibers of the parameter map are countable.

• mapsTo : Set.MapsTo θ (Set.Icc 0 1) (Set.Icc 0 1)

  Parameters stay in the path interval.

• map_zero : θ 0 = 0

  The initial parameter is preserved.

• map_one : θ 1 = 1

  The final parameter is preserved.

• path_eq (t : ↑unitInterval) : γ t = δ.extend (θ ↑t)

  The new path follows the old path through the parameter map.

inductive TauCeti.Green.BoundaryChain.PiecewiseGraphArc (d : Coordinate) (U : Set ℂ) : Arc → Prop

A finite graph-piece presentation of an actual path, including ignored constant-coordinate pieces. These certificates contain no integral identities or field assumptions.

• constant {d : Coordinate} {U : Set ℂ} {p q : ℂ} (γ : Path p q) (hγ : ∀ (t : ↑unitInterval), d.proj (γ t) = d.proj p) : PiecewiseGraphArc d U ⟨p, ⟨q, γ⟩⟩
• graph {d : Coordinate} {U : Set ℂ} {g : ℝ → ℝ} {a b : ℝ} {γ : Arc} (hγ : GraphArc d g a b γ) (hU : d.graph g '' Set.Icc a b ⊆ U) : PiecewiseGraphArc d U γ
• trans {d : Coordinate} {U : Set ℂ} {p q r : ℂ} {γ : Path p q} {δ : Path q r} (hγ : PiecewiseGraphArc d U ⟨p, ⟨q, γ⟩⟩) (hδ : PiecewiseGraphArc d U ⟨q, ⟨r, δ⟩⟩) : PiecewiseGraphArc d U ⟨p, ⟨r, γ.trans δ⟩⟩
• symm {d : Coordinate} {U : Set ℂ} {p q : ℂ} {γ : Path p q} (hγ : PiecewiseGraphArc d U ⟨p, ⟨q, γ⟩⟩) : PiecewiseGraphArc d U ⟨q, ⟨p, γ.symm⟩⟩
• reparam {d : Coordinate} {U : Set ℂ} {p q : ℂ} {γ δ : Path p q} (hδ : PiecewiseGraphArc d U ⟨p, ⟨q, δ⟩⟩) (θ : ℝ → ℝ) (h : RegularReparam θ γ δ) : PiecewiseGraphArc d U ⟨p, ⟨q, γ⟩⟩

theorem TauCeti.Green.BoundaryChain.PiecewiseGraphArc.integrable {d : Coordinate} {U : Set ℂ} {γ : Arc} (h : PiecewiseGraphArc d U γ) {P : ℂ → ℝ} (hP : ContinuousOn P U) : Integrable d.proj P (ofPath γ.snd.snd)

Every finite graph-piece path is genuinely Henstock integrable in its selected coordinate, with no Bochner integrability or absolute-continuity premise.

theorem TauCeti.Green.BoundaryChain.PiecewiseGraphArc.arcIntegral_trans {d : Coordinate} {U : Set ℂ} {p q r : ℂ} {γ : Path p q} {δ : Path q r} (hγ : PiecewiseGraphArc d U ⟨p, ⟨q, γ⟩⟩) (hδ : PiecewiseGraphArc d U ⟨q, ⟨r, δ⟩⟩) {P : ℂ → ℝ} (hP : ContinuousOn P U) : arcIntegral d.proj P ⟨p, ⟨r, γ.trans δ⟩⟩ = arcIntegral d.proj P ⟨p, ⟨q, γ⟩⟩ + arcIntegral d.proj P ⟨q, ⟨r, δ⟩⟩

The actual joined path integral is the sum of its finite graph-piece integrals. This is gauge additivity, including conditional integrability and arbitrary graph backtracking.

theorem TauCeti.Green.BoundaryChain.PiecewiseGraphArc.arcIntegral_reparam {d : Coordinate} {U : Set ℂ} {p q : ℂ} {γ δ : Path p q} (hδ : PiecewiseGraphArc d U ⟨p, ⟨q, δ⟩⟩) {θ : ℝ → ℝ} (h : RegularReparam θ γ δ) {P : ℂ → ℝ} (hP : ContinuousOn P U) : arcIntegral d.proj P ⟨p, ⟨q, γ⟩⟩ = arcIntegral d.proj P ⟨p, ⟨q, δ⟩⟩

A countable-fiber regular change of parameter preserves the gauge integral of a finite piecewise graph path. Endpoint preservation fixes its orientation.

theorem TauCeti.Green.BoundaryChain.PiecewiseGraphArc.arcIntegral_symm {d : Coordinate} {U : Set ℂ} {p q : ℂ} {γ : Path p q} (hγ : PiecewiseGraphArc d U ⟨p, ⟨q, γ⟩⟩) {P : ℂ → ℝ} (hP : ContinuousOn P U) : arcIntegral d.proj P ⟨q, ⟨p, γ.symm⟩⟩ = -arcIntegral d.proj P ⟨p, ⟨q, γ⟩⟩

Reversing an actual finite graph-piece path negates its gauge integral.