TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)

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.

Unweighted scalar geodesic X-ray injectivity on simple surfaces

Statement

Let $(M, g)$ be a compact, connected, nonempty smooth Riemannian surface with smooth boundary. Write $ν_{o u t}$ for its outward unit normal and use the curvature convention $R (A, B) C = \nabla_{A} \nabla_{B} C - \nabla_{B} \nabla_{A} C - \nabla_{[A, B]} C$ . Write $D_{t} J = \nabla_{\dot{γ}} J$ ; a Jacobi field along a unit-speed geodesic $γ$ is a smooth field $J$ satisfying $D_{t}^{2} J + R (J, \dot{γ}) \dot{γ} = 0$ . Assume $g (\nabla_{w} ν_{o u t}, w) > 0$ for every nonzero boundary-tangent vector $w$ , no nonzero Jacobi field on any positive-length unit-speed geodesic segment vanishes at both endpoints, and every maximal unit-speed geodesic starting in $M^{\circ}$ reaches $\partial M$ in finite forward and backward time. Set $S M = {(x, v) : x \in M, g_{x} (v, v) = 1}$ and $\partial_{+} S M = {(x, v) \in S M : x \in \partial M, g_{x} (v, - ν_{o u t}) > 0}$ . For a real-valued $f \in C_{c}^{\infty} (M^{\circ}, R)$ and $(x, v) \in \partial_{+} S M$ , let $γ_{x, v}$ be the unit-speed geodesic with initial data $(x, v)$ , let $τ_{+} (x, v)$ be its first positive boundary-exit time, and define

I_{0} f (x, v) = \int_{0}^{τ_{+} (x, v)} f (γ_{x, v} (t)) d t .

Then $I_{0} f = 0$ on $\partial_{+} S M$ implies $f = 0$ on $M$ . No orientability assumption on $M$ is required.

Statement references

Definition of simple surfaces and incoming geodesic data

Transport, Santaló, and index-form facts for simple surfaces

Pestov identity for geodesic data

Orientation-cover lifting of simple geometry and X-ray data

Facts & Assumptions

Given: A simple compact connected nonempty smooth Riemannian surface $M$ , a real scalar $f \in C_{c}^{\infty} (M^{\circ})$ , and zero boundary geodesic X-ray data $I_{0} f = 0$ .

[F1]

Simple surface and geodesic X-ray transform: simple means strictly convex boundary, no conjugate points, and finite forward/backward exit times; $I_{0} f$ is the integral of $f$ over each unit-speed boundary-to-boundary geodesic.

[F2]

The tangent orientation cover preserves simple-surface X-ray data: every connected component of the tangent orientation cover with pullback metric is compact, connected, oriented, and simple; its projection is a local isometry onto $M$ .

[F3]

The tangent orientation cover preserves simple-surface X-ray data: $I_{0, C} (f \circ π) (\tilde{z}) = I_{0, M} f (π (\tilde{z}))$ for every incoming state $\tilde{z}$ on a component $C$ .

[F4]

Surface geodesic flow, index form, and transport primitive: zero scalar data gives a smooth compactly supported transport primitive $u$ with $X u = - f$ and $u ∣_{\partial S M} = 0$ ; $V$ is tangent to $\partial S M$ .

[F5]

Pestov identity for geodesic data on a simple surface: for smooth real $u$ vanishing on the boundary of an oriented simple surface, $∥ V X u ∥^{2} = ∥ X V u ∥^{2} - (K V u, V u) + ∥ X u ∥^{2}$ .

[F6]

Surface geodesic flow, index form, and transport primitive: $d Σ = d V_{g} (x) d S_{x} (v)$ and Santaló's formula is $\int_{S M} h d Σ = \int_{\partial_{+} S M} μ \int_{0}^{τ_{+}} h (φ_{t} (z)) d t d Σ_{\partial}$ for continuous $h$ ; Riemannian volume density: in coordinates $d V_{g} = \sqrt{\det G_{x}} ∣ d x^{1} \dots d x^{n} ∣$ .

[F7]

Surface geodesic flow, index form, and transport primitive: $I_{γ} (Y, Y) = \int_{0}^{L} (∣ D_{t} Y ∣^{2} - g (R (Y, \dot{γ}) \dot{γ}, Y)) d t$ for endpoint-zero normal fields.

[F8]

Surface geodesic flow, index form, and transport primitive: the index form is positive for each nonzero endpoint-zero normal field.

[F9]

Fundamental theorem of riemannian geometry: the metric has a unique Levi-Civita connection.

[F10]

Levi civita connection: the Levi-Civita connection is metric-compatible and torsion-free.

[F11]

Curvature of an affine connection: $R (A, B) C = \nabla_{A} \nabla_{B} C - \nabla_{B} \nabla_{A} C - \nabla_{[A, B]} C$ .

[F12]

Riemann curvature four-tensor: $Rm (A, B, C, D) = g (R (A, B) C, D)$ .

Proof

1.1F1F2F3F4given

