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} [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, 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.

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

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

    Instances For
      Instances For
        @[simp]
        theorem Theorems100.«82».Cube.side_unitCube {n : } {j : Fin n} :
        Theorems100.«82».Cube.side Theorems100.«82».Cube.unitCube j = Set.Ico 0 1
        structure Theorems100.«82».Correct {n : } {ι : Type} (cs : ιTheorems100.«82».Cube n) :

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

        Instances For
          theorem Theorems100.«82».Correct.zero_le_of_mem_side {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : Theorems100.«82».Correct cs) {i : ι} {j : Fin (n + 1)} {x : } (hx : x Theorems100.«82».Cube.side (cs i) j) :
          0 x
          theorem Theorems100.«82».Correct.zero_le_of_mem {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : Theorems100.«82».Correct cs) {i : ι} {p : Fin (n + 1)} (hp : p Theorems100.«82».Cube.toSet (cs i)) (j : Fin (n + 1)) :
          0 p j
          theorem Theorems100.«82».Correct.zero_le_b {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : Theorems100.«82».Correct cs) {i : ι} {j : Fin (n + 1)} :
          theorem Theorems100.«82».Correct.b_add_w_le_one {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} (h : Theorems100.«82».Correct cs) {j : Fin (n + 1)} :
          Theorems100.«82».Cube.b (cs i) j + (cs i).w 1
          theorem Theorems100.«82».Correct.w_ne_one {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} (h : Theorems100.«82».Correct cs) [Nontrivial ι] (i : ι) :
          (cs i).w 1

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

          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.

          Instances For
            theorem Theorems100.«82».valley_unitCube {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} [Nontrivial ι] (h : Theorems100.«82».Correct cs) :
            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

            Instances For
              def Theorems100.«82».OnBoundary {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} {c : Theorems100.«82».Cube (n + 1)} :

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

              Instances For
                theorem Theorems100.«82».t_le_t {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} {c : Theorems100.«82».Cube (n + 1)} (hi : i Theorems100.«82».bcubes cs c) (j : Fin n) :
                theorem Theorems100.«82».w_lt_w {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} {c : Theorems100.«82».Cube (n + 1)} (h : Theorems100.«82».Correct cs) (v : Theorems100.«82».Valley cs c) (hi : i Theorems100.«82».bcubes cs c) :
                (cs i).w < c.w

                Every cube in the valley must be smaller than it

                There are at least two cubes in a valley

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

                There is a smallest cube in the valley

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

                Instances For
                  theorem Theorems100.«82».mi_minimal {n : } {ι : Type} {cs : ιTheorems100.«82».Cube (n + 1)} {i : ι} {c : Theorems100.«82».Cube (n + 1)} {h : Theorems100.«82».Correct cs} {v : Theorems100.«82».Valley cs c} [Finite ι] (hi : i Theorems100.«82».bcubes cs c) :
                  (cs (Theorems100.«82».mi h v)).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 : Theorems100.«82».Correct cs} {v : Theorems100.«82».Valley cs c} [Finite ι] (hii' : Theorems100.«82».mi h v i) (hi : i Theorems100.«82».bcubes cs c) :
                  (cs (Theorems100.«82».mi h v)).w < (cs i).w

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

                  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

                  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.

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

                  We get a sequence of cubes whose size is decreasing

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

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

                      theorem Theorems100.«82».cannot_cube_a_cube {n : } :
                      n 3∀ {s : Set (Theorems100.«82».Cube n)}, Set.Finite sSet.Nontrivial sSet.PairwiseDisjoint s Theorems100.«82».Cube.toSet⋃ (c : Theorems100.«82».Cube n) (_ : c s), Theorems100.«82».Cube.toSet c = Theorems100.«82».Cube.toSet Theorems100.«82».Cube.unitCubeSet.InjOn Theorems100.«82».Cube.w sFalse

                      Dissection of Cubes: A cube cannot be cubed.