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

A deformed sphere has the same total curvature

Example

Assume the axiom of choice. Let $(S^{2}, o)$ be the oriented two-sphere. Every smooth Riemannian metric $g$ on $S^{2}$ has $\int_{S^{2}} K_{g} d A_{g} = 4 π,$ although $K_{g}$ need not be constant. In particular the induced metric of an ellipsoid, transported to $S^{2}$ by radial projection, has total Gaussian curvature $4 π$ ; for the spheroid with semi-axes $(a, a, c)$ , $a \neq c$ , the Gaussian curvature takes the value $c^{2} / a^{4}$ at the poles and $1 / c^{2}$ on the equator, so it is not constant and the constancy of the integral is substantive.

Facts & Assumptions

Given: The oriented two-sphere $S^{2}$ with the round metric of radius $R$ as reference, an arbitrary smooth Riemannian metric $g$ on $S^{2}$ , and the spheroid $Σ_{a, c} = {x_{1}^{2} / a^{2} + x_{2}^{2} / a^{2} + x_{3}^{2} / c^{2} = 1}$ with $a, c > 0$ .

[A1]

full AC is assumed; it is inherited through the metric-independence corollary and the round-sphere example quoted below and is used nowhere else (The Axiom of Choice).

[F1]

For a closed oriented surface $M$ and two smooth Riemannian metrics $g_{0}, g_{1}$ on $M$ , $\int_{M} K_{g_{0}} d A_{g_{0}} = \int_{M} K_{g_{1}} d A_{g_{1}} = 2 π χ (M)$ (Metric independence of total Gaussian curvature).

[F2]

On the round sphere of radius $R$ , $χ (S^{2}) = 2$ and $\int_{S^{2}} K d A = 4 π$ (Total curvature of a round sphere).

[F3]

The inclusion $Σ_{a, c} ↪ R^{3}$ of the spheroid is an immersion, so the induced metric is Riemannian (Pullback of a riemannian metric is riemannian exactly for immersions); radial projection $R^{3} ∖ {0} \to S^{2}$ restricts to a diffeomorphism $Σ_{a, c} \to S^{2}$ , so the induced metric transported along it is a smooth Riemannian metric on $S^{2}$ . On the chart $X (u, v) = (a \sin u \cos v, a \sin u \sin v, c \cos u)$ its coefficients are $E = a^{2} \cos^{2} u + c^{2} \sin^{2} u$ , $F = 0$ , $G = a^{2} \sin^{2} u$ .

[F4]

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

[F5]

With $R (\partial_{i}, \partial_{j}) \partial_{k} = R^{ℓ}_{k i j} \partial_{ℓ}$ , the coordinate curvature formula is $R^{ℓ}_{k i j} = \partial_{i} Γ^{ℓ}_{j k} - \partial_{j} Γ^{ℓ}_{i k} + Γ^{m}_{j k} Γ^{ℓ}_{i m} - Γ^{m}_{i k} Γ^{ℓ}_{j m}$ (Coordinate formula for the curvature tensor).

[F6]

The four-tensor is $Rm (A, B, C, D) = g (R (A, B) C, D)$ , and the sectional curvature of the plane spanned by independent $A, B$ is $Rm (A, B, B, A) / (g (A, A) g (B, B) - g (A, B)^{2})$ (Riemann curvature four-tensor, Sectional curvature).

Verification

technique · obtain the total curvature $4\pi$ for every metric from metric independence and the round sphere, then compute the spheroid metric explicitly to exhibit nonconstant pointwise curvature

1.1F1F2F3givenalgebra

By [F2], $χ (S^{2}) = 2$ and the round metric has total curvature $4 π$ ; applying [F1] with the round metric as $g_{0}$ and any smooth metric $g$ on $S^{2}$ as $g_{1}$ gives $\int_{S^{2}} K_{g} d A_{g} = 2 π χ (S^{2}) = 4 π$ . The spheroid metric transported by the diffeomorphism of [F3] is such a smooth metric, so it too has total curvature $4 π$ .

1.2F3algebra

On the spheroid chart of [F3], $X_{u} = (a \cos u \cos v, a \cos u \sin v, - c \sin u)$ and $X_{v} = (- a \sin u \sin v, a \sin u \cos v, 0)$ , so the induced metric has $E = ⟨ X_{u}, X_{u} ⟩ = a^{2} \cos^{2} u + c^{2} \sin^{2} u$ , $F = ⟨ X_{u}, X_{v} ⟩ = 0$ and $G = ⟨ X_{v}, X_{v} ⟩ = a^{2} \sin^{2} u$ , all depending on $u$ alone.

