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} [LinearOrder α] {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 ∈ 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 Theorems100.«82».Cube (n : ℕ) : Type

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.

• b : Fin n → ℝ
• w : ℝ
• hw : 0 < self.w

theorem Theorems100.«82».Cube.hw' {n : ℕ} (c : Cube n) : 0 ≤ c.w

def Theorems100.«82».Cube.side {n : ℕ} (c : Cube n) (j : Fin n) : Set ℝ

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

Equations

• c.side j = Set.Ico (c.b j) (c.b j + c.w)

@[simp]

theorem Theorems100.«82».Cube.b_mem_side {n : ℕ} (c : Cube n) (j : Fin n) : c.b j ∈ c.side j

def Theorems100.«82».Cube.toSet {n : ℕ} (c : Cube n) : Set (Fin n → ℝ)

Equations

• c.toSet = {x : Fin n → ℝ | ∀ (j : Fin n), x j ∈ c.side j}

theorem Theorems100.«82».Cube.side_nonempty {n : ℕ} (c : Cube n) (i : Fin n) : (c.side i).Nonempty

theorem Theorems100.«82».Cube.univ_pi_side {n : ℕ} (c : Cube n) : Set.univ.pi c.side = c.toSet

theorem Theorems100.«82».Cube.toSet_subset {n : ℕ} {c c' : Cube n} : c.toSet ⊆ c'.toSet ↔ ∀ (j : Fin n), c.side j ⊆ c'.side j

theorem Theorems100.«82».Cube.toSet_disjoint {n : ℕ} {c c' : Cube n} : Disjoint c.toSet c'.toSet ↔ ∃ (j : Fin n), Disjoint (c.side j) (c'.side j)

theorem Theorems100.«82».Cube.b_mem_toSet {n : ℕ} (c : Cube n) : c.b ∈ c.toSet

def Theorems100.«82».Cube.tail {n : ℕ} (c : Cube (n + 1)) : Cube n

Equations

• c.tail = { b := Fin.tail c.b, w := c.w, hw := ⋯ }

theorem Theorems100.«82».Cube.side_tail {n : ℕ} (c : Cube (n + 1)) (j : Fin n) : c.tail.side j = c.side j.succ

def Theorems100.«82».Cube.bottom {n : ℕ} (c : Cube (n + 1)) : Set (Fin (n + 1) → ℝ)

Equations

• c.bottom = {x : Fin (n + 1) → ℝ | x 0 = c.b 0 ∧ Fin.tail x ∈ c.tail.toSet}

theorem Theorems100.«82».Cube.b_mem_bottom {n : ℕ} (c : Cube (n + 1)) : c.b ∈ c.bottom

def Theorems100.«82».Cube.xm {n : ℕ} (c : Cube (n + 1)) : ℝ

Equations

• c.xm = c.b 0 + c.w

theorem Theorems100.«82».Cube.b_lt_xm {n : ℕ} (c : Cube (n + 1)) : c.b 0 < c.xm

theorem Theorems100.«82».Cube.b_ne_xm {n : ℕ} (c : Cube (n + 1)) : c.b 0 ≠ c.xm

def Theorems100.«82».Cube.shiftUp {n : ℕ} (c : Cube (n + 1)) : Cube (n + 1)

Equations

• c.shiftUp = { b := Fin.cons c.xm (Fin.tail c.b), w := c.w, hw := ⋯ }

@[simp]

theorem Theorems100.«82».Cube.tail_shiftUp {n : ℕ} (c : Cube (n + 1)) : c.shiftUp.tail = c.tail

@[simp]

theorem Theorems100.«82».Cube.head_shiftUp {n : ℕ} (c : Cube (n + 1)) : c.shiftUp.b 0 = c.xm

def Theorems100.«82».Cube.unitCube {n : ℕ} : Cube n

Equations

• Theorems100.«82».Cube.unitCube = { b := fun (x : Fin n) => 0, w := 1, hw := Theorems100.«82».Cube.unitCube._proof_4 }

@[simp]

theorem Theorems100.«82».Cube.side_unitCube {n : ℕ} {j : Fin n} : unitCube.side j = Set.Ico 0 1

structure Theorems100.«82».Correct {n : ℕ} {ι : Type} (cs : ι → Cube n) : Prop

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

• PairwiseDisjoint : Pairwise (Function.onFun Disjoint (Cube.toSet ∘ cs))
• iUnion_eq : ⋃ (i : ι), (cs i).toSet = Cube.unitCube.toSet
• Injective : Function.Injective (Cube.w ∘ cs)
• three_le : 3 ≤ n

theorem Theorems100.«82».Correct.toSet_subset_unitCube {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} (h : Correct cs) {i : ι} : (cs i).toSet ⊆ Cube.unitCube.toSet

theorem Theorems100.«82».Correct.side_subset {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} (h : Correct cs) {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 : ι → Cube (n + 1)} (h : Correct cs) {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 : ι → Cube (n + 1)} (h : Correct cs) {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 : ι → Cube (n + 1)} (h : Correct cs) {i : ι} {j : Fin (n + 1)} : 0 ≤ (cs i).b j

theorem Theorems100.«82».Correct.b_add_w_le_one {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {i : ι} (h : Correct cs) {j : Fin (n + 1)} : (cs i).b j + (cs i).w ≤ 1

theorem Theorems100.«82».Correct.nontrivial_fin {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} (h : Correct cs) : Nontrivial (Fin n)

theorem Theorems100.«82».Correct.w_ne_one {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} (h : Correct cs) [Nontrivial ι] (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 : ι → Cube (n + 1)} {i : ι} (h : Correct cs) (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 : ι → Cube (n + 1)) (c : 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

• One or more equations did not get rendered due to their size.

theorem Theorems100.«82».valley_unitCube {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} [Nontrivial ι] (h : Correct cs) : Valley cs Cube.unitCube

The bottom of the unit cube is a valley

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

the cubes which lie in the valley c

Equations

• Theorems100.«82».bcubes cs c = {i : ι | (cs i).b 0 = c.b 0 ∧ (cs i).tail.toSet ⊆ c.tail.toSet}

def Theorems100.«82».OnBoundary {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {i : ι} {c : Cube (n + 1)} : i ∈ bcubes cs c → (j : Fin n) → Prop

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

Equations

• Theorems100.«82».OnBoundary x✝ 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 Theorems100.«82».tail_sub {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {i : ι} {c : Cube (n + 1)} (hi : i ∈ bcubes cs c) (j : Fin n) : (cs i).tail.side j ⊆ c.tail.side j

theorem Theorems100.«82».bottom_mem_side {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {i : ι} {c : Cube (n + 1)} (hi : i ∈ bcubes cs c) : c.b 0 ∈ (cs i).side 0

theorem Theorems100.«82».b_le_b {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {i : ι} {c : Cube (n + 1)} (hi : i ∈ bcubes cs c) (j : Fin n) : c.b j.succ ≤ (cs i).b j.succ

theorem Theorems100.«82».t_le_t {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {i : ι} {c : Cube (n + 1)} (hi : i ∈ bcubes cs c) (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 : ι → Cube (n + 1)} {i : ι} {c : Cube (n + 1)} (h : Correct cs) (v : Valley cs c) (hi : i ∈ bcubes cs c) : (cs i).w < c.w

Every cube in the valley must be smaller than it

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

There are at least two cubes in a valley

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

There is a cube in the valley

theorem Theorems100.«82».exists_mi {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {c : Cube (n + 1)} (h : Correct cs) (v : Valley cs c) [Finite ι] : ∃ i ∈ bcubes cs c, ∀ i' ∈ bcubes cs c, (cs i).w ≤ (cs i').w

There is a smallest cube in the valley

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

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

Equations

• Theorems100.«82».mi h v = Classical.choose ⋯

theorem Theorems100.«82».mi_mem_bcubes {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {c : Cube (n + 1)} {h : Correct cs} {v : Valley cs c} [Finite ι] : mi h v ∈ bcubes cs c

theorem Theorems100.«82».mi_minimal {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {i : ι} {c : Cube (n + 1)} {h : Correct cs} {v : Valley cs c} [Finite ι] (hi : i ∈ bcubes cs c) : (cs (mi h v)).w ≤ (cs i).w

theorem Theorems100.«82».mi_strict_minimal {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {i : ι} {c : Cube (n + 1)} {h : Correct cs} {v : Valley cs c} [Finite ι] (hii' : mi h v ≠ i) (hi : i ∈ bcubes cs c) : (cs (mi h v)).w < (cs i).w

theorem Theorems100.«82».mi_xm_ne_one {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {c : Cube (n + 1)} {h : Correct cs} {v : Valley cs c} [Finite ι] : (cs (mi h v)).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 : ι → Cube (n + 1)} {c : Cube (n + 1)} {h : Correct cs} {v : Valley cs c} [Finite ι] {j : Fin n} (bi : OnBoundary ⋯ j) : ∃ x ∈ c.side j.succ \ (cs (mi h v)).side j.succ, ∀ ⦃i' : ι⦄, i' ∈ bcubes cs c → i' ≠ mi h v → (cs (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 Theorems100.«82».mi_not_onBoundary {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {c : Cube (n + 1)} (h : Correct cs) (v : Valley cs c) [Finite ι] (j : Fin n) : ¬OnBoundary ⋯ 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 Theorems100.«82».mi_not_onBoundary' {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {c : Cube (n + 1)} {h : Correct cs} {v : Valley cs c} [Finite ι] (j : Fin n) : c.tail.b j < (cs (mi h v)).tail.b j ∧ (cs (mi h v)).tail.b j + (cs (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 Theorems100.«82».valley_mi {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} {c : Cube (n + 1)} {h : Correct cs} {v : Valley cs c} [Finite ι] : Valley cs (cs (mi h v)).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 : ι → Cube (n + 1)} (h : Correct cs) [Finite ι] [Nontrivial ι] : ℕ → { i : ι // Valley cs (cs i).shiftUp }

We get a sequence of cubes whose size is decreasing

Equations

• Theorems100.«82».sequenceOfCubes h 0 = ⟨Theorems100.«82».mi h ⋯, ⋯⟩
• Theorems100.«82».sequenceOfCubes h k.succ = ⟨Theorems100.«82».mi h ⋯, ⋯⟩

def Theorems100.«82».decreasingSequence {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} (h : Correct cs) [Finite ι] [Nontrivial ι] (k : ℕ) : ℝ

Equations

• Theorems100.«82».decreasingSequence h k = (cs ↑(Theorems100.«82».sequenceOfCubes h k)).w

theorem Theorems100.«82».strictAnti_sequenceOfCubes {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} (h : Correct cs) [Finite ι] [Nontrivial ι] : StrictAnti (decreasingSequence h)

theorem Theorems100.«82».injective_sequenceOfCubes {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} (h : Correct cs) [Finite ι] [Nontrivial ι] : Function.Injective (sequenceOfCubes h)

theorem Theorems100.«82».not_correct {n : ℕ} {ι : Type} {cs : ι → Cube (n + 1)} [Finite ι] [Nontrivial ι] : ¬Correct cs

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

theorem Theorems100.«82».cannot_cube_a_cube {n : ℕ} : n ≥ 3 → ∀ {s : Set (Cube n)}, s.Finite → s.Nontrivial → s.PairwiseDisjoint Cube.toSet → ⋃ c ∈ s, c.toSet = Cube.unitCube.toSet → Set.InjOn Cube.w s → False

Dissection of Cubes: A cube cannot be cubed.