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.

Distributions form a sheaf

Statement

For an open inclusion VΩ, restriction of a distribution is defined by testing on the smooth zero extension of a test in D(V). These restrictions are distributions and compose as restrictions do for functions. For any open cover (Uj)jJ of Ω, distributions ujD(Uj) agreeing on every overlap glue to a unique uD(Ω). This holds in ZF for an arbitrary index set J.

Facts & Assumptions

[F1]

Distributions are complex-linear continuous test functionals (Distribution).

[F2]

Continuity is equivalent to a finite-order estimate on each fixed compact support (Local finite order characterization of distributions).

[F3]

Multiplication by a smooth function preserves tests; its derivative estimates follow from the finite product rule used to justify Multiplication of a distribution by a smooth function.

[F4]

Every open cover has an at most countable locally finite smooth partition with compact supports, each support contained in some cover member, without selecting labels (Test function cutoffs and euclidean localization).

Proof

Given: the cover and compatible family in the statement.

1.1

For VΩ and φD(V), its support is compactly inside V, so extension by zero is smooth on Ω. On each compact KV its derivative seminorms are unchanged. The bound of F2 for u on K therefore gives that bound for its restriction; this proves restriction is a distribution. Testing successive zero extensions proves composition and identity of restrictions.

givenF1F2
2.1

Take the partition (η) of F4. For each and each test φ, the test ηφ has compact support inside any member containing suppη. Its evaluation by that member's distribution is independent of the member: two such members overlap on its support, so compatibility applies. Denote this uniquely specified number by v(φ); this definition selects no labels. Set u(φ)=v(φ). Only finitely many partition supports meet suppφ: local finiteness provides neighborhoods meeting finitely many supports, and a finite subcover of the compact support suffices. Thus the sum exists. Applying the same finite set to the union of two test supports proves complex linearity.

step 1.1givenF4
3.1

Fix compact KΩ. Only finitely many partition supports meet K. For these finitely many indices take containing cover members and their finite-order bounds on the compact supports of the corresponding η. Finite choices are provable by finite induction in ZF. Let m be the maximum of their orders, or zero if none occur. The finite product rule gives [step 2.1, F2, F3] pm(ηφ)2mmaxγmsupsuppηγη pm(φ)(φDK), where derivatives of φ vanish off K. Summing the finitely many bounds yields u(φ)CKpm(φ) with finite CK. Hence u is a distribution by F2.

step 2.1F2F3
4.1

If φD(Uj), every nonzero summand is evaluated on a test with compact support in Uj and a containing cover member. Compatibility makes it uj(ηφ). The finite sum is uj(φ) since η=1. Thus the restrictions are the prescribed ones. If a distribution w restricts to zero on each Uj, the same finite decomposition gives w(φ)=w(ηφ)=0 for every test. Applying this to the difference of two glued distributions proves uniqueness, and therefore independence of the partition. For the empty cover of the empty domain the sum defines the zero distribution and uniqueness still holds.

step 3.1step 2.1step 1.1F1F4

Depends on

Used by

Dependency tree · two levels

9 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