# mathlibdocumentation

mathlib-archive / 100-theorems-list.82_cubing_a_cube

Proof that a cube (in dimension n ≥ 3) cannot be cubed: There does not exist a partition of a cube into finitely many smaller cubes (at least two) of different sizes.

We follow the proof described here: http://www.alaricstephen.com/main-featured/2017/9/28/cubing-a-cube-proof

theorem theorems_100.82.Ico_lemma {α : Type u_1} [linear_order α] {x₁ x₂ y₁ y₂ z₁ z₂ w : α} (h₁ : x₁ < y₁) (hy : y₁ < y₂) (h₂ : y₂ < x₂) (hz₁ : z₁ y₂) (hz₂ : y₁ z₂) (hw : w set.Ico y₁ y₂ w set.Ico z₁ z₂) :
(w : α), w set.Ico x₁ x₂ w set.Ico y₁ y₂ w set.Ico z₁ z₂

Given three intervals I, J, K such that J ⊂ I, neither endpoint of J coincides with an endpoint of I, ¬ (K ⊆ J) and K does not lie completely to the left nor completely to the right of J. Then I ∩ K \ J is nonempty.

structure theorems_100.82.cube (n : ) :

A (hyper)-cube (in standard orientation) is a vector b consisting of the bottom-left point of the cube, a width w and a proof that w > 0. We use functions from fin n to denote vectors.

Instances for theorems_100.82.cube
• theorems_100.82.cube.has_sizeof_inst
theorem theorems_100.82.cube.hw' {n : } (c : theorems_100.«82».cube n) :
0 c.w
def theorems_100.82.cube.side {n : } (c : theorems_100.«82».cube n) (j : fin n) :

The j-th side of a cube is the half-open interval [b j, b j + w)

