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

Antipodal points on a round sphere have many minimizing geodesics

Statement refuted

The assertion that a pair of points joined by a minimizing geodesic must have a unique minimizing geodesic is false. Assume ACω. For every n≥2, every p on the round unit sphere Sn is antipodal to −p, and p and −p are joined by infinitely many distinct minimizing half-great-circles. More precisely, every unit u∈TpSn gives one such curve

γu(t)=cos⁡t p+sin⁡t u,0≤t≤π.

Facts & Assumptions

Given: An integer n≥2, a point p∈Sn, and the round metric induced by the Euclidean inner product.

[A1]

The Axiom of Countable Choice (ACω) is the assumed ACω. It is used only when Hopf–Rinow theorem supplies a globally minimizing geodesic; the explicit family of half-great-circles uses no choice principle.

[F1]

For F(x)=⟨x,x⟩, dFp(v)=2⟨p,v⟩ is nonzero at every unit p. Hence A regular level set is an embedded submanifold gives Sn its smooth boundaryless n-manifold structure and The tangent space of a regular level set is the kernel gives TpSn=p⊥. Inclusion is an immersion, so Pullback of a riemannian metric is riemannian exactly for immersions makes the restricted Euclidean inner product its round metric. Instantiating For n≥2, the sphere Sn−1 is path-connected and connected in Rn+1 shows that Sn is path connected, and Every path-connected space is connected, and every path component lies inside a component makes it connected.

[F2]

In a chart at p, Coordinate derivations form a basis of the tangent space supplies a basis of the n-dimensional tangent space. Since n≥2, applying Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans to its first two vectors gives fixed orthonormal vectors u1,u2∈TpSn.

[F3]

Great circles as round-sphere geodesics proves that all maximal round-sphere geodesics, constant or nonconstant, are defined on R. It also proves that for each unit u∈TpSn, the displayed γu is a unit-speed geodesic. Thus the round sphere is geodesically complete.

[F4]

Under [A1], Hopf–Rinow theorem says that a nonempty, connected, boundaryless, geodesically complete Riemannian manifold has a minimizing geodesic between every two points. Riemannian distance is a metric gives separation and nonnegativity for its Riemannian distance.

[F5]

Riemannian speed and length computes the length of a unit-speed curve on [0,π] as π, and Riemannian distance on a connected manifold defines distance as the infimum of the lengths of piecewise-smooth joining curves. Signs, monotonicity intervals, and ranges of sine and cosine says that cosine is strictly decreasing on [0,π], while Quarter-turn values and shifts by pi/2 and pi gives cos⁡π=−1, sin⁡π=0, cos⁡(π/2)=0, and sin⁡(π/2)=1.

Counterexample

technique · explicit family and distance comparison
1.1A1F1F3F4

The point p is not equal to −p: equality would give p=0, contrary to ∣p∣=1. By [F1] and [F3], the round sphere satisfies all the geometric hypotheses of [F4]. Hence [F4], under [A1], supplies a minimizing geodesic η:[0,1]→Sn from p to −p with constant speed L=d(p,−p)>0 and length L.

1.2F2F3F5

Fix any unit u∈TpSn; such a vector exists because [F2] supplies u1. By [F3] and [F5], γu is a geodesic from γu(0)=ptoγu(π)=−p of length π. Therefore the definition of Riemannian distance gives L=d(p,−p)≤π. The calculation applies to every unit u.

1.3F2algebra

For each m∈N, define um=u1+mu21+m2. Orthonormality gives ∣um∣=1. If um=uk, comparison of the nonzero u1 coefficients and then of the ratios of the u2 and u1 coefficients gives m=k. Hence (um)m∈N is an infinite family of distinct unit tangent vectors. This construction uses the two fixed vectors from [F2], not a choice of a vector from each member of a family.

2.1F3F5step 1.1step 1.2

Apply the explicit great-circle formula [F3] to the nonconstant geodesic η, based at t=0. Its speed is L, so there is a unit w∈TpSn such that η(t)=cos⁡(Lt)p+sin⁡(Lt)w. Taking the Euclidean inner product of the endpoint equality −p=η(1) with p, and using w⊥p, gives cos⁡L=−1. Steps 1.1--1.2 put L in (0,π]. Cosine is strictly decreasing on [0,π] and cos⁡π=−1 by [F5], so L=π. Thus d(p,−p)=π.

3.1F5step 1.2step 2.1step 1.3

Since the unit vector in step 1.2 was arbitrary, steps 1.2 and 2.1 show that every γu has length π=d(p,−p) and is globally minimizing. In particular this holds for every um. Moreover [F5] gives γum(π/2)=um. The distinctness in step 1.3 therefore makes these curves distinct. This is an explicit infinite collection of minimizing half-great-circles with the same two endpoints and proves the claimed failure of uniqueness.

4.1A1F2F4F5step 1.1step 1.3step 3.1∎

The lower-dimensional cases n=0,1 lie outside the quantified claim: the construction of an infinite family in step 1.3 specifically requires the two orthonormal tangent directions that [F2] obtains from n≥2. The zero-distance case cannot occur because p≠−p and the Riemannian distance is a metric; the parameter endpoints 0,π/2,π were evaluated explicitly. No empty-manifold case arises because p is given, and there is no iff assertion. Assumption [A1] is spent exactly in step 1.1 through Hopf--Rinow and nowhere in the explicit family.

Source locator

  • Datar, Proposition 15.3.1 and its complete proof, printed pp. 117--118 (PDF pp. 125--126), identifies round-sphere geodesics with great circles.
  • Datar, Theorem 19.2.1 and its proof, printed pp. 141--144 (PDF pp. 149--152), supplies the Hopf--Rinow equivalences and a minimizing geodesic. The calculation d(p,−p)=π and the explicit infinite family are derived above rather than imported from a citation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

95 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