2.1F4step 1.2algebra

Substituting $E = E (u)$ , $G = G (u)$ in [F4], the only nonzero symbols are $Γ^{1}_{11} = E^{'} / (2 E)$ , $Γ^{1}_{22} = - G^{'} / (2 E)$ and $Γ^{2}_{12} = Γ^{2}_{21} = G^{'} / (2 G)$ .

3.1F5F6step 2.1algebra

With $x^{1} = u$ , $x^{2} = v$ , the needed component of [F5] is $R^{1}_{212} = \partial_{1} Γ^{1}_{22} - \partial_{2} Γ^{1}_{12} + Γ^{m}_{22} Γ^{1}_{1 m} - Γ^{m}_{12} Γ^{1}_{2 m}$ , whose four terms are $- G^{''} / (2 E) + G^{'} E^{'} / (2 E^{2})$ , $0$ , $- G^{'} E^{'} / (4 E^{2})$ and $G^{' 2} / (4 E G)$ ; hence $R^{1}_{212} = - G^{''} / (2 E) + G^{'} E^{'} / (4 E^{2}) + G^{' 2} / (4 E G)$ . Since $F = 0$ , [F6] gives $K = Rm (\partial_{1}, \partial_{2}, \partial_{2}, \partial_{1}) / (E G) = R^{1}_{212} / G$ .

4.1step 3.1algebra

Specialize $E = a^{2} \cos^{2} u + c^{2} \sin^{2} u$ and $G = a^{2} \sin^{2} u$ , so that $G^{'} = 2 a^{2} \sin u \cos u$ , $G^{''} = 2 a^{2} (\cos^{2} u - \sin^{2} u)$ and $E^{'} = 2 (c^{2} - a^{2}) \sin u \cos u$ . Multiplying $K$ by $4 E^{2} G$ and expanding with $\sin^{2} u + \cos^{2} u = 1$ gives $- 2 E G^{''} + E^{'} G^{'} + E G^{' 2} / G = 4 c^{2} G$ , hence $K = c^{2} / E^{2} = c^{2} / (a^{2} \cos^{2} u + c^{2} \sin^{2} u)^{2}$ on the chart.

5.1step 4.1algebra

As $u \to 0$ or $u \to π$ one has $E \to a^{2}$ , so the continuous extension of $K$ to the poles has value $c^{2} / a^{4}$ , while at the equator $u = π / 2$ one has $E = c^{2}$ and $K = c^{2} / c^{4} = 1 / c^{2}$ . If $a \neq c$ these values differ, since $c^{2} / a^{4} = 1 / c^{2}$ would force $c^{4} = a^{4}$ and hence $c = a$ ; therefore the Gaussian curvature of a nonspherical spheroid is not constant.

6.1F1F2step 1.1step 4.1step 5.1

Steps 1.1 and 5.1 together show that the total curvature $4 π$ is metric-independent while the pointwise curvature is not: the round sphere is the constant-curvature case $a = c$ , and the nonspherical spheroid has total curvature $4 π$ by step 1.1 with nonconstant $K$ by step 5.1.

7.1A1step 6.1∎

No new choice is made: the chart, the metric coefficients and the reference metric are explicit, and full AC entered only through the inherited metric-independence corollary and round-sphere example.

Source locator

Lee, Riemannian Manifolds: An Introduction to Curvature, Chapter 9, Theorem 9.7 and Problem 9-5, printed pp. 167-172, proves that the total curvature is $2 π χ (M)$ and hence a topological invariant; the surfaces-of-revolution and ellipsoid computations are Lee's Exercise 3.3(b)-(c) printed pp. 25-26, Problem 5-2(a) printed p. 87 and Problem 8-1(a) printed p. 150, and Datar, Lectures on Riemannian Geometry, Lecture 2, Theorem 2.2.4, printed pp. 14-15, states the global identity. The spheroid curvature $c^{2} / (a^{2} \cos^{2} u + c^{2} \sin^{2} u)^{2}$ is computed here from the Christoffel and curvature formulas of Christoffel formula for the levi civita connection and Coordinate formula for the curvature tensor, not imported; the values $c^{2} / a^{4}$ at the poles and $1 / c^{2}$ at the equator exhibit the nonconstancy.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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