LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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 boundary of a solid between continuous graphs over a compact Jordan base has content zero

Statement

Let $K$ be the solid of A solid between continuous graphs over a compact Jordan base. The boundary of $K$ has content zero.

Facts & Assumptions

Given: A compact Jordan set $D \subseteq R^{m}$ , continuous $α, β : D \to R$ with $α \leq β$ , and $K : = {(u, t) : u \in D, α (u) \leq t \leq β (u)}$ .

[F1]

If $A \subseteq R^{m}$ has content zero and $c \leq d$ , then $A \times [c, d]$ has content zero in $R^{m + 1}$ (The product of a content-zero set and a compact interval has content zero).

[F2]

The graph of every continuous $f : C \to R$ on a compact set $C \subseteq R^{m}$ has content zero in $R^{m + 1}$ (The graph of a continuous function on a compact Euclidean set has content zero).

[F3]

A metric-bounded set is Jordan measurable if and only if its boundary is null, equivalently has content zero (A bounded set in $R^{m}$ is Jordan measurable iff its boundary is null, equivalently of content zero).

Proof

technique · direct

1.1givenF3algebra

If $D = \emptyset$ , then $K$ and its boundary are empty. Otherwise the extreme-value theorem bounds both functions in one interval $[c, d]$ . Any point of $\partial K$ either projects to $\partial D$ , or projects to the interior of $D$ and lies on $t = α (u)$ or $t = β (u)$ ; hence $\partial K \subseteq graph (α) \cup graph (β) \cup (\partial D \times [c, d])$ . Since $D$ is Jordan measurable, [F3] makes $\partial D$ content zero.

2.1step 1.1F1F2

By [F2] the two graph pieces have content zero, and by [F1] the product $\partial D \times [c, d]$ has content zero.

3.1step 2.1constructalgebra∎

Given a positive tolerance, cover each of the three sets in step 2.1 with total cube volume below one third of it. Their union covers $\partial K$ , so the boundary has content zero.

Depends on

Dependency tree · 2 levels

Sources

Michael E. Taylor, Introduction to Analysis in Several Variables, Theorem 3.1.9