LemmaStatement: AI-adaptedProof: 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.

Smooth boundary tests separate locally integrable traces

Statement

Assume Countable Choice. Let $(M, g)$ be a compact smooth Riemannian manifold with smooth boundary, let $T > 0$ , and let $Σ = (0, T) \times \partial M$ . Write $d S_{g}$ for the Riemannian volume density of the metric restricted to $T \partial M$ , and give $Σ$ the product density $d t d S_{g}$ . If a measurable function $f$ is locally integrable in every smooth product chart of $Σ$ and $\int_{Σ} f ψ d S_{g} d t = 0 for every ψ \in C_{c}^{\infty} (Σ),$ then $f = 0$ almost everywhere on $Σ$ .

Statement references

The Axiom of Countable Choice ( ${A C}_{ω}$ )

Riemannian metric and riemannian manifold

Riemannian volume density

Riemannian Green identity, boundary trace, and wave lifting

Locally integrable functions embed in distributions

Assuming countable choice, every second countable space is Lindelöf

Facts & Assumptions

Given: Countable Choice, the product boundary manifold $Σ$ with its smooth positive Riemannian density $d S_{g} d t$ , and a locally integrable $f$ whose pairing with every smooth compactly supported test is zero.

[A1]

Countable Choice allows passage from the second-countable product chart basis to a countable atlas and union of its chart-null exceptional sets. (The Axiom of Countable Choice ( ${A C}_{ω}$ ), Assuming countable choice, every second countable space is Lindelöf)

[F1]

In a boundary chart $y = (y^{1}, \dots, y^{n - 1})$ , the restricted metric has smooth positive-definite matrix $G_{\partial, a b} = g (\partial_{y^{a}}, \partial_{y^{b}})$ . By the Riemannian volume-density formula, $d S_{g} = \sqrt{\det G_{\partial}} ∣ d y^{1} \dots d y^{n - 1} ∣$ ; this coefficient is smooth and strictly positive, and multiplying by $d t$ gives the product chart density. (Riemannian metric and riemannian manifold, Riemannian volume density)

[F2]

A locally integrable function on a Euclidean open set whose regular distribution is zero vanishes almost everywhere, under Countable Choice. (Locally integrable functions embed in distributions)

Proof

1.1F1F2givenconstruct

Fix a product coordinate chart $V \subset Σ$ with coordinates $(t, y)$ and write $d S_{g} d t = m (t, y) d t d y$ , where $m$ is smooth and strictly positive by [F1]. For every $φ \in C_{c}^{\infty} (V)$ , extending it by zero gives a global test $ψ \in C_{c}^{\infty} (Σ)$ . The assumed pairing then says $\int_{V} (f \circ κ^{- 1}) (t, y) m (t, y) φ (t, y) d t d y = 0.$ The function $(f \circ κ^{- 1}) m$ is locally integrable; its regular distribution is therefore zero, so [F2] gives $(f \circ κ^{- 1}) m = 0$ almost everywhere on $V$ . Positivity of $m$ implies $f = 0$ almost everywhere on $V$ .

2.1A1F1step 1.1given∎

Second countability and [A1] provide an at-most-countable cover of $Σ$ by such product coordinate charts. Each chart-null exceptional set is null for the induced product measure because the chart density is smooth and positive. The countable union remains null under Countable Choice, and step 1.1 shows $f = 0$ outside it. Hence $f = 0$ almost everywhere on all of $Σ$ .

Depends on

Used by

A potential perturbation beyond the two-trip distance is invisible before time T Example

Dependency tree · two levels

24 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

Medet Nursultanov and Lauri Oksanen, Introduction to inverse problems for hyperbolic PDEs (full lecture notes, arXiv:2311.06020v2) (standard reference, not scraped)
Mikko Salo, On geometric inverse problems and microlocal analysis (full author lecture notes, arXiv:2312.08123v1) (standard reference, not scraped)