Alphabeta Math
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.

Sequential convergence in test function space

Statement

For tests φj,φ∈D(Ω), φj→φ in the LF topology if and only if the supports of φj eventually lie in one compact K⊆Ω and ∂αφj→∂αφ uniformly on Ω for every multi-index α. Equivalently one compact contains all their supports and that of the limit, and convergence holds in its fixed-support topology. This is a sequence criterion, in ZF.

Facts & Assumptions

[F1]

The LF topology induces exactly the derivative-seminorm topology on each fixed-support space, and its inclusion is continuous (Test function lf topology universal property).

[F2]

A convergent sequence with its limit is bounded; a bounded set of tests has common compact support (Bounded test function sets have common compact support).

Proof

Given: a sequence of tests and a test φ.

1.1givenF1F2

If φj→φ in the LF topology, F2 places the sequence and limit in one DK. Convergence in the subspace topology follows directly: any subspace neighborhood of φ is the intersection with an ambient neighborhood, which eventually contains the sequence. By F1, pm(φj−φ)→0 for every m. Since derivatives vanish off K, this gives uniform convergence of every derivative on Ω.

2.1step 1.1givenF1

Conversely suppose eventual common support and the stated uniform convergence. For x∉K, the eventual values φj(x) are zero, so φ(x)=0; since K is closed, its support is contained in K. The finite union L of K and the finitely many initial test supports is compactly inside Ω and contains every support. For each m, uniform convergence of the finitely many derivatives through order m gives pm,L(φj−φ)→0. F1 first yields convergence in DL, then LF convergence by the continuous inclusion.

3.1step 2.1step 1.1

These arguments also prove the stated equivalent all-support formulation. Empty Ω and eventually zero sequences satisfy the same reasoning; no compactness extraction or chosen subsequence is used. The finite initial union is essential to passing from eventual to all-support language. □

Depends on

Dependency tree · 2 levels

Sources