Green's theorem on the standard triangle

The independently constructed graph divisions and their geometric comparison certificates give Green's theorem on the genuine convex hull of 0, 1, and I. The boundary consists of the three actual straight paths. For fields C¹ near the triangle, all gauge, curve, and area integrability hypotheses follow from continuity and compactness.

theorem TauCeti.Green.green_standardTriangle {U : Set ℂ} (hU : IsOpen U) (hTU : standardTriangle ⊆ U) {P Q : ℂ → ℝ} (hP : ContDiffOn ℝ 1 P U) (hQ : ContDiffOn ℝ 1 Q U) : MeasureTheory.IntegrableOn (curl P Q) standardTriangle MeasureTheory.volume ∧ curveIntegral (oneForm P Q) (Path.segment 0 1) + curveIntegral (oneForm P Q) (Path.segment 1 Complex.I) - curveIntegral (oneForm P Q) (Path.segment 0 Complex.I) = ∫ (z : ℂ) in standardTriangle, curl P Q z

Green on the standard triangle for fields C¹ on any open neighborhood. The three Bochner curve integrals add the edges from 0 to 1 and from 1 to I, and subtract the edge from 0 to I.