DefinitionDefinition: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 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.

Signed exterior angle at an ordinary corner

Definition

Let $D$ be a regular oriented region in an oriented Riemannian surface, and let $p$ be one of its ordinary boundary vertices. Let $T_{-}$ and $T_{+}$ be the incoming and outgoing one-sided unit tangents to the positively oriented boundary at $p$ . The signed exterior angle at $p$ is the unique $α \in (- π, π)$ such that $T_{+} = \cos (α) T_{-} + \sin (α) J T_{-},$ where $J$ is the positive quarter-turn. The opposite-tangent case $T_{+} = - T_{-}$ is excluded because it does not distinguish $+ π$ from $- π$ .

If $β \in (0, 2 π)$ is the interior sector angle at a positively oriented boundary corner, then $α = π - β .$ Thus convex corners have positive exterior angle, reflex corners have negative exterior angle, and a straight subdivision point has angle zero. For the same tangent vectors, replacing $J$ by $- J$ changes $α$ to $- α$ . For fixed $J$ , reversing the boundary parameter changes the ordered pair to $(- T_{+}, - T_{-})$ and also changes the signed angle to $- α$ .

Facts & Assumptions

Given: An oriented Riemannian surface with positive quarter-turn $J$ , a regular oriented region $D$ , and its positively oriented boundary with a specified ordinary vertex $p$ and one-sided unit tangents $T_{-}, T_{+}$ .

[F1]

In a positive orthonormal frame, $J E_{1} = E_{2}$ and $J E_{2} = - E_{1}$ ; hence for any unit vector $T$ , $(T, J T)$ is a positive orthonormal basis (Oriented Riemannian surface and positive quarter-turn).

[F2]

At an ordinary vertex the one-sided velocities are not opposite: the regular-region definition requires $v_{+} \neq - c v_{-}$ for every $c > 0$ (Regular oriented surface regions with corners).

Proof

technique · oriented metric coordinates in the tangent plane

1.1F1F2given

By [F1], $(T_{-}, J T_{-})$ is a positive orthonormal basis of $T_{p} M$ . Write $T_{+} = a T_{-} + b J T_{-}$ . Since $T_{+}$ is unit, $a^{2} + b^{2} = 1$ . By [F2], $T_{+} \neq - T_{-}$ , so $(a, b) \neq (- 1, 0)$ . The unit circle with that one point removed has a unique angle coordinate $α \in (- π, π)$ , with $a = \cos α$ and $b = \sin α$ . This proves existence and uniqueness of the stated signed angle. If $T_{+} = T_{-}$ , then $(a, b) = (1, 0)$ and $α = 0$ .

2.1F1F2step 1.1given

At a positively oriented boundary vertex the region lies to the left of each boundary arc. Its interior sector angle $β$ is therefore the positive turn from $T_{+}$ to the backward tangent $- T_{-}$ through the sector, with $0 < β < 2 π$ by the supplied ordinary-corner chart and [F2]. In the positive orthonormal basis $(T_{-}, J T_{-})$ , the turn from $T_{-}$ to $- T_{-}$ is $π$ , while the turn from $T_{-}$ to $T_{+}$ is $α$ . Thus the positive turn from $T_{+}$ to $- T_{-}$ through the region is $π - α$ ; since $α \in (- π, π)$ , this number is already in $(0, 2 π)$ and equals $β$ , with no modulo ambiguity. Hence $α = π - β$ . Therefore $β < π$ gives $α > 0$ , $β = π$ gives $α = 0$ , and $β > π$ gives $α < 0$ .

3.1F1F2step 1.1∎

For the same ordered pair, replacing $J$ by $- J$ changes the coefficient $b$ in step 1.1 to $- b$ , so the unique principal angle changes to $- α$ . On reversing the boundary parameter, the ordered pair becomes $(- T_{+}, - T_{-})$ . The rotation by $- α$ sends $- T_{+}$ to $- T_{-}$ , since rotations commute with multiplication by $- 1$ ; as $- α \in (- π, π)$ , this is again the unique principal angle. Both assertions include $α = 0$ , and the non-antipodal hypothesis [F2] keeps the principal angle unambiguous.

Source locator

Lee, Riemannian Manifolds: An Introduction to Curvature, Chapter 9, §“Some Plane Geometry,” printed p. 157, defines the oriented exterior turn in $[- π, π]$ and notes the ambiguity when the tangents are opposite; §“The Gauss–Bonnet Formula,” printed p. 163, defines the corresponding angle using the Riemannian inner product and the given surface orientation. Datar, Lectures on Riemannian Geometry, Lecture 2, §2.0, printed pp. 10–11, uses the signed angle and excludes exterior angles $\pm π$ for curved polygons. For a non-antipodal tangent pair, the closed interval convention reduces uniquely to $(- π, π)$ ; the local basis calculation and the $α = π - β$ relation are derived above.

Depends on

Used by

Corner terms are required even in the plane Counterexample
Area excess of a spherical geodesic triangle Example
Summing local Gauss-Bonnet over a supplied triangulation Lemma
The Gauss-Bonnet expression is independent of the metric Lemma
Total turning with connection and corner terms Proposition
Gauss-Bonnet for a geodesic triangle Theorem
Hopf turning-tangent theorem with ordinary corners Theorem
Local Gauss-Bonnet for a frameable disk region Theorem
Local Gauss-Bonnet for an arbitrary disk region Theorem

Dependency tree · two levels

5 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)