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

Test function cutoffs and euclidean localization

Statement

In ZF, for compact K⊆Ω⊆Rn with Ω open, there is χ∈Cc∞(Ω) with 0≤χ≤1 and χ=1 on a neighborhood of K. Every open cover of Ω admits an at most countable locally finite smooth partition of unity with compact supports, each support contained in some cover member. Subordination here asserts existence of such a member for each support; it does not select cover labels.

Facts & Assumptions

[F1]

The explicit smooth cutoff b equals one on the closed unit ball, vanishes outside the radius-two ball, and satisfies 0≤b≤1; translated dilates have the stated derivative scaling (Explicit compactly supported smooth cutoffs).

[F2]

Smoothness and multi-index notation are as in Ck maps and multi-index derivative notation in Euclidean space, applied componentwise.

Proof

Given: the compact set and open set of the first assertion; an open cover U of Ω for the second.

1.1givenF1F2

For each point of K, there is a rational center q and positive rational r such that the point belongs to B(q,r) and B‾(q,2r)⊆Ω. These inner balls cover K, so a finite list suffices by compactness. Put bj(x)=b((x−qj)/rj) and χ=1−∏j(1−bj). Then χ is smooth, lies in [0,1], equals one on the union of the inner balls, and has support in the finite union of the compact outer balls inside Ω. For K=∅ take the empty product and χ=0.

2.1step 1.1algebra

For nonempty Ω, set Kj={x:∣x∣≤j, dist⁡(x,Rn∖Ω)≥1/j} for j≥1, interpreting distance to the empty set as infinity; set K0=K−1=∅. These are compact subsets of Ω, Kj⊆int⁡Kj+1, and their interiors cover Ω. Closedness follows from continuity of distance (its absolute difference is at most the distance of the two points), and boundedness gives compactness. The shell Hj=Kj∖int⁡Kj−1 is compact and lies in the open set Gj=int⁡Kj+1∖Kj−2.

3.1step 2.1given

Fix an enumeration of rational center/radius pairs and a coding of finite lists by natural numbers. For each j, consider pairs with B‾(q,2r)⊆Gj and with this closed ball contained in some U∈U. Their inner balls cover Hj: at any shell point openness of Gj and of one cover member gives a sufficiently small ball, then a rational center and radius. Compactness gives a finite subcover. Select the least code of a finite list that covers Hj, taking the empty list for an empty shell. This is a specified function of j, not Countable Choice.

4.1step 3.1F1F2

Form the corresponding translated dilates bj,k of F1. Their supports lie in Gj, and each support lies in some cover member. This family is locally finite: a point has a neighborhood inside some KN, and supports with j≥N+2 miss KN, while only finitely many balls occur at each of the finitely many earlier stages. Every point belongs to some shell, so s=∑j,kbj,k is everywhere positive. The sum is locally finite and smooth; hence ηj,k=bj,k/s are smooth, nonnegative, have compact support in the same outer balls, and sum to one. The double index is countable. For empty Ω use the empty family. These constructions choose no cover labels and no arbitrary sequence of witnesses. □

Depends on

Dependency tree · 2 levels

Sources