CounterexampleConstruction: 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.

Wrong boundary orientation reverses the disk term

Statement refuted

Assume the axiom of choice. The boundary integral $\int_{\partial M} k_{g} d s$ appearing in the Gauss-Bonnet formula is unchanged if the boundary orientation convention "outward normal first" is replaced by "inward normal first". On a Euclidean disk the replacement makes the boundary clockwise and changes $\int k_{g} d s$ from $+ 2 π$ to $- 2 π$ while $χ (D) = 1$ , so the outward-normal-first identity would fail if the reversed convention were used.

Facts & Assumptions

Given: A Euclidean disk of radius $R > 0$ in the standard oriented plane, and the two candidate boundary conventions compared on the same circle.

[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]

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

[F2]

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

[F3]

The Euclidean Levi-Civita derivative in Cartesian coordinates is $\nabla_{X} Y = \sum_{j} X (Y^{j}) \partial_{j}$ 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; thus $\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 curvilinear triangulation of a compact smooth surface with boundary has the well-defined count $χ (M) = V - E + F$ (Curvilinear face-to-face triangulation, Topological well-definedness of the surface Euler characteristic).

Counterexample

technique · compute the boundary term of the same Euclidean disk in both conventions and show that the identity fails with the reversed one

1.1F3F4F5givenalgebra

Let $D = {x \in R^{2} : ∣ x ∣ \leq R}$ with $R > 0$ , the standard orientation and Euclidean metric. The frame $(\partial_{1}, \partial_{2})$ is orthonormal with $\nabla \partial_{i} = 0$ by [F3], so its connection form vanishes and $d ω = 0$ ; [F4] gives $K d A = 0$ , hence $K \equiv 0$ and $\int_{D} K d A = 0$ . The three vertices $R (1, 0)$ , $R (- 1 / 2, \sqrt{3} / 2)$ , $R (- 1 / 2, - \sqrt{3} / 2)$ divide the boundary circle into three regular $C^{2}$ arcs bounding a single closed face, a curvilinear triangulation with $V = 3$ , $E = 3$ , $F = 1$ ; by [F5], $χ (D) = 1$ .

1.2F1F3algebra

In the outward-normal-first convention, $ν = (\cos t, \sin t)$ is the outward normal at $γ (t) = R (\cos t, \sin t)$ and $T = (- \sin t, \cos t)$ is the unit tangent with $(ν, T)$ positive; $J T = - (\cos t, \sin t)$ is the inward unit conormal. 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_{\partial D} k_{g} d s = (1 / R) \cdot 2 π R = + 2 π$ .

1.3F1F3algebra

In the inward-normal-first convention the same circle is oriented by the inward normal $ν^{'} = - (\cos t, \sin t)$ : the selected tangent $T^{'}$ must satisfy that $(ν^{'}, T^{'})$ is positive, so $T^{'} = (\sin t, - \cos t) = - T$ , the clockwise unit tangent. Then $J T^{'} = + (\cos t, \sin t)$ and 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_{\partial D} k_{g}^{'} d s = - 2 π$ .

2.1F2step 1.1step 1.2step 1.3algebra

With the outward-normal-first boundary of step 1.2, the identity [F2] reads $0 + 2 π = 2 π χ (D) = 2 π$ , which is true. With the inward-normal-first boundary of step 1.3 the same identity would read $0 + (- 2 π) = 2 π χ (D) = 2 π$ , which is false. Hence the boundary term is not convention-independent: replacing outward-normal-first by inward-normal-first reverses it, and the reversed convention is incompatible with the Gauss-Bonnet identity.

3.1A1step 2.1∎

No new choice is made: the disk, the two parametrizations and the triangulation are explicit, and full AC entered only through the inherited smooth-boundary corollary of [F2].

Source locator

Lee, Riemannian Manifolds: An Introduction to Curvature, Chapter 9, Theorem 9.3 and the convention preceding it, printed pp. 163-167, fixes the boundary orientation by the outward normal and yields the positive disk contribution; Datar, Lectures on Riemannian Geometry, Lecture 2, Theorem 2.0.1, printed pp. 10-13, uses the same convention. The sign reversal under the opposite normal-first convention is computed here from the definition Signed geodesic curvature with the Euclidean connection Fundamental theorem of riemannian geometry.

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)