TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Constant coefficient differential operators become polynomial multipliers

Statement

Assume Countable Choice. Let $P (z) = \sum_{α \in A} a_{α} z^{α}$ be a complex polynomial in $n$ variables, with $A$ finite, and put $P (\partial) = \sum_{α \in A} a_{α} \partial^{α}$ . Then, for every $u \in S^{'} (R^{n})$ ,

$F (P (\partial) u) = P (2 π i ξ) F u$

in $S^{'} (R^{n})$ .

Facts & Assumptions

Given: Countable Choice, a finite polynomial $P$ , and $u \in S^{'} (R^{n})$ .

[F1]

For every multi-index $α$ , $F (\partial^{α} u) = (2 π i ξ)^{α} F u$ (Fourier differentiation and multiplication identities on tempered distributions).

Proof

technique · finite linearity

1.1F1algebra

Fourier transformation, distributional differentiation, and finite addition are complex-linear, giving the following finite expansion.

$F (P (\partial) u) = \sum_{α \in A} a_{α} F (\partial^{α} u) .$

[F1, algebra]

2.1F1step 1.1∎

Substitute [F1] into the finite sum from step 1.1 and factor the common distribution $F u$ to obtain $\sum_{α} a_{α} (2 π i ξ)^{α} F u = P (2 π i ξ) F u$ . This includes constant and zero polynomials. The statement is only an algebraic equivalence: it asserts no division by $P (2 π i ξ)$ and no existence or regularity theorem for a PDE. Countable Choice is used only through [F1].

Depends on

Used by

Fundamental solution by division of a fourier symbol Example

Dependency tree · two levels

11 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

Semyon Dyatlov, Lecture notes for 18.155 (2022) (standard reference, not scraped)