CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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 Solovay model has no Banach–Tarski decomposition

Statement

In $M$ , there do not exist a closed ball $K \subseteq R^{3}$ , a finite partition $K = ⨆_{i < m} A_{i}$ , one rigid motion $g_{i}$ for each $i < m$ , and two disjoint congruent copies $K_{0}, K_{1}$ of $K$ such that

$K_{0} ⊔ K_{1} = ⨆_{i < m} g_{i} [A_{i}] .$

Thus every original piece is used exactly once in the alleged reassembly of the disjoint union; this is the usual equidecomposition formulation, not two separate reassemblies each reusing all the pieces.

Facts & Assumptions

Given: The finite partition, one-motion-per-piece reassembly, and two copies displayed in the statement.

[F1]

Universal real measurability transfers to finite-dimensional Euclidean spaces: every alleged piece is Lebesgue measurable.

[F2]

Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation and Lebesgue measure on $R^{n}$ is invariant under every orthogonal linear map: assuming Countable Choice, rigid motions preserve measure.

[F3]

A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included: assuming Countable Choice, positive-radius balls have positive finite measure by box containment.

[F4]

The Solovay inner model satisfies Dependent Choice and AC implies DC implies countable choice: $M$ satisfies Dependent Choice, hence Countable Choice.

Proof

1.1

By F4, Countable Choice holds in $M$ . If the radius is $r > 0$ , the ball contains a cube of side $2 r / \sqrt{3}$ and lies in a cube of side $2 r$ ; hence F3 gives $0 < V = λ_{3} (K) < \infty$ . Finite additivity gives $V = \sum_{i < m} λ (A_{i})$ , and F2 gives $\sum_{i < m} λ (g_{i} [A_{i}]) = V$ . But the displayed one-use reassembly and the disjoint congruent copies give $\sum_{i < m} λ (g_{i} [A_{i}]) = λ (K_{0} ⊔ K_{1}) = 2 V$ . Thus $V = 2 V$ , contradicting $0 < V < \infty$ .

F1F2F3F4Given

1.2

If $r = 0$ , $K$ is a singleton. Its finite partition has exactly one nonempty piece. Because the statement permits exactly one image of each original piece, the displayed union of the $g_{i} [A_{i}]$ has one point, whereas $K_{0} ⊔ K_{1}$ has two. Thus the zero-volume endpoint is excluded without the volume calculation.

Given

2.1

The positive- and zero-radius cases exhaust closed balls, proving the claim.

step 1.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

44 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

Solovay, A model of set-theory in which every set of reals is Lebesgue measurable (standard reference, not scraped)