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.
The Gauss-Bonnet expression is independent of the metric
Statement
Assume the axiom of choice through the local structure, Stokes and triangulation suppliers. Let be an oriented smooth surface and let be a compact regular oriented surface region with finitely many ordinary corners; let be smooth Riemannian metrics on an open neighbourhood of . For a smooth metric on that neighbourhood write where is the Gaussian curvature of , the signed geodesic curvature of the positively oriented boundary, and the signed exterior angles measured with . Then .
If in addition is a closed compact nonorientable smooth surface carrying smooth metrics and denotes the orientation-free Riemannian area density of , then . No classification of surfaces, Euler-Poincare theorem or characteristic-class theory is used.
Facts & Assumptions
Given: An oriented surface with a compact regular oriented region and two smooth metrics on a neighbourhood of it; in the second part, a closed nonorientable compact surface with two smooth metrics.
Full AC is inherited through the curvilinear triangulation supplier and its Jordan/plane-graph inputs; Stokes and the structure equation need only its countable-choice consequence (The Axiom of Choice, The Axiom of Countable Choice ()).
For a smooth positive orthonormal frame of a metric with connection form one has (Gaussian curvature structure equation).
Rotating a frame through a supplied smooth angle lift changes the connection form to ; on overlaps of two frames the transition angle is the same for a whole family of frames when the transition function of the family is fixed (Rotation law for the surface connection form).
For a regular unit-speed curve with tangent relative to a positive frame, (Tangent-angle formula for geodesic curvature).
For a compact regular oriented surface region with ordinary corners and a smooth one-form on a neighbourhood, (Stokes formula for finite ordinary surface corners).
At a positively oriented ordinary corner the signed exterior angle is the unique principal turn from the incoming to the outgoing unit tangent, equal to for interior angle (Signed exterior angle at an ordinary corner).
Reversing the parameter of a regular unit-speed curve changes the sign of its signed geodesic curvature at every point (Signs of geodesic curvature under reversals).
Every compact smooth Riemannian surface admits a finite face-to-face curvilinear triangulation with each face in a frameable chart (Finite curvilinear triangulation of a compact Riemannian surface).
A regular oriented surface region has a finite decomposition of its boundary into regular arcs and ordinary corners, with the outward-normal-first orientation (Regular oriented surface regions with corners).
The Riemannian area density and the orientation-free integral of a continuous function against it are defined without a choice of orientation (Riemannian volume density, Orientation-free density integration and its properties).
Proof
The metric is smooth and positive definite for every . Cover a neighbourhood of by finitely many oriented charts carrying positive -orthonormal frames, and on each chart let be the -self-adjoint positive bundle map with ; the positive square root is smooth in the point and in . Applying to a -orthonormal frame gives a positive -orthonormal frame, and because acts identically in every chart, the transition functions between overlapping charts are the same -valued functions for all .
On each boundary component choose a smooth starting point and divide its finitely many arcs further into finitely many chart-contained pieces. Make every genuine corner interior to one chosen frame chart, and put every added chart cut at a smooth point. For each , choose a continuous angle lift of the -unit tangent relative to the selected -frame on each smooth piece. Let be the sum of their angle increments plus the genuine corner jumps of [F5]. Integrating [F3] piecewise and summing gives , where each connection form is taken in that piece's selected frame.
Let be the connection form of the -frame on a chart and set . On an overlap, [F2] gives with independent of by step 1.1, so is chart-independent and defines a global smooth one-form on a neighbourhood of .
At a smooth artificial chart cut, the angle of the same tangent in the next frame differs from its angle in the preceding frame by the negative of their frame-transition angle, modulo . Step 1.1 makes that transition independent of ; choose its lift once, so the jump between the two continuous angle lifts is fixed throughout . At a genuine corner the jump between the one-sided angles in their common frame is the principal exterior angle , with the branch fixed continuously in because the tangent rays never become antipodal. Thus, on each closed boundary component, plus the sum of the fixed artificial-cut jumps is an integral multiple of : after all smooth increments and jumps the unit tangent returns to its starting direction. Both terms are continuous in , and the artificial-cut sum is constant, so this integer multiple is constant. Summing over the boundary components gives .
By [F1], for every , hence , that is .
Subtract the two piecewise identities of step 1.2. The connection forms need not be globally defined, but on every chosen boundary piece their difference is the restriction of the global form from step 2.1. Therefore, by steps 3.1 and 2.2, . Stokes [F4] makes this zero, so .
For the nonorientable closed case, fix a finite curvilinear triangulation of , which exists by [F7] applied to ; orient each triangular face arbitrarily and give it the induced boundary orientation. Each face is a compact regular disk region with ordinary corners and carries both restricted metrics, so steps 1.1-3.1 apply to it: writing for the face functional, one has for every face.
Summing over the finitely many faces, the area terms combine to the orientation-free integrals and by [F9]. Each interior edge has two incident faces on opposite sides; their inward conormals are opposite independently of their arbitrary face orientations, because reversing a face orientation reverses both its boundary tangent and its quarter-turn. Thus the signed curvature integrals cancel, and there are no boundary edges. At each vertex with incident faces the face-corner angles sum to , so the corner terms contribute , a number independent of the metric. Hence .
Source locator
Wendl, The Gauss-Bonnet Formula, Chapter 6, Section 6.3, printed pp. 147-152, gives the connection-form proof of Gauss-Bonnet and the transgression identity behind the comparison of two metrics (Corollary 6.42); Lee, Riemannian Manifolds, printed pp. 163-169, gives the local and global formulas in the conventions used on this page. The metric interpolation, the fixed-transition family of frames, the standard-one-form construction of step 2.1 and the closed nonorientable summation are proved here from the library items listed above; the boundary turning constant of step 2.2 uses only continuity in the metric family, so no classification theorem or Euler-Poincare identity enters this lemma.
Depends on
- The Axiom of Choice
- Rotation law for the surface connection form
- Gaussian curvature structure equation
- Tangent-angle formula for geodesic curvature
- Stokes formula for finite ordinary surface corners
- Finite curvilinear triangulation of a compact Riemannian surface
- Regular oriented surface regions with corners
- Signed exterior angle at an ordinary corner
- Signs of geodesic curvature under reversals
- Riemannian volume density
- Orientation-free density integration and its properties
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
52 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
- Chris Wendl, The Gauss-Bonnet Formula, Chapter 6, Section 6.3 (standard reference, not scraped)
- John M. Lee, Riemannian Manifolds: An Introduction to Curvature (1997) (standard reference, not scraped)