ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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 intervals removed from the Smith-Volterra-Cantor set have total length $1 / 2$ , so the set cannot be covered by intervals of total length less than $1 / 2$

Example

Let $S$ be the Smith-Volterra-Cantor set (The Smith-Volterra-Cantor set: the same construction removing, at stage $n \geq 1$ , an open middle interval of length $4^{- n}$ from each of the $2^{n - 1}$ remaining intervals). At stage $n$ exactly $2^{n}$ open intervals, each of length $4^{- n - 1}$ , are removed, so the lengths removed at that stage total $2^{n} \cdot 4^{- n - 1} = 4^{- 1} \cdot 2^{- n}$ and over all stages they total

$\sum_{n = 0}^{\infty} 4^{- 1} \cdot 2^{- n} = 4^{- 1} \cdot 2 = \frac{1}{2} .$

Correspondingly, no cover of $S$ by intervals has total length below $\frac{1}{2}$ : if $(a_{k})$ , $(b_{k})$ are sequences of reals with $a_{k} \leq b_{k}$ , $S \subseteq ⋃_{k} [a_{k}, b_{k}]$ and $\sum_{k < i} (b_{k} - a_{k}) \leq M$ for every $i$ , then $M \geq \frac{1}{2}$ (The Smith-Volterra-Cantor set is compact, perfect and nowhere dense, and does not have measure zero).

The two numbers are the two halves of the unit interval's length, and the second is what "the set has positive measure" means in the vocabulary available here: this library defines no outer measure, so the assertion is about covers and their total lengths, never about a number attached to $S$ itself.

Facts & Assumptions

Given: The Smith-Volterra-Cantor set $S$ , the lengths $(λ_{n})$ , the gaps $g_{n}$ , the lists $(N_{n}, ℓ^{(n)})$ and the removed intervals $M_{j}^{(n)} = (e_{j}^{(n)} + λ_{n + 1}, e_{j}^{(n)} + g_{n})$ of The Smith-Volterra-Cantor set: the same construction removing, at stage $n \geq 1$ , an open middle interval of length $4^{- n}$ from each of the $2^{n - 1}$ remaining intervals.

[L1]

Each $M_{j}^{(n)}$ has length $g_{n} - λ_{n + 1} = λ_{n} - 2 λ_{n + 1} = 4^{- n - 1}$ , and $\sum_{j < N_{n}} c = 2^{n} c$ for every real $c$ (The Smith-Volterra-Cantor set: the same construction removing, at stage $n \geq 1$ , an open middle interval of length $4^{- n}$ from each of the $2^{n - 1}$ remaining intervals, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Integer powers $a^{m}$ , Laws of integer exponents).

[L2]

$\sum_{n = 0}^{\infty} 2^{- n} = 2$ , convergent series scale termwise, and a series of nonnegative terms converges exactly when its partial sums are bounded, the sum being their supremum (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges, Series, partial sums, convergence and the sum, divergence, and the tail series, A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum, Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L3]

If sequences $(a_{k})$ , $(b_{k})$ with $a_{k} \leq b_{k}$ cover $S$ and all partial total lengths are at most $M$ , then $M \geq 2^{- 1}$ ; and $S$ is not null (The Smith-Volterra-Cantor set is compact, perfect and nowhere dense, and does not have measure zero, claim 4, Measure zero (a countable cover by intervals of total length below every $ε$ ) and content zero (a finite such cover)).

[L4]

A finite family of intervals covering $[a, b]$ has total length at least $b - a$ , and the same holds for a countable family (If finitely many intervals cover a closed bounded interval $[a, b]$ , the sum of their lengths is at least $b - a$ , A sequence of intervals covering $[a, b]$ has total length at least $b - a$ , so no interval of positive length has measure zero).

[L5]

Ordered-field arithmetic: $0 < 1$ , so $2 > 0$ and $4 > 0$ ; adding a constant and multiplying by a positive preserve an inequality (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property)). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.

Verification

technique · direct

1.1

Stage $n$ . By [L1] the intervals removed at stage $n$ are the $M_{j}^{(n)}$ for $j < N_{n}$ , each of length $4^{- n - 1}$ , so their lengths total $\sum_{j < N_{n}} 4^{- n - 1} = 2^{n} \cdot 4^{- n - 1}$ , which equals $4^{- 1} \cdot 2^{- n}$ because $4^{- n - 1} = 4^{- 1} \cdot 4^{- n} = 4^{- 1} \cdot 2^{- 2 n}$ and $2^{n} \cdot 2^{- 2 n} = 2^{- n}$ by [L1] and [L5].

givenL1L5

2.1

All stages together. The terms $4^{- 1} 2^{- n}$ are nonnegative, and by [L2] the series $\sum_{n} 4^{- 1} 2^{- n}$ converges with sum $4^{- 1} \cdot 2 = 2^{- 1}$ . So the total length of all the removed intervals is exactly $2^{- 1}$ .

step 1.1L2L5

3.1

The lower bound for covers. [L3] says precisely that a bound $M$ on all the partial total lengths of a cover of $S$ satisfies $M \geq 2^{- 1}$ ; so no cover of $S$ by intervals, countable or finite, has total length below $2^{- 1}$ , and in particular $S$ is not null. The two computations fit together: the removed intervals of total length $2^{- 1}$ and any cover of $S$ of total length $M$ together cover $[0, 1]$ , so $M + 2^{- 1} \geq 1$ by [L4], which is the same bound.

step 2.1L3L4∎

Remarks

What the numbers do and do not say. "Total length of the removed intervals" is a sum of lengths of an explicit family, and "no cover below $1 / 2$ " is a statement about all covers. Neither says that $S$ has measure $1 / 2$ : that would require an outer measure, which is not defined at this point in the reading order. The pair of statements is nevertheless the exact content of the classical assertion.
Why $4^{- n}$ and not $3^{- n}$ . For the middle-thirds construction the removed length at stage $n$ is $2^{n} 3^{- n - 1}$ , and $\sum_{n} 2^{n} 3^{- n - 1} = 3^{- 1} \cdot 3 = 1$ , so everything is removed in the sense of total length and the Cantor set is null (The Cantor set is compact, perfect, uncountable, nowhere dense and of measure zero, and it contains no interval of positive length, so its only nonempty connected subsets are single points). Here the removed pieces shrink faster than they multiply and only half the length goes.
The bound $1 / 2$ is sharp in one direction only. The removed intervals together with a cover of $S$ must reach total length $1$ , so a cover of $S$ cannot do better than $1 / 2$ ; whether total length exactly $1 / 2$ is approached by covers of $S$ is a question about outer measure and is not asked here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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

Smith-Volterra-Cantor set (Wikipedia) (standard reference, not scraped)
Null set (Wikipedia) (standard reference, not scraped)
A. Jin, Cantor sets in topology, analysis, and financial markets (standard reference, not scraped)

The intervals removed from the Smith-Volterra-Cantor set have total length 1/21/2, so the set cannot be covered by intervals of total length less than 1/21/2