If $f = 0$ , the conclusion holds; assume $f \neq 0$ for contradiction. Let $C$ be any connected component of the tangent orientation cover of $M$ and let $\tilde{f} = f \circ π$ on $C$ . By [F2], $C$ is a compact oriented simple surface and $I_{0, C} \tilde{f} = 0$ . The transport conclusion of [F4] supplies $u \in C_{c}^{\infty} (S C^{\circ})$ with $X u = - \tilde{f}$ and $u = 0$ on $\partial S C$ .

2.1F4F5step 1.1

The vector field $V$ is vertical, so it differentiates functions along a fixed fibre and $V \tilde{f} = 0$ . Applying [F4] and [F5] to $u$ gives $0 = ∥ V X u ∥^{2} = ∥ X V u ∥^{2} - (K V u, V u) + ∥ X u ∥^{2}$ .

3.1F4F7F8F9F10F11F12step 1.1step 2.1

By [F4], $V u = 0$ on $\partial S C$ : $V$ is tangent to that boundary and $u$ vanishes there. Fix any incoming unit geodesic $γ : [0, L] \to C$ , and let $Q$ denote positive rotation by $90$ degrees on each oriented tangent plane. In a positive orthonormal frame $e_{1}, e_{2} = Q e_{1}$ , metric compatibility gives $\nabla_{A} e_{1} = ω (A) e_{2}$ and $\nabla_{A} e_{2} = - ω (A) e_{1}$ for a scalar one-form $ω$ . Using $(\nabla_{A} Q) e_{i} = \nabla_{A} (Q e_{i}) - Q \nabla_{A} e_{i}$ , we get $(\nabla_{A} Q) e_{1} = - ω (A) e_{1} + ω (A) e_{1} = 0$ and $(\nabla_{A} Q) e_{2} = - ω (A) e_{2} + ω (A) e_{2} = 0$ , so $\nabla Q = 0$ and $n (t) = Q \dot{γ} (t)$ is a parallel unit normal. The scalar function $w (t) = V u (γ (t), \dot{γ} (t))$ has $w (0) = w (L) = 0$ , and put $Y (t) = w (t) n (t)$ ; then $∣ D_{t} Y ∣^{2} = (w^{'})^{2}$ . The positive frame $(\dot{γ}, n)$ gives $K = g (R (\dot{γ}, n) n, \dot{γ})$ . The curvature definition gives $R (n, \dot{γ}) = - R (\dot{γ}, n)$ ; metric compatibility and the scalar commutator identity give $0 = A (B g (C, D)) - B (A g (C, D)) - [A, B] g (C, D) = g (R (A, B) C, D) + g (C, R (A, B) D)$ . Taking $A = \dot{γ}$ , $B = n$ , $C = \dot{γ}$ , and $D = n$ yields $g (R (\dot{γ}, n) \dot{γ}, n) = - K$ , hence $g (R (n, \dot{γ}) \dot{γ}, n) = K$ . Therefore $\int_{0}^{L} ((X V u)^{2} - K (V u)^{2}) (γ (t), \dot{γ} (t)) d t = I_{γ} (Y, Y) \geq 0$ , with equality allowed only when $Y = 0$ , by [F8].

4.1F6step 3.1algebra

Apply Santaló's formula from [F6] to the continuous function $(X V u)^{2} - K (V u)^{2}$ on $S C$ . Step 3.1 shows that its integral over each boundary-to-boundary geodesic is nonnegative; the incoming flux weight is positive. Hence $∥ X V u ∥^{2} - (K V u, V u) = \int_{S C} ((X V u)^{2} - K (V u)^{2}) d Σ \geq 0$ .

5.1F2F6step 1.1step 2.1step 4.1choose∎

Since $X u = - \tilde{f}$ , the remaining term in step 2.1 is $∥ X u ∥^{2} = ∥ \tilde{f} ∥^{2}$ . Under the standing assumption $f \neq 0$ , choose an interior point $x$ with $f (x) \neq 0$ ; continuity gives an open neighborhood on which $f$ is nonzero. By [F2], $π ∣_{C}$ is onto and a local diffeomorphism, so $\tilde{f}$ is nonzero on a nonempty open subset of $C$ ; [F6] supplies a smooth positive Liouville density, making $∥ \tilde{f} ∥^{2} > 0$ . This contradicts step 2.1 together with the nonnegative quantity in step 4.1. Therefore $f = 0$ .

Source locator

The source comparisons and item-specific dispositions are recorded in research/inverse-problems-knot-theory-all-109-2026-10-19-batch-38.coverage.json and the batch notes.

Depends on

Used by

Dependency tree · two levels

31 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

Gabriel P. Paternain, Mikko Salo, and Gunther Uhlmann, Geometric inverse problems, with emphasis on two dimensions (standard reference, not scraped)
Joonas Ilmavirta, Geometry of geodesics, full lecture notes (standard reference, not scraped)
Mikko Salo, On geometric inverse problems and microlocal analysis, author-hosted lecture notes (standard reference, not scraped)