PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-07

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.

Positivity of the oriented integral

Statement

Let $ω \in Ω_{c}^{n} (M)$ be nonnegative on the positive determinant ray of an oriented smooth manifold. Then $\int_{M} ω \geq 0$ , and $ω \neq 0$ implies $\int_{M} ω > 0$ .

Facts & Assumptions

[F1]

Linearity and additivity of the form integral: For compactly supported smooth top forms $ω, η$ on an oriented $M^{n}$ and $a, b \in R$ , $\int_{M} (a ω + b η) = a \int_{M} ω + b \int_{M} η .$ Also $\int_{M} ω = \sum_{C} \int_{C} ω ∣_{C}$ , where $C$ ranges over connected components with their restricted orientations; only finitely many meet $supp ω$ .

[F2]

Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ : Let $Q = \prod_{j < m} [a_{j}, b_{j}]$ be nondegenerate. For integrable $f, g : Q \to R$ and scalars $α, β$ , the function $α f + β g$ is integrable and its integral is $α \int_{Q} f + β \int_{Q} g$ . If $f \leq g$ , then $\int_{Q} f \leq \int_{Q} g$ . Also $∣ f ∣$ is integrable and $∣ \int_{Q} f ∣ \leq \int_{Q} ∣ f ∣$ . If $a_{r} < c < b_{r}$ , cutting $Q$ at the coordinate hyperplane $x_{r} = c$ gives two nondegenerate subrectangles; integrability on $Q$ is equivalent to integrability on both restrictions, and their integral values add to the integral over $Q$ .

Proof

Given: The objects and hypotheses in the statement above.

1.1

In a signed chart, nonnegativity means $σ_{ϕ} f \geq 0$ . Multiplying by nonnegative partition weights and using Riemann monotonicity shows every chart contribution is nonnegative, so their finite sum is nonnegative.

F1F2

2.1

If $n \geq 1$ and $ω_{p} \neq 0$ , some partition weight is positive at $p$ . Its signed coefficient is continuous and positive there, hence at least $c > 0$ on a sufficiently small rectangle, or on a half-rectangle at a face. Inside this neighborhood choose a nondegenerate rectangle of positive volume; monotonicity and rectangle additivity bound that chart integral below by $c$ times its positive volume. The other terms are nonnegative.

F2step 1.1

3.1

For $n = 0$ every summand $ε (p) ω (p)$ is nonnegative and a nonzero form has a strictly positive summand. The zero form and the empty manifold give zero. These observations prove all assertions.

F1step 1.1step 2.1∎

Depends on

Used by

Nonzero total integral obstructs exactness on a closed manifold Corollary
False: summing unweighted atlas integrals is valid False statement

Dependency tree · two levels

13 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

Lee Proposition 16.6(c), pp.407–408 (nonnegative version by the same proof) (standard reference, not scraped)