Soundness of the kernel tree walk

kCheck hok b t = true, together with coverage of the holes of t, covers the box b: no point of b is a reduced Rupert pose.

structure Cayley.Pack.Inv (b : K.KBox) : Prop

The invariants of the boxes produced by the walk.

• chart : b.chart < 5
• face : b.face < 6
• lenc : b.c.length = 5
• lenh : b.h.length = 5
• hpos (i : Fin 5) : 0 ≤ b.h.getD (↑i) 0
• mag (i : Fin 5) : |b.c.getD (↑i) 0| + |b.h.getD (↑i) 0| ≤ 2 * 2 ^ b.K

def Cayley.Pack.Covered (b : K.KBox) : Prop

No point of the box is a reduced Rupert pose.

Equations

• Cayley.Pack.Covered b = ∀ (t : Fin 5 → ℝ), (∀ (i : Fin 5), |t i| ≤ 1) → Cayley.PtOK b.chart b.face (Cayley.kpt b t) → ¬Cayley.Bad b.chart b.face (Cayley.kpt b t)

Splitting

theorem Cayley.Pack.getD_set_eq (l : List ℤ) (d : ℕ) (x : ℤ) (hd : d < l.length) : (l.set d x).getD d 0 = x

theorem Cayley.Pack.getD_set_ne (l : List ℤ) (d i : ℕ) (x : ℤ) (h : i ≠ d) : (l.set d x).getD i 0 = l.getD i 0

theorem Cayley.Pack.getD_map2 (l : List ℤ) (i : ℕ) : (List.map (fun (x : ℤ) => 2 * x) l).getD i 0 = 2 * l.getD i 0

theorem Cayley.Pack.split_fst (b : K.KBox) (d : ℕ) : (b.split d).1.chart = b.chart ∧ (b.split d).1.face = b.face

theorem Cayley.Pack.split_snd (b : K.KBox) (d : ℕ) : (b.split d).2.chart = b.chart ∧ (b.split d).2.face = b.face

theorem Cayley.Pack.split_inv (b : K.KBox) (hb : Inv b) (d : ℕ) (hd : d < 5) : Inv (b.split d).1 ∧ Inv (b.split d).2

theorem Cayley.Pack.split_cover (b : K.KBox) (hb : Inv b) (d : ℕ) (hd : d < 5) (t : Fin 5 → ℝ) (ht : ∀ (i : Fin 5), |t i| ≤ 1) : (∃ (t' : Fin 5 → ℝ), (∀ (i : Fin 5), |t' i| ≤ 1) ∧ kpt (b.split d).1 t' = kpt b t) ∨ ∃ (t' : Fin 5 → ℝ), (∀ (i : Fin 5), |t' i| ≤ 1) ∧ kpt (b.split d).2 t' = kpt b t

Every point of a box is a point of one of its two halves.

theorem Cayley.Pack.split_big (b : K.KBox) (hb : Inv b) (d : ℕ) (hd : 5 ≤ d) : (b.split d).1 = b ∧ (b.split d).2 = b

theorem Cayley.Pack.holes_nil (b : K.KBox) (tr : K.KTree) (h : K.kCheck false b tr = true) : K.holes b tr = []

A hole-free check has no holes.

theorem Cayley.Pack.walk (hok : Bool) (tr : K.KTree) (b : K.KBox) : Inv b → K.kCheck hok b tr = true → ∀ (t : Fin 5 → ℝ), (∀ (i : Fin 5), |t i| ≤ 1) → PtOK b.chart b.face (kpt b t) → Bad b.chart b.face (kpt b t) → ∃ hb ∈ K.holes b tr, Inv hb ∧ hb.chart = b.chart ∧ hb.face = b.face ∧ ∃ (t' : Fin 5 → ℝ), (∀ (i : Fin 5), |t' i| ≤ 1) ∧ kpt hb t' = kpt b t

The tree walk. A bad point of a checked box lies in one of its holes.

theorem Cayley.Pack.covered_of_check (b : K.KBox) (hb : Inv b) (tr : K.KTree) (h : K.kCheck false b tr = true) : Covered b

A hole-free checked box is covered.