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.

Total curvature of a round sphere

Example

Assume the axiom of choice. Let $S_{R}^{2}$ be the round sphere of radius $R > 0$ with its induced metric and standard orientation. Then $K \equiv 1 / R^{2}$ , the area is $4 π R^{2}$ , and $\int_{S_{R}^{2}} K d A = \frac{1}{R^{2}} \cdot 4 π R^{2} = 4 π = 2 π χ (S_{R}^{2})$ with $χ (S_{R}^{2}) = 2$ counted from the octahedral curvilinear triangulation $V = 6$ , $E = 12$ , $F = 8$ . The polar chart used for the curvature computation misses only the two poles and the seam, where $K$ is obtained by continuity.

Facts & Assumptions

Given: The round sphere $S_{R}^{2}$ of radius $R > 0$ with the metric induced from $R^{3}$ , its standard orientation, and the spherical polar chart $X (θ, φ) = R (\sin θ \cos φ, \sin θ \sin φ, \cos θ)$ .

[A1]

full AC is assumed; it is inherited through the global Gauss-Bonnet theorem quoted below and also covers the countable-choice hypothesis inherited by the curvature structure equation; the explicit computations add no choice (The Axiom of Choice).

[F1]

For every closed oriented Riemannian surface, $\int_{S_{R}^{2}} K d A = 2 π χ (S_{R}^{2})$ (Global Gauss-Bonnet for closed oriented surfaces).

[F2]

For a regular embedded surface patch the induced metric coefficients are the Euclidean Gram products of its parameter tangent vectors, and its area density is the square root of the Gram determinant (The first fundamental form, Gram matrix, and area density of a surface patch).

[F3]

The area of a regular patch is the integral of its Gram area density over its parameter domain; changing bounded integrands on a content-zero parameter boundary does not change that integral (Surface area and scalar surface integrals on a regular patch, Content-zero parameter-boundary exceptions do not affect surface integrals).

[F4]

In coordinates the Levi-Civita symbols are $Γ^{k}_{i j} = \frac{1}{2} \sum_{ℓ} g^{k ℓ} (\partial_{i} g_{j ℓ} + \partial_{j} g_{i ℓ} - \partial_{ℓ} g_{i j})$ (Christoffel formula for the levi civita connection).

[F5]

For a smooth positive orthonormal frame with connection form $ω (X) = g (\nabla_{X} e_{1}, e_{2})$ one has $\nabla_{X} e_{1} = ω (X) e_{2}$ and $d ω = - K d A$ ; the area form satisfies $d A = e^{1} \land e^{2}$ for the dual coframe and is the unique positive unit top form of the orientation (Connection one-form of an oriented orthonormal frame, Gaussian curvature structure equation, The riemannian volume form is the unique positive unit top form, Riemannian volume form on an oriented manifold).

[F6]

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

Verification

technique · compute the round metric, connection form and curvature in polar coordinates, integrate the constant curvature against the sphere's area, and count an explicit triangulation

1.1F2F4algebra

Direct differentiation of $X (θ, φ) = R (\sin θ \cos φ, \sin θ \sin φ, \cos θ)$ gives $⟨ X_{θ}, X_{θ} ⟩ = R^{2}$ , $⟨ X_{φ}, X_{φ} ⟩ = R^{2} \sin^{2} θ$ , and $⟨ X_{θ}, X_{φ} ⟩ = 0$ . By [F2] these are the induced metric coefficients, so $e_{1} = (1 / R) \partial_{θ}$ and $e_{2} = (1 / (R \sin θ)) \partial_{φ}$ are a smooth positive orthonormal frame with dual coframe $e^{1} = R d θ$ , $e^{2} = R \sin θ d φ$ . By [F4], $Γ^{θ}_{φ φ} = - \sin θ \cos θ$ and $Γ^{φ}_{θ φ} = Γ^{φ}_{φ θ} = \cot θ$ are the only nonzero symbols, so $\nabla_{e_{1}} e_{1} = 0$ and $\nabla_{e_{2}} e_{1} = (\cot θ / R) e_{2}$ .

1.2F6givenconstruct

Let $u_{1}, u_{2}, u_{3}$ be the standard unit coordinate vectors in $R^{3}$ . The six points $\pm R u_{1}, \pm R u_{2}, \pm R u_{3}$ are the vertices of the regular octahedron inscribed in $S_{R}^{2}$ ; radial projection of its boundary gives a face-to-face curvilinear triangulation of $S_{R}^{2}$ with $V = 6$ , $E = 12$ (the octahedron's edges, each a great-circle arc) and $F = 8$ (the spherical triangles cut out by the coordinate octants), so by [F6] $χ (S_{R}^{2}) = 6 - 12 + 8 = 2$ .

2.1F5step 1.1algebra

By step 1.1, $ω (e_{1}) = 0$ and $ω (e_{2}) = \cot θ / R$ , hence $ω = \cos θ d φ$ ; then $d ω = - \sin θ d θ \land d φ$ , while $d A = e^{1} \land e^{2} = R^{2} \sin θ d θ \land d φ$ by [F5]. Comparing with $d ω = - K d A$ gives $K = 1 / R^{2}$ on the chart. The chart domain is dense in $S_{R}^{2}$ (its complement is the two poles together with the seam $φ = 0$ ), and both $K$ and the constant $1 / R^{2}$ are continuous on $S_{R}^{2}$ , so $K \equiv 1 / R^{2}$ on all of $S_{R}^{2}$ .

2.2F2F3F5step 1.1algebra

The Gram determinant of step 1.1 is $R^{4} \sin^{2} θ$ , so [F2] gives area density $R^{2} \sin θ$ on $0 < θ < π$ , $0 < φ < 2 π$ . The excluded poles and longitude seam are the parameter-boundary exceptions of [F3] and contribute zero area. Hence $Area (S_{R}^{2}) = \int_{0}^{2 π} \int_{0}^{π} R^{2} \sin θ d θ d φ = 4 π R^{2}$ . This is also the Riemannian area form of [F5].

3.1F1step 2.1step 2.2step 1.2algebra

By steps 2.1 and 2.2, $\int_{S_{R}^{2}} K d A = (1 / R^{2}) \cdot 4 π R^{2} = 4 π$ , and by step 1.2, $2 π χ (S_{R}^{2}) = 2 π \cdot 2 = 4 π$ ; the global identity [F1] is therefore verified on the round sphere, $\int_{S_{R}^{2}} K d A = 2 π χ (S_{R}^{2})$ .

4.1A1step 3.1∎

No new choice is made: the polar chart, the octahedral vertices and the triangulation are explicit, and AC licenses the inherited global Gauss-Bonnet theorem of [F1] and the countable-choice assumption of the structure equation in [F5].

Source locator

Lee, Riemannian Manifolds: An Introduction to Curvature, Chapter 9, Theorem 9.7, printed pp. 167-172, gives the global identity, and Datar, Lectures on Riemannian Geometry, Lecture 2, Theorem 2.2.4, printed pp. 14-15, states it. The round metric and total area are computed directly above from the Gram coefficients and patch area density The first fundamental form, Gram matrix, and area density of a surface patch, while $χ (S_{R}^{2}) = 2$ is counted from the octahedral triangulation.

Depends on

Used by

A deformed sphere has the same total curvature Example

Dependency tree · two levels

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