CounterexampleConstruction: 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.

The wrong boundary sign in the half-space computation

Statement refuted

False assertion: Stokes on the standard oriented half-line remains valid if its boundary point is assigned the positive sign instead of its induced negative sign.

Facts & Assumptions

[F1]

Compact-support Stokes on the upper half-space: Give $H^{n} = {x_{n} \geq 0}$ the standard orientation, $n \geq 1$ , and its face the outward-normal-first orientation. If $η \in Ω_{c}^{n - 1} (H^{n})$ and $j : \partial H^{n} ↪ H^{n}$ , then $\int_{H^{n}} d η = \int_{\partial H^{n}} j^{*} η .$ With $η = \sum_{i} a_{i} d x^{1} \land \dots \land \hat{d x^{i}} \land \dots \land d x^{n}$ , both sides are $(- 1)^{n} \int_{R^{n - 1}} a_{n} (x^{'}, 0) d x^{'}$ for $n > 1$ , and $- a_{1} (0)$ for $n = 1$ .

Counterexample

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

1.1

Choose a smooth compactly supported f on $[0, \infty)$ with f=1 near zero. Explicitly, put $b (u) = e^{- 1 / u}$ for $u > 0$ and zero otherwise, and $f (t) = b (2 - t) / (b (2 - t) + b (t - 1))$ . The denominator is positive for all t, and all derivatives of b vanish at zero, so f is smooth, equals one for t at most one, and zero for t at least two.

construct

2.1

The half-space Stokes formula in dimension one gives $\int_{0}^{\infty} f^{'} (t) d t = - f (0) = - 1$ , equivalently the FTC difference $f (2) - f (0)$ . Giving the endpoint positive sign instead yields $+ f (0) = 1$ , so the proposed convention breaks the identity.

F1step 1.1∎

Depends on

Compact-support Stokes on the upper half-space

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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 Theorem 16.11 proof pp.412–413 (standard reference, not scraped)