Gauss-Bonnet for compact oriented surface regions with boundary and corners

In presentation (a), [F1] gives finite face-to-face triangular closed disks of $M$ in frameable ambient charts, with its original boundary and corners retained. Orient every face by the ambient orientation. Their regular edges and ordinary sectors satisfy [F3], which yields ${\int }_{M}KdA+{\int }_{\mathrm{\partial }M}{k}_{g}ds+{\sum }_j{\alpha }_j=2\pi (V-E+F)$. The finite regular CW conclusion of [F1] identifies $V-E+F$ with the homology Euler characteristic of the cornered region.

In presentation (b), let $M_{+}$ be the labelled copy in the metric-extended double neighbourhood $\widehat{M}$ of [F2]. Choose positive boundary collar coordinates $(y,t)$ on $M_{+}$ with $t\ge 0$ and positive tangent coordinate $y$ chosen consistently with the given orientation and the outward-normal-first convention. The seam transitions of [F5] preserve $t$, and the transitions in $y$ have positive Jacobian because the boundary orientation is fixed. Thus these seam charts orient a smaller open neighbourhood of the seam on both sides. On the interior of $M_{+}$ this orientation agrees with the given one; adjoining its given interior charts gives an oriented open ambient neighbourhood of $M_{+}$ with the extended metric. This uses chart transition signs, not independent extensions of a differential form across the seam.

The labelled copy $M_{+}$ is the closure of its interior in that oriented ambient neighbourhood, and its smooth boundary has ordinary half-disk charts and no corners. Thus it is a regular oriented region of type (a). Apply step 1.1 with empty corner sum. The supplied metric restricts to $g$, so its curvature, area form, and boundary geodesic curvature on $M_{+}$ are those of $(M,g)$. The finite triangular data are a curvilinear triangulation in the smooth-boundary sense, and [F4] identifies its count with $\chi (M)$. This gives the claimed identity in (b). Full AC licenses both the finite triangulation [F1] and the local summation [F3]; its countable-choice consequence licenses [F2] and [F5], as stated in [A1].