# Documentation

## Archive.Wiedijk100Theorems.CubingACube

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 Theorems100.«82».Ico_lemma {α : Type u_1} [] {x₁ : α} {x₂ : α} {y₁ : α} {y₂ : α} {z₁ : α} {z₂ : α} {w : α} (h₁ : x₁ < y₁) (hy : y₁ < y₂) (h₂ : y₂ < x₂) (hz₁ : z₁ y₂) (hz₂ : y₁ z₂) (hw : wSet.Ico y₁ y₂ w Set.Ico z₁ z₂) :
wSet.Ico x₁ x₂, wSet.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.

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
theorem Theorems100.«82».Cube.hw {n : } (self : ) :
0 < self.w
theorem Theorems100.«82».Cube.hw' {n : } (c : ) :
0 c.w
def Theorems100.«82».Cube.side {n : } (c : ) (j : Fin n) :

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

Equations
Instances For
@[simp]
theorem Theorems100.«82».Cube.b_mem_side {n : } (c : ) (j : Fin n) :
c.b j c.side j
def Theorems100.«82».Cube.toSet {n : } (c : ) :
Set (Fin n)
Equations
• c.toSet = {x : Fin n | ∀ (j : Fin n), x j c.side j}
Instances For
theorem Theorems100.«82».Cube.side_nonempty {n : } (c : ) (i : Fin n) :
(c.side i).Nonempty
theorem Theorems100.«82».Cube.univ_pi_side {n : } (c : ) :
Set.univ.pi c.side = c.toSet
theorem Theorems100.«82».Cube.toSet_subset {n : } {c : } {c' : } :
c.toSet c'.toSet ∀ (j : Fin n), c.side j c'.side j
theorem Theorems100.«82».Cube.toSet_disjoint {n : } {c : } {c' : } :
Disjoint c.toSet c'.toSet ∃ (j : Fin n), Disjoint (c.side j) (c'.side j)
theorem Theorems100.«82».Cube.b_mem_toSet {n : } (c : ) :
c.b c.toSet
Equations
• c.tail = { b := Fin.tail c.b, w := c.w, hw := }
Instances For
theorem Theorems100.«82».Cube.side_tail {n : } (c : Theorems100.«82».Cube (n + 1)) (j : Fin n) :
c.tail.side j = c.side j.succ
Equations
Instances For
Equations
• c.xm = c.b 0 + c.w
Instances For
Equations
Instances For
@[simp]
theorem Theorems100.«82».Cube.tail_shiftUp {n : } (c : Theorems100.«82».Cube (n + 1)) :
c.shiftUp.tail = c.tail
@[simp]
theorem Theorems100.«82».Cube.head_shiftUp {n : } (c : Theorems100.«82».Cube (n + 1)) :
c.shiftUp.b 0 = c.xm
Equations
Instances For
@[simp]
theorem Theorems100.«82».Cube.side_unitCube {n : } {j : Fin n} :
Theorems100.«82».Cube.unitCube.side j = Set.Ico 0 1
structure Theorems100.«82».Correct {n : } {ι : Type} (cs : ) :

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

• PairwiseDisjoint : Pairwise (Disjoint on Theorems100.«82».Cube.toSet cs)
• iUnion_eq : ⋃ (i : ι), (cs i).toSet = Theorems100.«82».Cube.unitCube.toSet
• Injective : Function.Injective (Theorems100.«82».Cube.w cs)
• three_le : 3 n
Instances For
theorem Theorems100.«82».Correct.PairwiseDisjoint {n : } {ι : Type} {cs : } (self : ) :
Pairwise (Disjoint on Theorems100.«82».Cube.toSet cs)
theorem Theorems100.«82».Correct.iUnion_eq {n : } {ι : Type} {cs : } (self : ) :
⋃ (i : ι), (cs i).toSet = Theorems100.«82».Cube.unitCube.toSet
theorem Theorems100.«82».Correct.Injective {n : } {ι : Type} {cs : } (self : ) :
Function.Injective (Theorems100.«82».Cube.w cs)
theorem Theorems100.«82».Correct.three_le {n : } {ι : Type} {cs : } (self : ) :
3 n
theorem Theorems100.«82».Correct.toSet_subset_unitCube {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : ) {i : ι} :
(cs i).toSet Theorems100.«82».Cube.unitCube.toSet
theorem Theorems100.«82».Correct.side_subset {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : ) {i : ι} {j : Fin (n + 1)} :
(cs i).side j Set.Ico 0 1
theorem Theorems100.«82».Correct.zero_le_of_mem_side {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : ) {i : ι} {j : Fin (n + 1)} {x : } (hx : x (cs i).side j) :
0 x
theorem Theorems100.«82».Correct.zero_le_of_mem {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : ) {i : ι} {p : Fin (n + 1)} (hp : p (cs i).toSet) (j : Fin (n + 1)) :
0 p j
theorem Theorems100.«82».Correct.zero_le_b {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : ) {i : ι} {j : Fin (n + 1)} :
0 (cs i).b j
theorem Theorems100.«82».Correct.b_add_w_le_one {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} (h : ) {j : Fin (n + 1)} :
(cs i).b j + (cs i).w 1
theorem Theorems100.«82».Correct.w_ne_one {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : ) [] (i : ι) :
(cs i).w 1

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

theorem Theorems100.«82».Correct.shiftUp_bottom_subset_bottoms {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} (h : ) (hc : (cs i).xm 1) :
(cs i).shiftUp.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 Theorems100.«82».Valley {n : } {ι : Type} (cs : ιTheorems100.«82».Cube (n + 1)) (c : Theorems100.«82».Cube (n + 1)) :

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
• One or more equations did not get rendered due to their size.
Instances For
theorem Theorems100.«82».valley_unitCube {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} [] (h : ) :
Theorems100.«82».Valley cs Theorems100.«82».Cube.unitCube

The bottom of the unit cube is a valley

def Theorems100.«82».bcubes {n : } {ι : Type} (cs : ιTheorems100.«82».Cube (n + 1)) (c : Theorems100.«82».Cube (n + 1)) :
Set ι

the cubes which lie in the valley c

Equations
• = {i : ι | (cs i).b 0 = c.b 0 (cs i).tail.toSet c.tail.toSet}
Instances For
def Theorems100.«82».OnBoundary {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} {c : Theorems100.«82».Cube (n + 1)} :
i Fin nProp

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

Equations
• = (c.b j.succ = (cs i).b j.succ (cs i).b j.succ + (cs i).w = c.b j.succ + c.w)
Instances For
theorem Theorems100.«82».tail_sub {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} {c : Theorems100.«82».Cube (n + 1)} (hi : i ) (j : Fin n) :
(cs i).tail.side j c.tail.side j
theorem Theorems100.«82».bottom_mem_side {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} {c : Theorems100.«82».Cube (n + 1)} (hi : i ) :
c.b 0 (cs i).side 0
theorem Theorems100.«82».b_le_b {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} {c : Theorems100.«82».Cube (n + 1)} (hi : i ) (j : Fin n) :
c.b j.succ (cs i).b j.succ
theorem Theorems100.«82».t_le_t {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} {c : Theorems100.«82».Cube (n + 1)} (hi : i ) (j : Fin n) :
(cs i).b j.succ + (cs i).w c.b j.succ + c.w
theorem Theorems100.«82».w_lt_w {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} {c : Theorems100.«82».Cube (n + 1)} (h : ) (v : ) (hi : i ) :
(cs i).w < c.w

Every cube in the valley must be smaller than it

theorem Theorems100.«82».nontrivial_bcubes {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {c : Theorems100.«82».Cube (n + 1)} (h : ) (v : ) :
().Nontrivial

There are at least two cubes in a valley

theorem Theorems100.«82».nonempty_bcubes {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {c : Theorems100.«82».Cube (n + 1)} (h : ) (v : ) :
().Nonempty

There is a cube in the valley

theorem Theorems100.«82».exists_mi {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {c : Theorems100.«82».Cube (n + 1)} (h : ) (v : ) [] :
i, i', (cs i).w (cs i').w

There is a smallest cube in the valley

def Theorems100.«82».mi {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {c : Theorems100.«82».Cube (n + 1)} (h : ) (v : ) [] :
ι

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

Equations
Instances For
theorem Theorems100.«82».mi_mem_bcubes {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {c : Theorems100.«82».Cube (n + 1)} {h : } {v : } [] :
theorem Theorems100.«82».mi_minimal {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} {c : Theorems100.«82».Cube (n + 1)} {h : } {v : } [] (hi : i ) :
(cs ()).w (cs i).w
theorem Theorems100.«82».mi_strict_minimal {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} {c : Theorems100.«82».Cube (n + 1)} {h : } {v : } [] (hii' : i) (hi : i ) :
(cs ()).w < (cs i).w
theorem Theorems100.«82».mi_xm_ne_one {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {c : Theorems100.«82».Cube (n + 1)} {h : } {v : } [] :
(cs ()).xm 1

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

theorem Theorems100.«82».smallest_onBoundary {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {c : Theorems100.«82».Cube (n + 1)} {h : } {v : } [] {j : Fin n} (bi : ) :
xc.side j.succ \ (cs ()).side j.succ, ∀ ⦃i' : ι⦄, i' i' (cs ()).b j.succ (cs i').side j.succx (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 Theorems100.«82».mi_not_onBoundary {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {c : Theorems100.«82».Cube (n + 1)} (h : ) (v : ) [] (j : Fin n) :

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 Theorems100.«82».mi_not_onBoundary' {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {c : Theorems100.«82».Cube (n + 1)} {h : } {v : } [] (j : Fin n) :
c.tail.b j < (cs ()).tail.b j (cs ()).tail.b j + (cs ()).w < c.tail.b j + c.w

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

theorem Theorems100.«82».valley_mi {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {c : Theorems100.«82».Cube (n + 1)} {h : } {v : } [] :
Theorems100.«82».Valley cs (cs ()).shiftUp

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

noncomputable def Theorems100.«82».sequenceOfCubes {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : ) [] [] :
{ i : ι // Theorems100.«82».Valley cs (cs i).shiftUp }

We get a sequence of cubes whose size is decreasing

Equations
• = let v := ; ⟨,
• = let v := ; ⟨,
Instances For
def Theorems100.«82».decreasingSequence {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : ) [] [] (k : ) :
Equations
• = (cs ).w
Instances For
theorem Theorems100.«82».strictAnti_sequenceOfCubes {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : ) [] [] :
theorem Theorems100.«82».injective_sequenceOfCubes {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : ) [] [] :
theorem Theorems100.«82».not_correct {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} [] [] :

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

theorem Theorems100.«82».cannot_cube_a_cube {n : } :
n 3∀ {s : }, s.Finites.Nontrivials.PairwiseDisjoint Theorems100.«82».Cube.toSetcs, c.toSet = Theorems100.«82».Cube.unitCube.toSetSet.InjOn Theorems100.«82».Cube.w sFalse

Dissection of Cubes: A cube cannot be cubed.