False statementConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

False: summing unweighted atlas integrals is valid

Statement

False assertion: for an arbitrary covering atlas one may integrate a compactly supported top form by summing unweighted chart integrals, without partition weights.

Facts & Assumptions

[F1]

Independence of atlas, partition and refinement: The compact-support integral on an oriented manifold is independent of the chart cover, coordinate maps, subordinate partition, and refinement. If $U \subset M$ is open and contains $supp ω$ , with its restricted orientation, then $\int_{U} ω ∣_{U} = \int_{M} ω$ .

[F2]

Positivity of the oriented integral: 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$ .

Refutation

Given: The proposed assertion; use the data constructed below.

1.1

On $R$ with increasing orientation choose the two distinct global charts $x$ and $y = 2 x$ . Let $f (x) = e^{- 1 / (1 - x^{2})}$ for $∣ x ∣ < 1$ and zero otherwise, and $ω = f (x) d x$ . This is a nonnegative smooth compactly supported nonzero form, so $I = \int ω > 0$ . Smoothness at the cut follows since every derivative is an exponential factor times a polynomial in reciprocal powers of $1 - x^{2}$ , tending to zero there.

F2algebra

2.1

Each of the two charts contains the support and computes $I$ by chart/partition independence. The proposed unweighted sum is $I + I = 2 I \neq I$ . The atlas genuinely has distinct coordinate maps; its overlap is counted twice.

F1step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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.5 proof pp.405–406 (necessity of partition weights) (standard reference, not scraped)