Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-09
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.

Finite ambient partitions near compact sets

Statement

Under the page measure convention, if a finite family of open sets Uj⊂Rn covers compact K, there are smooth nonnegative χj with compact support in Uj such that ∑jχj=1 on a neighborhood of K. These are ambient smooth functions, also when K is only a C1 hypersurface.

Facts & Assumptions

Given: A compact Euclidean set K and a finite open cover of K, with the ambient smooth-step and bump conventions in the statement.

[F1]

Nested balls admit smooth bumps with a strict compact support margin. (Compactly supported scaled Euclidean bumps).

[F2]

Compact Euclidean sets admit finite subcovers. (Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[F3]

The standard step has values zero for inputs at most zero and one for inputs at least one. (The standard smooth step function).

Proof

1.1

If K is empty take all chi_j zero. Otherwise consider all pairs of concentric balls with positive rational radii r<R whose closed outer ball lies in some U_j and whose inner ball meets K. Their inner balls cover K, because every point has a positive neighborhood inside a member of the given open cover. Compactness (F2) retains finitely many such inner balls covering K. F1 gives corresponding bumps b_l, equal to one on those inner balls and compactly supported in their assigned U_j.

givenF1F2
2.1

Put s=∑lbl. Then s is smooth with compact support, and s at least one on K. Define θ=σ(4s−1). By F3 theta=1 wherever s at least one half, a neighborhood of K, and its support lies in the compact set where s at least one quarter. On s>0 put fl=θbl/s, and extend by zero on s=0. Because theta vanishes on s at most one quarter, this extension is smooth. Each f_l has compact support in the assigned U_j, is nonnegative, and their sum is theta.

step 1.1F3algebra
3.1

For each j sum f_l over the finitely many bumps assigned to U_j, using zero if no bump is assigned. These sums are the required chi_j: their supports are finite unions of compact subsets of U_j, and their total is theta=1 near K. Since all constructions took place in the ambient Euclidean space, no differentiability of K was required.

step 2.1algebra∎

Source notes

Hunter, §1.9.2 Theorem 1.31, printed pp. 12–13. A finite normalized-bump construction is supplied here.

Depends on

Used by

Dependency tree · two levels

46 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