The main soundness theorem of the kernel checker

If each of the 15 root boxes carries a checked skeleton whose holes are checked hole-free subtrees, then the Noperthedron is not Rupert.

theorem Cayley.Pack.face_ax0 (r : Fin 3 → ℝ) (R : ℝ) (hR : ∀ (i : Fin 3), |r i| ≤ R) (hmax : ∀ (i : Fin 3), |r i| ≤ |r 0|) (hpos : 0 < |r 0|) : ∃ face < 6, ∃ (ρ : ℝ) (s0 : ℝ) (s1 : ℝ), 0 ≤ ρ ∧ ρ ≤ R ∧ |s0| ≤ 1 ∧ |s1| ≤ 1 ∧ ρ • faceR face s0 s1 = r

theorem Cayley.Pack.face_ax1 (r : Fin 3 → ℝ) (R : ℝ) (hR : ∀ (i : Fin 3), |r i| ≤ R) (hmax : ∀ (i : Fin 3), |r i| ≤ |r 1|) (hpos : 0 < |r 1|) : ∃ face < 6, ∃ (ρ : ℝ) (s0 : ℝ) (s1 : ℝ), 0 ≤ ρ ∧ ρ ≤ R ∧ |s0| ≤ 1 ∧ |s1| ≤ 1 ∧ ρ • faceR face s0 s1 = r

theorem Cayley.Pack.face_ax2 (r : Fin 3 → ℝ) (R : ℝ) (hR : ∀ (i : Fin 3), |r i| ≤ R) (hmax : ∀ (i : Fin 3), |r i| ≤ |r 2|) (hpos : 0 < |r 2|) : ∃ face < 6, ∃ (ρ : ℝ) (s0 : ℝ) (s1 : ℝ), 0 ≤ ρ ∧ ρ ≤ R ∧ |s0| ≤ 1 ∧ |s1| ≤ 1 ∧ ρ • faceR face s0 s1 = r

theorem Cayley.Pack.exists_face (r : Fin 3 → ℝ) (R : ℝ) (hR : ∀ (i : Fin 3), |r i| ≤ R) : ∃ face < 6, ∃ (ρ : ℝ) (s0 : ℝ) (s1 : ℝ), 0 ≤ ρ ∧ ρ ≤ R ∧ |s0| ≤ 1 ∧ |s1| ≤ 1 ∧ ρ • faceR face s0 s1 = r

Every vector with |rᵢ| ≤ R is ρ c for c on a face of the unit cube.

The root boxes

theorem Cayley.Pack.rootK_plain (i : ℕ) (hi : i < 3) : (K.rootK i).chart = i + 1 ∧ ∀ (t : Fin 5 → ℝ), kpt (K.rootK i) t = ![1 / 2 + 1 / 2 * t 0, 1 / 4 + 1 / 4 * t 1, t 2, t 3, t 4]

theorem Cayley.Pack.rootK_blow0 (f : ℕ) (hf : f < 6) : (K.rootK (3 + f)).chart = 0 ∧ (K.rootK (3 + f)).face = f ∧ ∀ (t : Fin 5 → ℝ), kpt (K.rootK (3 + f)) t = ![1 / 2 + 1 / 2 * t 0, 1 / 4 + 1 / 4 * t 1, t 2, t 3, 1 / 2 + 1 / 2 * t 4]

theorem Cayley.Pack.rootK_blow4 (f : ℕ) (hf : f < 6) : (K.rootK (9 + f)).chart = 4 ∧ (K.rootK (9 + f)).face = f ∧ ∀ (t : Fin 5 → ℝ), kpt (K.rootK (9 + f)) t = ![1 / 2 + 1 / 2 * t 0, 1 / 4 + 1 / 4 * t 1, t 2, t 3, 1 + t 4]

theorem Cayley.Pack.rootK_inv (i : ℕ) (hi : i < 15) : Inv (K.rootK i)

Coverage

theorem Cayley.Pack.cover {u v : ℝ} {j : ℕ} {r : Fin 3 → ℝ} (hred : Reduced u v j r) : ∃ i < 15, ∃ (t : Fin 5 → ℝ), (∀ (k : Fin 5), |t k| ≤ 1) ∧ (K.rootK i).chart = j ∧ kpt (K.rootK i) t 0 = u ∧ kpt (K.rootK i) t 1 = v ∧ rOf (kblow j) (K.rootK i).face (kpt (K.rootK i) t) = r ∧ PtOK (K.rootK i).chart (K.rootK i).face (kpt (K.rootK i) t)

Assembly

theorem Cayley.Pack.AllOK_mem {P : List (K.KBox × K.KTree)} (h : K.AllOK P) (p : K.KBox × K.KTree) : p ∈ P → K.kCheck false p.1 p.2 = true

theorem Cayley.Pack.root_covered (b : K.KBox) (hb : Inv b) (S : K.KTree) (P : List (K.KBox × K.KTree)) (hs : K.kCheck true b S = true) (hh : K.holes b S = List.map Prod.fst P) (ha : K.AllOK P) : Covered b

A root skeleton whose holes are checked hole-free subtrees covers its box.

def Cayley.Pack.RootOK (i : ℕ) : Prop

The certificate facts for one root box.

Equations

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

theorem Cayley.Pack.kernel_sound (h : ∀ i < 15, RootOK i) : ¬IsRupert Noperthedron.exactVerts

Main soundness theorem. Certificates for the 15 root boxes refute Rupertness.