mathlib3 documentation

mathlib-archive / wiedijk_100_theorems.cubing_a_cube

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
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.

source
structure theorems_100.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.

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

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

Equations
source
@[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
source
def theorems_100.82.cube.to_set {n : ℕ} (c : theorems_100.«82».cube n) :
set (fin n → ℝ)
Equations
source
theorem theorems_100.82.cube.side_nonempty {n : ℕ} (c : theorems_100.«82».cube n) (i : fin n) :
(c.side i).nonempty
source
theorem theorems_100.82.cube.univ_pi_side {n : ℕ} (c : theorems_100.«82».cube n) :
set.univ.pi c.side = c.to_set
source
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
source
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)
source
theorem theorems_100.82.cube.b_mem_to_set {n : ℕ} (c : theorems_100.«82».cube n) :
c.b ∈ c.to_set
source
@[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 := _}
source
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
source
def theorems_100.82.cube.bottom {n : ℕ} (c : theorems_100.«82».cube (n + 1)) :
set (fin (n + 1) → ℝ)
Equations
source
theorem theorems_100.82.cube.b_mem_bottom {n : ℕ} (c : theorems_100.«82».cube (n + 1)) :
c.b ∈ c.bottom
source
def theorems_100.82.cube.xm {n : ℕ} (c : theorems_100.«82».cube (n + 1)) :
ℝ
Equations
  • c.xm = c.b 0 + c.w
source
theorem theorems_100.82.cube.b_lt_xm {n : ℕ} (c : theorems_100.«82».cube (n + 1)) :
c.b 0 < c.xm
source
theorem theorems_100.82.cube.b_ne_xm {n : ℕ} (c : theorems_100.«82».cube (n + 1)) :
c.b 0 ≠ c.xm
source
def theorems_100.82.cube.shift_up {n : ℕ} (c : theorems_100.«82».cube (n + 1)) :
theorems_100.«82».cube (n + 1)
Equations
source
@[simp]
theorem theorems_100.82.cube.tail_shift_up {n : ℕ} (c : theorems_100.«82».cube (n + 1)) :
c.shift_up.tail = c.tail
source
@[simp]
theorem theorems_100.82.cube.head_shift_up {n : ℕ} (c : theorems_100.«82».cube (n + 1)) :
c.shift_up.b 0 = c.xm
source
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}
source
@[simp]
theorem theorems_100.82.cube.side_unit_cube {n : ℕ} {j : fin n} :
theorems_100.«82».cube.unit_cube.side j = set.Ico 0 1
source
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

source
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
source
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 ⊆ set.Ico 0 1
source
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
source
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
source
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
source
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
source
theorem theorems_100.82.correct.nontrivial_fin {n : ℕ} {ι : Type} {cs : ι → theorems_100.«82».cube (n + 1)} (h : theorems_100.«82».correct cs) :
nontrivial (fin n)
source
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.

source
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.

source
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)
source
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

source
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}
source
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)
source
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
source
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
source
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
source
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
source
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

source
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

source
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

source
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

source
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
source
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
source
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
source
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
source
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

source
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

source
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.

source
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.

source
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.

source
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, _⟩
source
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
source
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)
source
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)
source
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.

source
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.