Geometric comparison of directional boundary chains

The comparison generators include coordinate-constant arcs, endpoint cycles on one graph, and actual joins, reversals, and regular reparametrizations of finite graph-piece paths. They compare original whole arcs with their pieces even when the whole arc is not a graph. Integer sums of these geometric generators have zero coordinate integral. Graph containment in U is part of the geometric certificate, so field continuity is needed only on U. The two coordinates can use entirely different comparison certificates.

theorem TauCeti.Green.BoundaryChain.integral_eq_boundary_of_graph {d : Coordinate} {g : ℝ → ℝ} {a b : ℝ} {c : BoundaryChain} (hc : ∀ γ ∈ c.support, GraphArc d g a b γ) {P : ℂ → ℝ} (hP : ContinuousOn P (d.graph g '' Set.Icc a b)) : (integral d.proj P) c = (Finsupp.linearCombination ℤ fun (z : ℂ) => ∫ (t : ℝ) in a..d.proj z, P (d.graph g t)) (boundary c)

The integral of a graph-supported chain is the integral primitive evaluated at its endpoint boundary. This is the telescoping mechanism behind all graph comparisons.

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

Geometric null chains for a directional integral. Graph cycles have zero endpoint boundary; coordinate-constant arcs are ignored. The constructors contain no integral claims.

• zero {d : Coordinate} {U : Set ℂ} : NullChain d U 0
• add {d : Coordinate} {U : Set ℂ} {c e : BoundaryChain} : NullChain d U c → NullChain d U e → NullChain d U (c + e)
• neg {d : Coordinate} {U : Set ℂ} {c : BoundaryChain} : NullChain d U c → NullChain d U (-c)
• constant {d : Coordinate} {U : Set ℂ} {p q : ℂ} (γ : Path p q) (hγ : ∀ (t : ↑unitInterval), d.proj (γ t) = d.proj p) : NullChain d U (ofPath γ)
• graph {d : Coordinate} {U : Set ℂ} {g : ℝ → ℝ} {a b : ℝ} {c : BoundaryChain} (hgraph : d.graph g '' Set.Icc a b ⊆ U) (harcs : ∀ γ ∈ c.support, GraphArc d g a b γ) (hboundary : boundary c = 0) : NullChain d U c
• join {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, δ⟩⟩) : NullChain d U (ofPath (γ.trans δ) - (ofPath γ + ofPath δ))
• reverse {d : Coordinate} {U : Set ℂ} {p q : ℂ} {γ : Path p q} (hγ : PiecewiseGraphArc d U ⟨p, ⟨q, γ⟩⟩) : NullChain d U (ofPath γ + ofPath γ.symm)
• reparam {d : Coordinate} {U : Set ℂ} {p q : ℂ} {γ δ : Path p q} (hδ : PiecewiseGraphArc d U ⟨p, ⟨q, δ⟩⟩) (θ : ℝ → ℝ) (h : RegularReparam θ γ δ) : NullChain d U (ofPath γ - ofPath δ)

theorem TauCeti.Green.BoundaryChain.NullChain.trans {d : Coordinate} {U : Set ℂ} {c e f : BoundaryChain} (hce : NullChain d U (c - e)) (hef : NullChain d U (e - f)) : NullChain d U (c - f)

Geometric comparisons compose by actual cancellation of the intermediate chain.

theorem TauCeti.Green.BoundaryChain.NullChain.zsmul {d : Coordinate} {U : Set ℂ} {c : BoundaryChain} (h : NullChain d U c) (n : ℤ) : NullChain d U (n • c)

Integer multiplicities preserve geometric null-chain certificates.

theorem TauCeti.Green.BoundaryChain.NullChain.sum {d : Coordinate} {U : Set ℂ} {ι : Type u_1} (s : Finset ι) (c : ι → BoundaryChain) (h : ∀ i ∈ s, NullChain d U (c i)) : NullChain d U (∑ i ∈ s, c i)

Independent geometric comparisons can be added over any finite family.

theorem TauCeti.Green.BoundaryChain.NullChain.graph_reparam {d : Coordinate} {U : Set ℂ} {g : ℝ → ℝ} {a b : ℝ} {p q : ℂ} {γ δ : Path p q} (hγ : GraphArc d g a b ⟨p, ⟨q, γ⟩⟩) (hδ : GraphArc d g a b ⟨p, ⟨q, δ⟩⟩) (hU : d.graph g '' Set.Icc a b ⊆ U) : NullChain d U (ofPath γ - ofPath δ)

Graph reparametrizations with the same endpoints represent the same directional boundary.

theorem TauCeti.Green.BoundaryChain.NullChain.graph_subdivision {d : Coordinate} {U : Set ℂ} {g : ℝ → ℝ} {a b : ℝ} {p q r : ℂ} {γ : Path p q} {γ₁ : Path p r} {γ₂ : Path r q} (hγ : GraphArc d g a b ⟨p, ⟨q, γ⟩⟩) (h₁ : GraphArc d g a b ⟨p, ⟨r, γ₁⟩⟩) (h₂ : GraphArc d g a b ⟨r, ⟨q, γ₂⟩⟩) (hU : d.graph g '' Set.Icc a b ⊆ U) : NullChain d U (ofPath γ - (ofPath γ₁ + ofPath γ₂))

Subdivision at a common endpoint preserves the directional boundary presentation.

theorem TauCeti.Green.BoundaryChain.NullChain.segment {d : Coordinate} {U : Set ℂ} {p q : ℂ} (hpq : d.proj p = d.proj q) : NullChain d U (ofPath (Path.segment p q))

A straight segment parallel to the unused coordinate is ignored by the comparison.

theorem TauCeti.Green.BoundaryChain.NullChain.integrable_and_integral_eq_zero {d : Coordinate} {U : Set ℂ} {c : BoundaryChain} (h : NullChain d U c) {P : ℂ → ℝ} (hP : ContinuousOn P U) : Integrable d.proj P c ∧ (integral d.proj P) c = 0

Every geometrically null chain is gauge integrable and has zero directional integral.

theorem TauCeti.Green.BoundaryChain.NullChain.integral_eq {d : Coordinate} {U : Set ℂ} {c e : BoundaryChain} (h : NullChain d U (c - e)) {P : ℂ → ℝ} (hP : ContinuousOn P U) : (integral d.proj P) c = (integral d.proj P) e

A geometric certificate comparing two boundaries gives equality of their coordinate integrals. Integrability transfer is given separately by NullChain.integrable_iff.

theorem TauCeti.Green.BoundaryChain.NullChain.integrable_iff {d : Coordinate} {U : Set ℂ} {c e : BoundaryChain} (h : NullChain d U (c - e)) {P : ℂ → ℝ} (hP : ContinuousOn P U) : Integrable d.proj P c ↔ Integrable d.proj P e

Integrability transfers across a geometric comparison certificate.