CounterexampleConstruction: AI-generatedVerification: AI-generatedPipeline-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 cut point that is not conjugate because two minimizers arrive

Statement refuted

Refuted claim. Let $(M, g)$ be a complete, connected Riemannian manifold without boundary, let $p \in M$ , and let $q \in Cut (p)$ be a cut point of $p$ reached by a minimizing geodesic segment $γ$ from $p$ to $q$ . Then $p$ and $q$ are conjugate along $γ$ .

Facts & Assumptions

Given: The countable-choice axiom ${A C}_{ω}$ ; a circumference $L > 0$ ; the flat circle $C_{L} = R / (L Z)$ with period-coordinate metric $d x^{2}$ ; the base point $p = [x]$ ; the antipode $q = [x + L / 2]$ ; and the two opposite semicircles $γ_{+} (t) = [x + t]$ and $γ_{-} (t) = [x - t]$ on $[0, L / 2]$ .

[A1]

The exact choice assumption is ${A C}_{ω}$ of The Axiom of Countable Choice ( ${A C}_{ω}$ ). It is inherited only through the flat-circle example's maximal-geodesic, Hopf--Rinow and cut-time interfaces; the one-dimensional Jacobi calculation below uses no choice, and no full Axiom of Choice is used.

[F1]

In the flat circle $C_{L}$ the antipodal cut-time statement holds: both unit directions have cut time $L / 2$ , the cut locus is the single antipode $Cut (p) = {[x + L / 2]}$ , and at that cut point the two opposite semicircles are distinct minimizing geodesics (Cut locus of a point on a flat circle).

[F2]

The points $γ (a)$ and $γ (b)$ are conjugate along the affinely parametrized geodesic segment $γ : [a, b] \to M$ exactly when the space $K_{γ} (a, b) = {J \in J (γ) : J (a) = 0, J (b) = 0}$ of Jacobi fields vanishing at both endpoints contains a nonzero field (Conjugate points along a geodesic and their multiplicity).

[F3]

A smooth field $J$ along $γ$ is Jacobi exactly when it satisfies the Jacobi equation $D_{t}^{2} J + R (J, \dot{γ}) \dot{γ} = 0$ (Jacobi field).

[F4]

In a coordinate chart of a Riemannian metric, the Levi-Civita Christoffel symbols are given by the Christoffel formula; for the period chart of $C_{L}$ the metric matrix is the constant $1 \times 1$ matrix $(1)$ , so the formula gives $Γ^{1}_{11} = 0$ (Christoffel formula for the levi civita connection).

[F5]

In a coordinate chart the curvature components are recovered from the Christoffel symbols by the coordinate curvature formula; when the Christoffel symbols vanish identically in the chart, every component $R^{ℓ}_{k i j}$ vanishes, so the curvature operator $R$ is zero at each point of the chart (Coordinate formula for the curvature tensor).

[F6]

For a local frame $e$ with connection form $B (t) = ω_{γ (t)} (\dot{γ} (t))$ , a field $V (t) = e (γ (t)) v (t)$ has covariant derivative $D_{t} V = e (γ (t)) (v^{'} (t) + B (t) v (t))$ (Local frame formula for covariant differentiation along a curve); a section is parallel exactly when $D_{t} V = 0$ (Parallel section along a curve). In the period chart of $C_{L}$ the coordinate field $\partial_{x}$ is a frame along either semicircle, and its connection form vanishes because it is built from the symbols $Γ^{1}_{11} = 0$ of [F4].

Proof

technique · realize the two minimizing semicircles of the flat circle example, note that the flat connection makes the coordinate frame parallel and the curvature zero, and solve the resulting scalar Jacobi equation $j''=0$ with two endpoint zeros

1.1F1

By [F1], $q$ lies in $Cut (p)$ , and $γ_{+}$ and $γ_{-}$ are distinct minimizing geodesics from $p$ to $q$ with common length $L / 2$ . In a period chart containing the image of the closed semicircle, $γ_{+}$ lifts to the affine line $s \mapsto x + s$ and $γ_{-}$ lifts to $s \mapsto x - s$ ; each lift has constant unit coordinate speed on $[0, L / 2]$ .

1.2F4F5F6

In that period chart the metric coefficient is the constant $1$ , so [F4] gives vanishing Christoffel symbols, [F5] gives $R = 0$ at every point of the chart, and [F6] makes the coordinate field $\partial_{x}$ a parallel frame along the semicircle, since its connection form is built from those vanishing symbols.

2.1F3F5F6step 1.2

Let $J$ be a smooth vector field along $γ_{+}$ . On the chart domain write $J (t) = j (t) \partial_{x}$ for a smooth real function $j$ . As $\partial_{x}$ is parallel by step 1.2, the frame formula [F6] gives $D_{t} J = j^{'} \partial_{x}$ and $D_{t}^{2} J = j^{''} \partial_{x}$ , while the curvature term vanishes because $R = 0$ by step 1.2. Thus, by [F3], $J$ is a Jacobi field along $γ_{+}$ exactly when the scalar equation $j^{''} (t) = 0$ holds on $[0, L / 2]$ , whose solutions are $j (t) = a + b t$ with constants $a, b \in R$ .

3.1F3step 2.1algebra

Suppose $J$ is a Jacobi field along $γ_{+}$ with $J (0) = J (L / 2) = 0$ . By step 2.1, $j (t) = a + b t$ with $a = j (0) = 0$ and $a + b L / 2 = j (L / 2) = 0$ . Since $L / 2 > 0$ , the second equation forces $b = 0$ , hence $j = 0$ and $J = 0$ . The same calculation applies to $γ_{-}$ , whose chart lift $s \mapsto x - s$ has the same constant metric coefficient and the same vanishing symbols.

4.1F2step 3.1

Consequently $K_{γ_{+}} (0, L / 2) = {0}$ and $K_{γ_{-}} (0, L / 2) = {0}$ : the only Jacobi field along either minimizing semicircle vanishing at both endpoints is the zero field. By the conjugacy definition [F2], $p$ and $q$ are not conjugate along either semicircle.

5.1A1F1F2step 1.1step 4.1

Therefore $q$ is a cut point of $p$ , reached by the two distinct minimizing geodesics $γ_{+}$ and $γ_{-}$ , and it is not conjugate to $p$ along either of them; the claim in the Statement refuted is false. Boundary and choice audit: the two semicircles have positive length $L / 2$ , so both endpoint times are distinct and the endpoint zeros are genuine; the circle is one-dimensional and nonempty, with no degenerate interval and no constant geodesic among the two witnesses; the zero field is the only endpoint-vanishing Jacobi field and it cannot witness conjugacy by [F2]. Exactly ${A C}_{ω}$ is used, and only to invoke the flat-circle example's cut-time interface by [A1]; the Jacobi computation selects nothing. The refuted claim is a one-way implication, so no converse case arises.

$□$

Source locator

Lee, Riemannian Manifolds: An Introduction to Curvature, Chapter 10, printed p.190 / PDF label P206, lines 7559–7571, observes that the flat cylinder has no conjugate points and that wrappings longer than halfway stop minimizing; that geometry is realized here on the flat circle, and the local nonconjugacy calculation is carried out rather than quoted. Datar, Lectures on Riemannian Geometry, Appendix C.14.2, printed p.278 / PDF labels P284–285, lines 14021–14050, states Klingenberg's lemma with an exercise outline relating nonconjugate cut points to two minimizing geodesics; the explicit circle witness above does not use that exercise as a proof.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

63 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 (2025) (standard reference, not scraped)