ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-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.

A compactly supported bump remains uniquely determined from limited angles

Example

Let $Θ \subset S^{1}$ be a nonempty proper open antipodally symmetric set whose complement contains a nonempty open arc. Write $θ^{⊥} = (- θ_{2}, θ_{1})$ and define the line Radon integral by $R g (θ, s) = \int_{R} g (s θ + t θ^{⊥}) d t$ using the compact-support Riemann integral in $t$ . Choose a smooth function $ψ$ supported in $B_{1} (0)$ and equal to one on ${\overline{B}}_{1 / 2} (0)$ . For every $h \in C_{c}^{\infty} (B_{1} (0); C)$ , equality of the restricted line data $R h (θ, s) = R ψ (θ, s)$ for all $θ \in Θ$ and $s \in R$ forces $h = ψ$ . The Fourier-Laplace transforms of these compactly supported functions are entire in each complex frequency coordinate, so their agreement on the measured open wedge determines their values at every real frequency. In particular, $R ψ$ is not identically zero.

Example references

Measured Fourier wedge and blind directions

Compact-support entire Fourier-Laplace transform

Choice-free compact-support uniqueness from an open set of angles

Mikko Salo, On geometric inverse problems and microlocal analysis, §2.1

Venkataswaran P. Krishnan and Eric Todd Quinto, Microlocal Analysis in Tomography, §1.3.2

Facts & Assumptions

Given: The set $Θ$ , a smooth bump $ψ$ supported in $B_{1} (0)$ and equal to one on ${\overline{B}}_{1 / 2} (0)$ , and a compactly supported smooth function $h$ with the same restricted line data as $ψ$ .

[F1]

Visible covectors for limited-angle data: the Fourier wedge of measured line normals is $W_{Θ} = {σ θ : θ \in Θ, σ \neq 0}$ , a nonempty open sector when $Θ$ is nonempty and open.

[F2]

A smooth bump between concentric Euclidean balls: a smooth compactly supported function equal to one on a smaller concentric ball and supported in a larger ball exists.

[F3]

The compact-support Fourier-Laplace transform is entire in each coordinate: the compact-support Riemann Fourier-Laplace transform is entire in each coordinate and restricts to the usual compact-support Fourier transform on real frequencies.

[F4]

The Fourier-slice identity for the Euclidean Radon transform: with the compact-support Riemann line-integral convention, the Fourier transform of Radon data equals the object Fourier transform on the ray $σ θ$ .

[F5]

Compactly supported smooth functions are unique from any open set of Radon angles: zero limited-angle data for a compactly supported smooth function force that function to vanish everywhere, by the choice-free analytic-continuation argument.

Verification

technique · direct

1.1F2givenconstruct

The ball $B_{1} (0)$ contains a smaller concentric ball, so [F2] supplies a bump with the stated support and plateau. It is nonzero because it equals one on the nonempty inner ball.

1.2F1F3F4F5given

If $h$ has the same restricted data as $ψ$ , linearity of the line integral gives $R (h - ψ) (θ, s) = 0$ for every measured pair. By [F4], the Fourier transforms of $h$ and $ψ$ agree on $W_{Θ}$ ; [F3] identifies these values as restrictions of their coordinate-entire Fourier-Laplace transforms. Applying [F5] to the compactly supported difference $h - ψ$ gives $h - ψ = 0$ everywhere.

2.1F5step 1.1algebra∎

If the data of $ψ$ were zero, [F5] would imply $ψ = 0$ , contradicting its value one on ${\overline{B}}_{1 / 2} (0)$ . Thus its restricted data are nonzero while uniquely determining it in the stated compact-support class.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

Mikko Salo, On geometric inverse problems and microlocal analysis, §2.1 (standard reference, not scraped)
Venkataswaran P. Krishnan and Eric Todd Quinto, Microlocal Analysis in Tomography (standard reference, not scraped)