CorollaryStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck passaudited 2026-09-30

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Gauss-Bonnet with smooth boundary

Statement

Assume the axiom of choice through the parent triangulation and metric-extension suppliers. Let $M$ be a compact oriented Riemannian surface with smooth boundary, presented as in presentation (b) of Gauss-Bonnet for compact oriented surface regions with boundary and corners (the metric-extension neighbourhood of the labelled copy in its smooth double), or equivalently as a compact regular oriented region with empty corner set in an oriented boundaryless Riemannian surface. Then $\int_{M} K d A + \int_{\partial M} k_{g} d s = 2 π χ (M),$ the boundary carrying the outward-normal-first orientation, and when $\partial M = \emptyset$ the boundary integral is omitted, so that $\int_{M} K d A = 2 π χ (M)$ .

Facts & Assumptions

Given: A compact oriented Riemannian surface with smooth boundary in one of the two equivalent presentations, with the outward-normal-first boundary orientation.

[A1]

Full AC is inherited through the parent theorem, including both its curvilinear triangulation and local Gauss–Bonnet summation suppliers; this specialization makes no further choice (The Axiom of Choice).

[F1]

For a compact oriented Riemannian surface presented with smooth boundary, or as a regular region with finitely many ordinary corners, $\int_{M} K d A + \int_{\partial M} k_{g} d s + \sum_{j} α_{j} = 2 π χ (M)$ ; in the smooth-boundary presentation the corner sum is empty and when $\partial M = \emptyset$ both boundary terms are omitted (Gauss-Bonnet for compact oriented surface regions with boundary and corners).

[F2]

Each boundary curve in a regular-region presentation is a cyclic concatenation of finitely many regular $C^{2}$ embedded arcs meeting only at consecutive endpoints (Regular oriented surface regions with corners). At a smooth boundary, any such subdivision points are smooth points: their adjacent oriented tangent directions agree, so their interior angle is $π$ and their signed exterior angle is $0$ .

[F3]

For a compact smooth surface with smooth boundary, the number $χ (M)$ in [F1] is the common value of $V - E + F$ over the finite curvilinear triangulations of $M$ (Topological well-definedness of the surface Euler characteristic).

Proof

technique · apply the parent theorem with empty corner set and evaluate the corner sum as zero

1.1A1F1given

The parent theorem [F1] applies to the given presentation and gives $\int_{M} K d A + \int_{\partial M} k_{g} d s + \sum_{j} α_{j} = 2 π χ (M),$ with the outward-normal-first boundary orientation and with the corner sum empty in the smooth-boundary presentation.

2.1F1F2F3step 1.1algebra

In the smooth-boundary presentation there are no geometric corners. A closed boundary circle may be divided into finitely many regular arcs as in [F2]; every resulting subdivision point is smooth, with interior angle $π$ and signed exterior angle $0$ . Thus the corner sum in step 1.1 vanishes, and its removal gives $\int_{M} K d A + \int_{\partial M} k_{g} d s = 2 π χ (M)$ ; if $\partial M = \emptyset$ the boundary integral is absent, and the identity reads $\int_{M} K d A = 2 π χ (M)$ . The value $χ (M)$ on the right is the invariant of [F3].

3.1A1step 1.1step 2.1∎

The full-choice assumption is inherited unchanged from the parent theorem: the proof above adds only the evaluation of a vanishing finite sum and introduces no new selection or existence claim.

Source locator

Lee, Riemannian Manifolds: An Introduction to Curvature, Chapter 9, printed pp. 156-172, states the Gauss-Bonnet formula with the boundary integral and no corner term on smooth boundary (Theorem 9.3) and its global form (Theorem 9.7); Datar, Lectures on Riemannian Geometry, Lecture 2, Sections 2.0-2.2, printed pp. 10-15, writes the corner terms and observes that they are absent on smooth boundary (Theorem 2.0.1). The evaluation of the empty corner sum uses the library convention of Regular oriented surface regions with corners, and the Euler characteristic is the invariant of Topological well-definedness of the surface Euler characteristic; the transfer of the full axiom-of-choice hypothesis from the parent theorem is a bookkeeping step performed above.

Depends on

Used by

Wrong boundary orientation reverses the disk term Counterexample
Euclidean annulus boundary signs Example
Euclidean disk boundary curvature Example
Gauss-Bonnet for a spherical cap Example
A boundary term is necessary False statement

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John M. Lee, Riemannian Manifolds: An Introduction to Curvature (1997) (standard reference, not scraped)
Ved Datar, Lectures on Riemannian Geometry (standard reference, not scraped)