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

Extension by zero for distributions with ambient closed support

Statement

Let $F$ be closed in $R^{n}$ , let $F \subseteq Ω$ with $Ω$ open, and let $u \in D^{'} (Ω)$ have support contained in $F$ . Then there is a unique distribution $\tilde{u}$ on $R^{n}$ restricting to $u$ on $Ω$ and with support contained in $F$ . No compactness of $F$ is required. The assertion holds in ZF and uses ambient closedness, not merely relative closedness in $Ω$ .

Facts & Assumptions

[F1]

Compatible distributions on an arbitrary open cover glue uniquely (Distributions form a sheaf).

[F2]

A distribution vanishes on the complement of its support, and support is the complement of its largest vanishing open set (Support of a distribution).

Proof

Given: $F, Ω, u$ as in the statement.

1.1

The sets $Ω$ and $R^{n} ∖ F$ are open and cover $R^{n}$ because $F \subseteq Ω$ . On their overlap $Ω ∖ F$ , the distribution $u$ vanishes by F2 since its support is contained in $F$ . Hence $u$ and the zero distribution on $R^{n} ∖ F$ are compatible.

givenF2

2.1

F1 glues them to $\tilde{u}$ . It restricts to $u$ and is zero on $R^{n} ∖ F$ , so F2 gives support contained in $F$ . Any other extension with this support must have the same two restrictions, and uniqueness in F1 makes it equal to $\tilde{u}$ .

step 1.1F1F2

3.1

If $F$ is empty, F2 makes $u = 0$ and the extension is zero; if $Ω = R^{n}$ , the extension is $u$ . Ambient closedness ensures that the second member of the cover is open. The proof therefore supplies no extension claim across a boundary when only relative closedness is known. There is no choice use beyond the choice-free sheaf theorem. $□$

step 2.1F1F2

Depends on

Used by

Smooth functions are weakly dense in distributions Corollary

Dependency tree · two levels

6 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

Razvan Gelca, Functional Analysis (standard reference, not scraped)