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.
Normal coordinates make the metric Euclidean throughout the chart
Statement
False claim: normal coordinates centred at a point make the Riemannian metric Euclidean at every point of their coordinate domain.
The library's current normal-coordinate interface assumes ; that background assumption is retained below and its exact use is identified, although the spherical calculation itself is explicit and choice-free.
Facts & Assumptions
Given: The smooth sphere , its round metric induced by the Euclidean dot product, the north pole , and the orthonormal basis , of .
The Axiom of Countable Choice () is the assumed .
For , is nonzero on . Thus A regular level set is an embedded submanifold makes it a smooth boundaryless surface and The tangent space of a regular level set is the kernel identifies . Its inclusion is an immersion, so Pullback of a riemannian metric is riemannian exactly for immersions and Riemannian metric and riemannian manifold make the restricted Euclidean dot product its round Riemannian metric.
Affine connection on a smooth manifold gives the connection axioms, Fundamental theorem of riemannian geometry characterizes the unique Levi--Civita connection, and Covariant derivative along a curve supplies differentiation along a curve.
Under [A1], Existence uniqueness and smooth dependence of geodesics identifies a geodesic from its initial data, Existence of normal neighborhoods and Normal neighborhood and normal coordinate chart supply the normal chart, and Properties of normal coordinates at the center gives and at its centre.
Sine is strictly increasing on , cosine is strictly decreasing on , , , and the mean value theorem applies to sine on a nondegenerate closed interval (Signs, monotonicity intervals, and ranges of sine and cosine, The derivatives of sine and cosine are cosine and minus sine, The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with ).
Refutation
Differentiating the equation gives , consistently with the round metric in [F1]. Put . For smooth tangent vector fields , define . The displayed formula is smooth and tangent-valued; pointwise linearity of and the ordinary directional-derivative product rule give real linearity in , function linearity in , and . Thus [F2] makes an affine connection. Moreover, for tangent , projection does not alter the dot product with either field, so the ordinary dot-product rule gives Finally is tangent, whence . Thus the connection is metric compatible and torsion free, and uniqueness in [F2] identifies it with the round Levi--Civita connection.
For with , put . Then , , , and is normal to the sphere. Applying the along-curve definition in [F2] to the projected connection of step 1.1 gives , so is a geodesic. Its formula extends at by the constant curve, and uniqueness in [F3] yields .
By [F3], restrict to a sufficiently small ball on which it is a diffeomorphism, and use the supplied basis to form normal coordinates. Choose and set , . Since , differentiating the formula of step 2.1 in the direction gives . This vector is exactly the second coordinate vector at because the inverse normal-coordinate chart is . By [F4], ; and the mean value theorem gives with . Strict decrease of cosine on gives , hence . Therefore the second coordinate vector has squared round length
The metric coefficient in step 3.1 is not the Euclidean value , even though [F3] gives and vanishing first metric derivatives at the centre. This is the exact failure: normal coordinates normalize the metric's value and first derivatives at their centre, not its values throughout the chart. The witness is two-dimensional and uses an interior point with ; is precisely the normalized centre, while empty and zero-dimensional manifolds cannot supply this counterexample. Assumption [A1] is used only through the library interfaces collected in [F3]; every construction and calculation in steps 1.1--3.1 is explicit and makes no choice.
Depends on
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Existence uniqueness and smooth dependence of geodesics
- Existence of normal neighborhoods
- Normal neighborhood and normal coordinate chart
- Properties of normal coordinates at the center
- Affine connection on a smooth manifold
- Covariant derivative along a curve
- Fundamental theorem of riemannian geometry
- A regular level set is an embedded submanifold
- The tangent space of a regular level set is the kernel
- Pullback of a riemannian metric is riemannian exactly for immersions
- Riemannian metric and riemannian manifold
- Signs, monotonicity intervals, and ranges of sine and cosine
- The derivatives of sine and cosine are cosine and minus sine
- The mean value theorem, as the case $g(x) = x$ of Cauchy's: for $f$ continuous on $[a,b]$ with $a < b$ and differentiable on $(a,b)$ there is $c \in (a,b)$ with $f(b) - f(a) = f'(c)(b-a)$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
60 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
- Ved Datar, Lectures on Riemannian Geometry, Example 17.1.3, Definition 17.2.1 and Proposition 17.2.2, pp. 128, 130--131 (standard reference, not scraped)