Equations
@[simp]
theorem theorems_100.82.cube.b_mem_side {n : } (c : theorems_100.«82».cube n) (j : fin n) :
c.b j c.side j
def theorems_100.82.cube.to_set {n : } (c : theorems_100.«82».cube n) :
Equations
theorem theorems_100.82.cube.side_nonempty {n : } (c : theorems_100.«82».cube n) (i : fin n) :
(c.side i).nonempty
theorem theorems_100.82.cube.univ_pi_side {n : } (c : theorems_100.«82».cube n) :
set.univ.pi c.side = c.to_set
theorem theorems_100.82.cube.to_set_subset {n : } {c c' : theorems_100.«82».cube n} :
c.to_set c'.to_set (j : fin n), c.side j c'.side j
theorem theorems_100.82.cube.to_set_disjoint {n : } {c c' : theorems_100.«82».cube n} :
disjoint c.to_set c'.to_set (j : fin n), disjoint (c.side j) (c'.side j)
theorem theorems_100.82.cube.b_mem_to_set {n : } (c : theorems_100.«82».cube n) :
c.b c.to_set
@[protected]
def theorems_100.82.cube.tail {n : } (c : theorems_100.«82».cube (n + 1)) :
theorems_100.«82».cube n
Equations
• c.tail = {b := fin.tail c.b, w := c.w, hw := _}
theorem theorems_100.82.cube.side_tail {n : } (c : theorems_100.«82».cube (n + 1)) (j : fin n) :
c.tail.side j = c.side j.succ
def theorems_100.82.cube.bottom {n : } (c : theorems_100.«82».cube (n + 1)) :
set (fin (n + 1) )
Equations
theorem theorems_100.82.cube.b_mem_bottom {n : } (c : theorems_100.«82».cube (n + 1)) :
c.b c.bottom
def theorems_100.82.cube.xm {n : } (c : theorems_100.«82».cube (n + 1)) :
Equations
• c.xm = c.b 0 + c.w
theorem theorems_100.82.cube.b_lt_xm {n : } (c : theorems_100.«82».cube (n + 1)) :
c.b 0 < c.xm
theorem theorems_100.82.cube.b_ne_xm {n : } (c : theorems_100.«82».cube (n + 1)) :
c.b 0 c.xm
def theorems_100.82.cube.shift_up {n : } (c : theorems_100.«82».cube (n + 1)) :
theorems_100.«82».cube (n + 1)
Equations
@[simp]
theorem theorems_100.82.cube.tail_shift_up {n : } (c : theorems_100.«82».cube (n + 1)) :
c.shift_up.tail = c.tail
@[simp]
theorem theorems_100.82.cube.head_shift_up {n : } (c : theorems_100.«82».cube (n + 1)) :
c.shift_up.b 0 = c.xm
def theorems_100.82.cube.unit_cube {n : } :
theorems_100.«82».cube n
Equations
• theorems_100.«82».cube.unit_cube = {b := λ (_x : fin n), 0, w := 1, hw := theorems_100.«82».cube.unit_cube._proof_1}
@[simp]
theorem theorems_100.82.cube.side_unit_cube {n : } {j : fin n} :
theorems_100.«82».cube.unit_cube.side j = 1
structure theorems_100.82.correct {n : } {ι : Type} (cs : ι theorems_100.«82».cube n) :
Prop
• pairwise_disjoint : pairwise (disjoint on theorems_100.«82».cube.to_set cs)
• Union_eq : ( (i : ι), (cs i).to_set) = theorems_100.«82».cube.unit_cube.to_set
• injective : function.injective (theorems_100.«82».cube.w cs)
• three_le : 3 n

A finite family of (at least 2) cubes partitioning the unit cube with different sizes

theorem theorems_100.82.correct.to_set_subset_unit_cube {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) {i : ι} :
(cs i).to_set theorems_100.«82».cube.unit_cube.to_set
theorem theorems_100.82.correct.side_subset {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) {i : ι} {j : fin (n + 1)} :
(cs i).side j 1
theorem theorems_100.82.correct.zero_le_of_mem_side {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) {i : ι} {j : fin (n + 1)} {x : } (hx : x (cs i).side j) :
0 x
theorem theorems_100.82.correct.zero_le_of_mem {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) {i : ι} {p : fin (n + 1) } (hp : p (cs i).to_set) (j : fin (n + 1)) :
0 p j
theorem theorems_100.82.correct.zero_le_b {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) {i : ι} {j : fin (n + 1)} :
0 (cs i).b j
theorem theorems_100.82.correct.b_add_w_le_one {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {i : ι} (h : theorems_100.«82».correct cs) {j : fin (n + 1)} :
(cs i).b j + (cs i).w 1
theorem theorems_100.82.correct.nontrivial_fin {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) :
theorem theorems_100.82.correct.w_ne_one {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) [nontrivial ι] (i : ι) :
(cs i).w 1

The width of any cube in the partition cannot be 1.

theorem theorems_100.82.correct.shift_up_bottom_subset_bottoms {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {i : ι} (h : theorems_100.«82».correct cs) (hc : (cs i).xm 1) :
(cs i).shift_up.bottom (i : ι), (cs i).bottom

The top of a cube (which is the bottom of the cube shifted up by its width) must be covered by bottoms of (other) cubes in the family.

def theorems_100.82.valley {n : } {ι : Type} (cs : ι theorems_100.«82».cube (n + 1)) (c : theorems_100.«82».cube (n + 1)) :
Prop

A valley is a square on which cubes in the family of cubes are placed, so that the cubes completely cover the valley and none of those cubes is partially outside the square. We also require that no cube on it has the same size as the valley (so that there are at least two cubes on the valley). This is the main concept in the formalization. We prove that the smallest cube on a valley has another valley on the top of it, which gives an infinite sequence of cubes in the partition, which contradicts the finiteness. A valley is characterized by a cube c (which is not a cube in the family cs) by considering the bottom face of c.

Equations
• theorems_100.«82».valley cs c = ((c.bottom (i : ι), (cs i).bottom) ( (i : ι), (cs i).b 0 = c.b 0 ( (x : fin n ), x (cs i).tail.to_set c.tail.to_set) (cs i).tail.to_set c.tail.to_set) (i : ι), (cs i).b 0 = c.b 0 (cs i).w c.w)
theorem theorems_100.82.valley_unit_cube {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} [nontrivial ι] (h : theorems_100.«82».correct cs) :
theorems_100.«82».valley cs theorems_100.«82».cube.unit_cube

The bottom of the unit cube is a valley

def theorems_100.82.bcubes {n : } {ι : Type} (cs : ι theorems_100.«82».cube (n + 1)) (c : theorems_100.«82».cube (n + 1)) :
set ι

the cubes which lie in the valley c

Equations
• theorems_100.«82».bcubes cs c = {i : ι | (cs i).b 0 = c.b 0 (cs i).tail.to_set c.tail.to_set}
def theorems_100.82.on_boundary {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {i : ι} {c : theorems_100.«82».cube (n + 1)} (hi : i theorems_100.«82».bcubes cs c) (j : fin n) :
Prop

A cube which lies on the boundary of a valley in dimension j

Equations
• theorems_100.«82».on_boundary hi j = (c.b j.succ = (cs i).b j.succ (cs i).b j.succ + (cs i).w = c.b j.succ + c.w)
theorem theorems_100.82.tail_sub {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {i : ι} {c : theorems_100.«82».cube (n + 1)} (hi : i theorems_100.«82».bcubes cs c) (j : fin n) :
(cs i).tail.side j c.tail.side j
theorem theorems_100.82.bottom_mem_side {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {i : ι} {c : theorems_100.«82».cube (n + 1)} (hi : i theorems_100.«82».bcubes cs c) :
c.b 0 (cs i).side 0
theorem theorems_100.82.b_le_b {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {i : ι} {c : theorems_100.«82».cube (n + 1)} (hi : i theorems_100.«82».bcubes cs c) (j : fin n) :
c.b j.succ (cs i).b j.succ
theorem theorems_100.82.t_le_t {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {i : ι} {c : theorems_100.«82».cube (n + 1)} (hi : i theorems_100.«82».bcubes cs c) (j : fin n) :
(cs i).b j.succ + (cs i).w c.b j.succ + c.w
theorem theorems_100.82.w_lt_w {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {i : ι} {c : theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) (v : theorems_100.«82».valley cs c) (hi : i theorems_100.«82».bcubes cs c) :
(cs i).w < c.w

Every cube in the valley must be smaller than it

theorem theorems_100.82.nontrivial_bcubes {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {c : theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) (v : theorems_100.«82».valley cs c) :
(theorems_100.«82».bcubes cs c).nontrivial

There are at least two cubes in a valley

theorem theorems_100.82.nonempty_bcubes {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {c : theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) (v : theorems_100.«82».valley cs c) :
(theorems_100.«82».bcubes cs c).nonempty

There is a cube in the valley

theorem theorems_100.82.exists_mi {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {c : theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) (v : theorems_100.«82».valley cs c) [finite ι] :
(i : ι) (H : i theorems_100.«82».bcubes cs c), (i' : ι), i' theorems_100.«82».bcubes cs c (cs i).w (cs i').w

There is a smallest cube in the valley

noncomputable def theorems_100.82.mi {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {c : theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) (v : theorems_100.«82».valley cs c) [finite ι] :
ι

We let mi be the (index for the) smallest cube in the valley c

Equations
• theorems_100.«82».mi h v =
theorem theorems_100.82.mi_mem_bcubes {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {c : theorems_100.«82».cube (n + 1)} {h : theorems_100.«82».correct cs} {v : theorems_100.«82».valley cs c} [finite ι] :
theorems_100.«82».mi h v theorems_100.«82».bcubes cs c
theorem theorems_100.82.mi_minimal {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {i : ι} {c : theorems_100.«82».cube (n + 1)} {h : theorems_100.«82».correct cs} {v : theorems_100.«82».valley cs c} [finite ι] (hi : i theorems_100.«82».bcubes cs c) :
(cs (theorems_100.«82».mi h v)).w (cs i).w
theorem theorems_100.82.mi_strict_minimal {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {i : ι} {c : theorems_100.«82».cube (n + 1)} {h : theorems_100.«82».correct cs} {v : theorems_100.«82».valley cs c} [finite ι] (hii' : theorems_100.«82».mi h v i) (hi : i theorems_100.«82».bcubes cs c) :
(cs (theorems_100.«82».mi h v)).w < (cs i).w
theorem theorems_100.82.mi_xm_ne_one {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {c : theorems_100.«82».cube (n + 1)} {h : theorems_100.«82».correct cs} {v : theorems_100.«82».valley cs c} [finite ι] :
(cs (theorems_100.«82».mi h v)).xm 1

The top of mi cannot be 1, since there is a larger cube in the valley

theorem theorems_100.82.smallest_on_boundary {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {c : theorems_100.«82».cube (n + 1)} {h : theorems_100.«82».correct cs} {v : theorems_100.«82».valley cs c} [finite ι] {j : fin n} (bi : theorems_100.«82».on_boundary theorems_100.«82».mi_mem_bcubes j) :
(x : ), x c.side j.succ \ (cs (theorems_100.«82».mi h v)).side j.succ ⦃i' : ι⦄, i' theorems_100.«82».bcubes cs c i' theorems_100.«82».mi h v (cs (theorems_100.«82».mi h v)).b j.succ (cs i').side j.succ x (cs i').side j.succ

If mi lies on the boundary of the valley in dimension j, then this lemma expresses that all other cubes on the same boundary extend further from the boundary. More precisely, there is a j-th coordinate x : ℝ in the valley, but not in mi, such that every cube that shares a (particular) j-th coordinate with mi also contains j-th coordinate x

theorem theorems_100.82.mi_not_on_boundary {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {c : theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) (v : theorems_100.«82».valley cs c) [finite ι] (j : fin n) :
¬theorems_100.«82».on_boundary theorems_100.«82».mi_mem_bcubes j

mi cannot lie on the boundary of the valley. Otherwise, the cube adjacent to it in the j-th direction will intersect one of the neighbouring cubes on the same boundary as mi.

theorem theorems_100.82.mi_not_on_boundary' {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {c : theorems_100.«82».cube (n + 1)} {h : theorems_100.«82».correct cs} {v : theorems_100.«82».valley cs c} [finite ι] (j : fin n) :
c.tail.b j < (cs (theorems_100.«82».mi h v)).tail.b j (cs (theorems_100.«82».mi h v)).tail.b j + (cs (theorems_100.«82».mi h v)).w < c.tail.b j + c.w

The same result that mi cannot lie on the boundary of the valley written as inequalities.

theorem theorems_100.82.valley_mi {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} {c : theorems_100.«82».cube (n + 1)} {h : theorems_100.«82».correct cs} {v : theorems_100.«82».valley cs c} [finite ι] :
theorems_100.«82».valley cs (cs (theorems_100.«82».mi h v)).shift_up

The top of mi gives rise to a new valley, since the neighbouring cubes extend further upward than mi.

noncomputable def theorems_100.82.sequence_of_cubes {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) [finite ι] [nontrivial ι] :
{i // theorems_100.«82».valley cs (cs i).shift_up}

We get a sequence of cubes whose size is decreasing

Equations
• theorems_100.«82».sequence_of_cubes h (k + 1) = let v : theorems_100.«82».valley cs (cs (theorems_100.«82».sequence_of_cubes h k).val).shift_up := _ in theorems_100.«82».mi h v _inst_1, _⟩
• theorems_100.«82».sequence_of_cubes h 0 = let v : theorems_100.«82».valley cs theorems_100.«82».cube.unit_cube := _ in theorems_100.«82».mi h v _inst_1, _⟩
noncomputable def theorems_100.82.decreasing_sequence {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) [finite ι] [nontrivial ι] (k : ) :
Equations
• theorems_100.«82».decreasing_sequence h k = (cs (theorems_100.«82».sequence_of_cubes h k).val).w
theorem theorems_100.82.strict_anti_sequence_of_cubes {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) [finite ι] [nontrivial ι] :
strict_anti (theorems_100.«82».decreasing_sequence h)
theorem theorems_100.82.injective_sequence_of_cubes {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) [finite ι] [nontrivial ι] :
function.injective (theorems_100.«82».sequence_of_cubes h)
theorem theorems_100.82.not_correct {n : } {ι : Type} {cs : ι theorems_100.«82».cube (n + 1)} [finite ι] [nontrivial ι] :
¬theorems_100.«82».correct cs

The infinite sequence of cubes contradicts the finiteness of the family.

theorem theorems_100.82.cannot_cube_a_cube {n : } :
n 3 {s : set (theorems_100.«82».cube n)}, s.finite s.nontrivial s.pairwise_disjoint theorems_100.«82».cube.to_set ( (c : theorems_100.«82».cube n) (H : c s), c.to_set) = theorems_100.«82».cube.unit_cube.to_set set.inj_on theorems_100.«82».cube.w s false

Dissection of Cubes: A cube cannot be cubed.