ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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.

Euclidean annulus boundary signs

Example

Assume the axiom of choice. Let $0 < r < R$ and let $A = {x \in R^{2} : r \leq ∣ x ∣ \leq R}$ be the Euclidean annulus with the standard orientation and metric. Then $K \equiv 0$ , the outer circle $∣ x ∣ = R$ contributes $+ 2 π$ and the inner circle $∣ x ∣ = r$ contributes $- 2 π$ to the boundary integral, and the total boundary integral vanishes: $\int_{A} K d A = 0, \int_{\partial A} k_{g} d s = 2 π - 2 π = 0, χ (A) = 0,$ so the Gauss-Bonnet identity reads $0 = 0$ . The opposite signs come from the outward-normal-first convention: the outward normal is radial and points away from the annulus on the outer circle but toward the origin on the inner circle, so the inner boundary is traversed clockwise.

Facts & Assumptions

Given: The open annulus data $0 < r < R$ , the region $A = {r \leq ∣ x ∣ \leq R}$ with the standard orientation of $R^{2}$ and the Euclidean metric.

[A1]

full AC is assumed; it is inherited through the smooth-boundary Gauss-Bonnet corollary quoted below and is used nowhere else in this Euclidean computation (The Axiom of Choice).

[F1]

For a compact oriented Riemannian surface with smooth boundary, $\int_{A} K d A + \int_{\partial A} k_{g} d s = 2 π χ (A)$ with the outward-normal-first boundary orientation (Gauss-Bonnet with smooth boundary).

[F2]

On each boundary arc the outward-normal-first rule selects the unit tangent $T$ with $(ν, T)$ positive for an outward transverse vector $ν$ , and then $J T$ is the inward unit conormal; the signed geodesic curvature of a regular $C^{2}$ unit-speed curve is $k_{g} = g (\nabla_{T} T, J T)$ (Regular oriented surface regions with corners, Oriented Riemannian surface and positive quarter-turn, Signed geodesic curvature).

[F3]

The Euclidean Levi-Civita derivative on $R^{2}$ is $\nabla_{X} Y = \sum_{j} X (Y^{j}) \partial_{j}$ in Cartesian coordinates, with vanishing Christoffel symbols; ordinary directional differentiation is torsion free and metric compatible for the constant Euclidean metric, so uniqueness identifies it as the Levi-Civita connection; in particular $\nabla_{T} T$ along a curve is the ordinary derivative of the unit tangent (Fundamental theorem of riemannian geometry).

[F4]

For a smooth positive orthonormal frame with connection form $ω$ , $d ω = - K d A$ (Gaussian curvature structure equation).

[F5]

A finite face-to-face piecewise $C^{2}$ curvilinear triangulation of a compact smooth surface with boundary has the well-defined count $χ (A) = V - E + F$ (Curvilinear face-to-face triangulation, Topological well-definedness of the surface Euler characteristic).

Verification

technique · compute the curvature, the Euler characteristic and the two boundary contributions of the Euclidean annulus

1.1F3F4algebra

The frame $(\partial_{1}, \partial_{2})$ of $R^{2}$ is orthonormal with $\nabla \partial_{i} = 0$ by [F3], so its connection form vanishes and $d ω = 0$ ; by [F4], $K d A = 0$ and hence $K \equiv 0$ on $A$ , so $\int_{A} K d A = 0$ .

1.2F5givenconstruct

With $u_{i} = (\cos (2 π i / 3), \sin (2 π i / 3))$ , put $a_{i} = r u_{i}$ and $b_{i} = R u_{i}$ for $i = 0, 1, 2$ (indices mod $3$ ). The polar map $Φ_{i} (s, t) = (r + (R - r) s) (\cos (2 π (i + t) / 3), \sin (2 π (i + t) / 3))$ is a smooth embedding of the closed parameter square $[0, 1]^{2}$ onto the $i$ th annular sector: its Jacobian determinant is $(R - r) (r + (R - r) s) 2 π / 3 > 0$ . Its diagonal $δ_{i} (t) = Φ_{i} (t, t)$ joins $a_{i}$ to $b_{i + 1}$ and has relative interior strictly inside $A$ and the angular sector. The two closed parameter triangles cut by $s = t$ map to regular curvilinear triangular disks with vertices $a_{i}, a_{i + 1}, b_{i + 1}$ and $a_{i}, b_{i}, b_{i + 1}$ . Thus the inner circle arcs $a_{i} a_{i + 1}$ , outer circle arcs $b_{i} b_{i + 1}$ , radial segments $a_{i} b_{i}$ and curves $δ_{i}$ are twelve edges with six vertices and six faces; sectors meet along full radial edges and their two triangles meet along $δ_{i}$ . The positive Jacobian gives the inherited orientations, with the outer arcs counterclockwise and the inner arcs clockwise. The resulting face-to-face curvilinear triangulation has interval links at all boundary vertices, so by [F5] $χ (A) = 6 - 12 + 6 = 0$ .

1.3F2F3algebra

On the outer circle $γ_{o u t} (t) = R (\cos t, \sin t)$ the outward normal is $ν = (\cos t, \sin t)$ and the outward-normal-first tangent is $T = (- \sin t, \cos t)$ with $J T = - (\cos t, \sin t)$ . By [F3], $\nabla_{T} T = - (1 / R) (\cos t, \sin t)$ , so $k_{g} = g (- (1 / R) (\cos t, \sin t), - (\cos t, \sin t)) = 1 / R$ and $\int_{∣ x ∣ = R} k_{g} d s = (1 / R) \cdot 2 π R = + 2 π$ .

1.4F2F3algebra

On the inner circle $γ_{i n} (t) = r (\cos t, \sin t)$ the outward normal of $A$ is $ν = - (\cos t, \sin t)$ , so the outward-normal-first tangent is the clockwise unit tangent $T^{'} = - (- \sin t, \cos t) = (\sin t, - \cos t)$ , and $J T^{'} = (\cos t, \sin t)$ . By [F3], $\nabla_{T^{'}} T^{'} = - (1 / r) (\cos t, \sin t)$ , so $k_{g}^{'} = g (- (1 / r) (\cos t, \sin t), (\cos t, \sin t)) = - 1 / r$ and $\int_{∣ x ∣ = r} k_{g} d s = - (1 / r) \cdot 2 π r = - 2 π$ .

2.1F1step 1.1step 1.2step 1.3step 1.4algebra

By steps 1.3 and 1.4 the boundary integral is $\int_{\partial A} k_{g} d s = 2 π - 2 π = 0$ , and by step 1.1 the curvature integral is $0$ ; with $χ (A) = 0$ of step 1.2 the identity [F1] reads $0 + 0 = 2 π \cdot 0$ , which is true.

3.1A1step 2.1∎

No new choice is made: the annulus, its triangulation and both circle parametrizations are explicit, and full AC entered only through the inherited smooth-boundary corollary of [F1].

Source locator

Lee, Riemannian Manifolds: An Introduction to Curvature, Chapter 9, Theorem 9.3, printed pp. 165-167, contains the boundary term with the outward-normal-first orientation, and Datar, Lectures on Riemannian Geometry, Lecture 2, Theorem 2.0.1, printed pp. 10-13, states the same formula; the annulus is the standard region with two boundary components whose contributions cancel. The Euclidean connection is the published library item Fundamental theorem of riemannian geometry; the sign of the inner contribution is computed here directly from the outward-normal-first rule, not assumed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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