Alphabeta Math
False statementConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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 ACω; 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 S2={qR3:qq=1}, its round metric induced by the Euclidean dot product, the north pole N=(0,0,1), and the orthonormal basis e1=(1,0,0), e2=(0,1,0) of TNS2.

[A1]
[F1]

For F(q)=qq, dFq(v)=2qv is nonzero on S2. 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 TqS2=q. 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.

[F2]

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.

[F3]

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 gij(N)=δij and kgij(N)=0 at its centre.

Refutation

technique · direct
1.1

Differentiating the equation qq=1 gives TqS2=q, consistently with the round metric in [F1]. Put Pq(z)=z(zq)q. For smooth tangent vector fields X,Y:S2R3, define XY=P(dY(X)). The displayed formula is smooth and tangent-valued; pointwise linearity of P and the ordinary directional-derivative product rule give real linearity in Y, function linearity in X, and X(fY)=X(f)Y+fXY. Thus [F2] makes an affine connection. Moreover, for tangent Y,Z, projection does not alter the dot product with either field, so the ordinary dot-product rule gives Xg(Y,Z)=g(XY,Z)+g(Y,XZ). Finally dY(X)dX(Y)=[X,Y] is tangent, whence XYYX=[X,Y]. Thus the connection is metric compatible and torsion free, and uniqueness in [F2] identifies it with the round Levi--Civita connection.

F1F2givenalgebra
2.1

For vTNS2 with r=v>0, put γv(t)=cos(tr)N+sin(tr)v/r. Then γv(t)=1, γv(0)=N, γ˙v(0)=v, and γ¨v=r2γv is normal to the sphere. Applying the along-curve definition in [F2] to the projected connection of step 1.1 gives Dtγ˙v=Pγv(γ¨v)=0, so γv is a geodesic. Its formula extends at v=0 by the constant curve, and uniqueness in [F3] yields expN(v)=cosrN+(sinr/r)v.

F2F3step 1.1algebra
3.1

By [F3], restrict expN to a sufficiently small ball Bρ(0)TNS2 on which it is a diffeomorphism, and use the supplied basis to form normal coordinates. Choose 0<r<min{ρ,π/2} and set x=re1, w=e2. Since xw=0, differentiating the formula of step 2.1 in the direction w gives d(expN)x(w)=(sinr/r)e2. This vector is exactly the second coordinate vector at q=expN(x) because the inverse normal-coordinate chart is expNEe. By [F4], sinr>sin0=0; and the mean value theorem gives c(0,r) with sinrsin0=rcosc. Strict decrease of cosine on [0,π] gives cosc<cos0=1, hence 0<sinr<r. Therefore the second coordinate vector has squared round length g22(q)=(sinrr)2<1.

F3F4step 2.1algebra
4.1

The metric coefficient in step 3.1 is not the Euclidean value 1, even though [F3] gives g22(N)=1 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 r>0; r=0 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.

A1F3step 3.1

Depends on

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