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.

Zero-integral compactly supported top forms on Euclidean space have compactly supported primitives

Statement

Let n≥1 and let ω∈Ωcn(Rn) satisfy ∫Rnω=0, with the standard orientation and the finite-localization integral. There exists η∈Ωcn−1(Rn) with dη=ω. For n=0, the integral of a form on the single point is its value, so zero integral means ω=0 and the zero element of Ωc−1=0 is the only primitive. The construction in positive dimension is by explicit finite-dimensional induction and requires no choice axiom.

Facts & Assumptions

[F1]

Integration descends to compactly supported top de Rham cohomology fixes the choice-free boundaryless integral convention and compact-primitive interpretation.

[F2]

A smooth bump between concentric Euclidean balls gives a smooth 0≤ρ≤1 on R that is one on [−1/2,1/2] and supported in (−1,1).

[F3]

Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm gives linearity, monotonicity, interval-slice additivity and the absolute integral bound.

[F6]

Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable identifies the compact rectangular integral with the iterated integral over its last coordinate.

[F7]

The de Rham complex and pullback extend to manifolds with boundary supplies the local coefficient differential formula and its signed wedge rule.

[F10]

Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous gives uniform continuity of each continuous derivative on a compact rectangle.

[F11]

Every continuous function on a closed nondegenerate rectangle in Rm is Riemann integrable gives integrability of all smooth coefficient and derivative restrictions on these rectangles.

[F12]

Finite chart localization gives choice-free integration and compact Stokes identifies the integral of a Euclidean chart-supported top form with its coefficient integral and gives locality.

[F13]

Change of variables for an injective C1 map on a compact Jordan set gives the invertible affine interval substitution, with the absolute determinant and oriented-interval sign treated separately.

Proof

Given: ω=f dx1∧⋯∧dxn of compact support and integral zero. We construct its compact primitive by induction on positive n, with the separate dimension-zero convention in the statement.

1.1F5F7F8F9F11F12given

By [F9], the increasing open cubes have a finite subfamily covering supp⁡f; take R>1 larger than the largest radius in such a finite family. Thus f vanishes outside a compact box strictly inside [−R,R]n. By [F11] and [F12], the given integral is the ordinary integral of f on that rectangle, and all sections used below are integrable. If n=1, put a(x)=∫−Rxf(t) dt using oriented interval integrals. The fundamental theorem gives a′=f; repeated differentiation makes a smooth. It vanishes for x≤−R, because the integrand is zero there, and for x≥R, because the total integral is zero. Hence η=a has compact support by [F8] and dη=f dx.

1.2F2F3F11

Fix one bump ρ from [F2]. By [F3], 1≤c:=∫−11ρ(t) dt≤2, since ρ=1 on the middle interval of length one and is between zero and one elsewhere. Integrability follows from [F11]. Put b=ρ/c. It is smooth, has compact support in (−1,1) and has integral one. This normalization uses one bump and an explicit positive integral bound, not a global positivity theorem or an infinite choice.

2.1F3F4F5F10F11F13step 1.1step 1.2

Let n≥2, write x′=(x1,…,xn−1), t=xn, and define f0(x′)=∫−RRf(x′,s) ds,g(x′,t)=f(x′,t)−f0(x′)b(t),h(x′,t)=∫−Rtg(x′,s) ds. The function f0 is smooth: repeatedly apply [F4] in each one parameter coordinate on smaller closed parameter rectangles. Each resulting derivative is the integral of the corresponding derivative of f. Joint continuity follows from [F10] and [F3], since the change of that integral is bounded by 2R times the uniform change of the integrand. Hence g is smooth. For joint smoothness of h, use h(x′,t)=(t+R)∫01g(x′,−R+u(t+R)) du. This formula is valid also at t=−R and for t<−R, by [F13] for t≠−R (reverse the interval when t<−R); at t=−R both sides are zero. On any compact parameter neighbourhood the integrand and all parameter derivatives are continuous on its product with [0,1]; repeated [F4], [F10] and the same bound prove all joint derivatives continuous. Finally [F5] gives ∂th=g.

3.1F3F6F8F11F12step 1.1step 1.2step 2.1

The function f0 vanishes outside [−R,R]n−1 and has compact support by [F8]. For every x′, ∫−RRg(x′,s) ds=f0(x′)−f0(x′)∫−RRb(s) ds=0, since R>1 and b is supported in (−1,1). Therefore h vanishes when t≤−R or t≥R. It also vanishes outside the stated x′ box, because both f and f0 vanish there. Thus h has closed support inside [−R,R]n and is compactly supported by [F8]. By [F6] with all smooth sections and by [F12], ∫Rn−1f0 dx′=∫Rnf dx=0.

4.1F7step 2.1step 3.1

Apply the induction hypothesis in dimension n−1 to the compactly supported top form f0 dx1∧⋯∧dxn−1. It gives a compactly supported (n−2)-form γ with dγ=f0 dx1∧⋯∧dxn−1. Let π:Rn→Rn−1 be projection and put η=(−1)n−1h dx1∧⋯∧dxn−1+π∗γ∧b(t) dt. For the first summand, every x′ derivative repeats a differential and vanishes; moving dt past n−1 factors cancels (−1)n−1, so its derivative is g dx1∧⋯∧dxn. For the second, [F7] gives π∗dγ∧b dt, since d(b dt)=b′ dt∧dt=0. Its coefficient is f0b. Thus dη=(g+f0b) dx1∧⋯∧dxn=ω.

5.1F8F9step 3.1step 4.1

The first summand of η is supported in [−R,R]n by step 3.1. The second is supported in supp⁡γ×[−1,1]. By [F9] the first factor is bounded; the product support is closed and bounded, so [F8] makes it compact. Their finite union is bounded, and the closed support of the sum lies in it, again compact by [F8]. This completes the induction with an actual compact primitive; projection pullback by itself was not claimed to preserve compact support.

6.1F1F2F8F12step 1.1step 1.2step 3.1step 4.1step 5.1∎

At n=0, [F1] and [F12] identify the integral on the standard oriented point with its scalar value; zero integral forces zero, the derivative of the zero negative-degree element. For zero input the construction gives f0=g=h=0 and one may take γ=0, hence η=0. The interval endpoints, zero fibres and vanishing support were checked in steps 1.1 and 3.1. The induction chooses one normalized bump and, at each of finitely many dimensions for a given input, one previously established primitive. There is no choice of primitives over an infinite family and no AC.

Depends on

Used by

Dependency tree · two levels

121 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