Soundness of the kernel gap leaf

pGapOK b s w₀ w₁ = true implies, at every point of the box, the hypotheses of gap_core.

The vertex table

theorem Cayley.Pack.vt_scaled' (t : ℕ) : t < 90 → (vertexOf (t / 6) (t % 6 / 3) (t % 3)).x.e ≤ 160 ∧ (vertexOf (t / 6) (t % 6 / 3) (t % 3)).y.e ≤ 160 ∧ (vertexOf (t / 6) (t % 6 / 3) (t % 3)).z.e ≤ 160 ∧ (vertexOf (t / 6) (t % 6 / 3) (t % 3)).x.m * 2 ^ (160 - (vertexOf (t / 6) (t % 6 / 3) (t % 3)).x.e) = (vt t).1 ∧ (vertexOf (t / 6) (t % 6 / 3) (t % 3)).y.m * 2 ^ (160 - (vertexOf (t / 6) (t % 6 / 3) (t % 3)).y.e) = (vt t).2.1 ∧ (vertexOf (t / 6) (t % 6 / 3) (t % 3)).z.m * 2 ^ (160 - (vertexOf (t / 6) (t % 6 / 3) (t % 3)).z.e) = (vt t).2.2

The kernel vertex table is the checker's vertexTab, scaled by 2^160.

theorem Cayley.Pack.vertexTab_eq (t : ℕ) (ht : t < 90) : vertexTab[t]! = vertexOf (t / 6) (t % 6 / 3) (t % 3)

theorem Cayley.Pack.vt_scaled (t : ℕ) (ht : t < 90) : vertexTab[t]!.x.e ≤ 160 ∧ vertexTab[t]!.y.e ≤ 160 ∧ vertexTab[t]!.z.e ≤ 160 ∧ vertexTab[t]!.x.m * 2 ^ (160 - vertexTab[t]!.x.e) = (vt t).1 ∧ vertexTab[t]!.y.m * 2 ^ (160 - vertexTab[t]!.y.e) = (vt t).2.1 ∧ vertexTab[t]!.z.m * 2 ^ (160 - vertexTab[t]!.z.e) = (vt t).2.2

theorem Cayley.Pack.D_scaled {q : QI} {m : ℤ} (he : q.e ≤ 160) (hm : q.m * 2 ^ (160 - q.e) = m) : D q = ↑m / 2 ^ 160

noncomputable def Cayley.Pack.vR (t : ℕ) : Fin 3 → ℝ

The tabulated vertex as a real vector.

Equations

• Cayley.Pack.vR t i = Cayley.Pack.svec (Cayley.Pack.vt t) i / 2 ^ 160

theorem Cayley.Pack.vR_err {t : ℕ} (ht : t < 90) (i : Fin 3) : |(vtx t - vR t) i| ≤ 1 / 2 ^ 60

The decoded polynomials

def Cayley.Pack.gp (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) : K.GData PE

The gap-leaf expressions for inner vertex s.

Equations

• Cayley.Pack.gp b s w0 w1 = Cayley.Pack.gapPE b (Cayley.Pack.vt s) w0 w1

def Cayley.Pack.Ap (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) : PE

A = Σ αₖ βₖ.

Equations

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

def Cayley.Pack.Ep0 (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) : PE

Eₖ = αₖ κD.

Equations

• Cayley.Pack.Ep0 b s w0 w1 = (Cayley.Pack.gp b s w0 w1).a0.mul (Cayley.Pack.gp b s w0 w1).kd

def Cayley.Pack.Ep1 (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) : PE

Equations

• Cayley.Pack.Ep1 b s w0 w1 = (Cayley.Pack.gp b s w0 w1).a1.mul (Cayley.Pack.gp b s w0 w1).kd

def Cayley.Pack.Ep2 (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) : PE

Equations

• Cayley.Pack.Ep2 b s w0 w1 = (Cayley.Pack.gp b s w0 w1).a2.mul (Cayley.Pack.gp b s w0 w1).kd

def Cayley.Pack.xp (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (T : ℤ × ℤ × ℤ) : PE

Σ Tₖ αₖ.

Equations

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

def Cayley.Pack.Fp (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (T : ℤ × ℤ × ℤ) : PE

F_T = A − (Σ Tₖ αₖ) κD.

Equations

• Cayley.Pack.Fp b s w0 w1 T = (Cayley.Pack.Ap b s w0 w1).sub ((Cayley.Pack.xp b s w0 w1 T).mul (Cayley.Pack.gp b s w0 w1).kd)

def Cayley.Pack.Lp (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) : PE

L = Σ αₖ Lₖ.

Equations

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

theorem Cayley.Pack.gp_int (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (k : Fin 10) : PE.ev (fun (i : Fin 5) => K.pX ↑i) ((gp b s w0 w1).get k) = (K.pGapData b (vt s) w0 w1).get k

Field values of gp.

theorem Cayley.Pack.gp_real (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (t : Fin 5 → ℝ) (k : Fin 10) : PE.ev t ((gp b s w0 w1).get k) = (gapR b (vt s) w0 w1 t).get k

theorem Cayley.Pack.gp_fields_real (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (t : Fin 5 → ℝ) : have g := gapR b (vt s) w0 w1 t; PE.ev t (gp b s w0 w1).a0 = g.a0 ∧ PE.ev t (gp b s w0 w1).a1 = g.a1 ∧ PE.ev t (gp b s w0 w1).a2 = g.a2 ∧ PE.ev t (gp b s w0 w1).b0 = g.b0 ∧ PE.ev t (gp b s w0 w1).b1 = g.b1 ∧ PE.ev t (gp b s w0 w1).b2 = g.b2 ∧ PE.ev t (gp b s w0 w1).kd = g.kd ∧ PE.ev t (gp b s w0 w1).l0 = g.l0 ∧ PE.ev t (gp b s w0 w1).l1 = g.l1 ∧ PE.ev t (gp b s w0 w1).l2 = g.l2

theorem Cayley.Pack.gapSc_eq (b : K.KBox) : 2 ^ K.gapSc b = (2 ^ b.K) ^ 2 * betaSc b

theorem Cayley.Pack.Fp_real (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (hj : b.chart < 5) (t : Fin 5 → ℝ) (T : ℤ × ℤ × ℤ) : PE.ev t (Fp b s w0 w1 T) = 2 ^ K.gapSc b * 2 ^ 160 * (cayleyDenom (kpt b t 1) (-kpt b t 0) 0 * kapJ b.chart * cayleyDenom (rOf (kblow b.chart) b.face (kpt b t) 0) (rOf (kblow b.chart) b.face (kpt b t) 1) (rOf (kblow b.chart) b.face (kpt b t) 2) * (lin (↑w0) (↑w1) ((outerRot (kpt b t 0) (kpt b t 1) * Qm b.chart (rOf (kblow b.chart) b.face (kpt b t))).mulVec (vR s)) - lin (↑w0) (↑w1) ((outerRot (kpt b t 0) (kpt b t 1)).mulVec fun (i : Fin 3) => svec T i / 2 ^ 160)))

The real value of F_T: the scaled gap of the tabulated vertices.

theorem Cayley.Pack.Lp_real (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (hj : b.chart < 5) (hbl : b.chart = 0 ∨ b.chart = 4) (t : Fin 5 → ℝ) : 2 * PE.ev t (Lp b s w0 w1) = 2 ^ K.gapScL b * 2 ^ 160 * (2 * lin (↑w0) (↑w1) ((NoR (kpt b t)).mulVec ((chartMR b.chart).mulVec (crossR (faceR b.face (kpt b t 2) (kpt b t 3)) (vR s) + kpt b t 4 • crossR (faceR b.face (kpt b t 2) (kpt b t 3)) (crossR (faceR b.face (kpt b t 2) (kpt b t 3)) (vR s))))))

The real value of L (blown-up charts): the scaled paired-vertex bracket.

Degrees and norms

theorem Cayley.Pack.gp_deg (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (hj : b.chart < 5) (hf : b.face < 6) (k : Fin 10) (i : Fin 5) : PE.deg i ((gp b s w0 w1).get k) ≤ degB k i

theorem Cayley.Pack.fits_all (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (hj : b.chart < 5) (hf : b.face < 6) (T : ℤ × ℤ × ℤ) : L3.Fits (Ap b s w0 w1) ∧ L3.Fits (Ep0 b s w0 w1) ∧ L3.Fits (Ep1 b s w0 w1) ∧ L3.Fits (Ep2 b s w0 w1) ∧ L3.Fits (Fp b s w0 w1 T) ∧ L3.Fits (Lp b s w0 w1)

theorem Cayley.Pack.O_eq : O = 2 ^ 399

theorem Cayley.Pack.nrm_add' (a c : PE) : (a.add c).nrm = a.nrm + c.nrm

theorem Cayley.Pack.nrm_sub' (a c : PE) : (a.sub c).nrm = a.nrm + c.nrm

theorem Cayley.Pack.nrm_mul' (a c : PE) : (a.mul c).nrm = a.nrm * c.nrm

theorem Cayley.Pack.nrm_c' (z : ℤ) : (PE.c z).nrm = z.natAbs

theorem Cayley.Pack.gapNrmOK_spec {b : K.KBox} {S : ℤ × ℤ × ℤ} {w0 w1 : ℤ} (h : K.gapNrmOK b S w0 w1 = true) : (K.gapNrm b S w0 w1).a0 * (K.gapNrm b S w0 w1).b0 + (K.gapNrm b S w0 w1).a1 * (K.gapNrm b S w0 w1).b1 + (K.gapNrm b S w0 w1).a2 * (K.gapNrm b S w0 w1).b2 + 2 ^ 161 * ((K.gapNrm b S w0 w1).a0 + (K.gapNrm b S w0 w1).a1 + (K.gapNrm b S w0 w1).a2) * (K.gapNrm b S w0 w1).kd < 2 ^ 390 ∧ (K.gapNrm b S w0 w1).a0 * (K.gapNrm b S w0 w1).l0 + (K.gapNrm b S w0 w1).a1 * (K.gapNrm b S w0 w1).l1 + (K.gapNrm b S w0 w1).a2 * (K.gapNrm b S w0 w1).l2 < 2 ^ 390

The norm guard from the cheap check nrmOK

theorem Cayley.Pack.gapNrmOK_of_le {b b' : K.KBox} {S S' : ℤ × ℤ × ℤ} {w0 w1 w0' w1' : ℤ} (h : ∀ (k : Fin 10), (K.gapNrm b S w0 w1).get k ≤ (K.gapNrm b' S' w0' w1').get k) (h' : K.gapNrmOK b' S' w0' w1' = true) : K.gapNrmOK b S w0 w1 = true

def Cayley.Pack.worstBox (chart face : ℕ) : K.KBox

The worst box of a chart and face: scale 2^16, every centre and radius 2^17.

Equations

• Cayley.Pack.worstBox chart face = { chart := chart, face := face, K := 16, c := List.replicate 5 ↑(2 ^ 17), h := List.replicate 5 ↑(2 ^ 17) }

def Cayley.Pack.S161 : ℤ × ℤ × ℤ

Every coordinate at the vertex bound.

Equations

• Cayley.Pack.S161 = (↑(2 ^ 161), ↑(2 ^ 161), ↑(2 ^ 161))

theorem Cayley.Pack.gapNrmOK_worst (chart : ℕ) : chart < 5 → ∀ face < 6, K.gapNrmOK (worstBox chart face) S161 1024 1024 = true

theorem Cayley.Pack.worstBox_getD (chart face i : ℕ) (hi : i < 5) : (worstBox chart face).c.getD i 0 = ↑(2 ^ 17) ∧ (worstBox chart face).h.getD i 0 = ↑(2 ^ 17)

theorem Cayley.Pack.gapNrmOK_box (b : K.KBox) (hj : b.chart < 5) (hf : b.face < 6) (hlc : b.c.length = 5) (hlh : b.h.length = 5) (hmag : ∀ (i : Fin 5), |b.c.getD (↑i) 0| + |b.h.getD (↑i) 0| ≤ 2 * 2 ^ b.K) {s : ℕ} (hs : s < 90) {w0 w1 : ℤ} (hn : K.nrmOK b w0 w1 = true) : K.gapNrmOK b (vt s) w0 w1 = true

A box with the walk's magnitude bound that passes nrmOK passes the norm guard.

theorem Cayley.Pack.nrm_all390 (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (h : K.gapNrmOK b (vt s) w0 w1 = true) (T : ℤ × ℤ × ℤ) (hT : T.1.natAbs < 2 ^ 161 ∧ T.2.1.natAbs < 2 ^ 161 ∧ T.2.2.natAbs < 2 ^ 161) : (Ap b s w0 w1).nrm < 2 ^ 390 ∧ (Ep0 b s w0 w1).nrm < 2 ^ 390 ∧ (Ep1 b s w0 w1).nrm < 2 ^ 390 ∧ (Ep2 b s w0 w1).nrm < 2 ^ 390 ∧ (Fp b s w0 w1 T).nrm < 2 ^ 390 ∧ (Lp b s w0 w1).nrm < 2 ^ 390

theorem Cayley.Pack.two390_lt_O : 2 ^ 390 < O

theorem Cayley.Pack.nrm_all (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (h : K.gapNrmOK b (vt s) w0 w1 = true) (T : ℤ × ℤ × ℤ) (hT : T.1.natAbs < 2 ^ 161 ∧ T.2.1.natAbs < 2 ^ 161 ∧ T.2.2.natAbs < 2 ^ 161) : (Ap b s w0 w1).nrm < O ∧ (Ep0 b s w0 w1).nrm < O ∧ (Ep1 b s w0 w1).nrm < O ∧ (Ep2 b s w0 w1).nrm < O ∧ (Fp b s w0 w1 T).nrm < O ∧ (Lp b s w0 w1).nrm < O

theorem Cayley.Pack.bern_room {n : ℕ} (h : n < 2 ^ 390) : 243 * ↑n + 2 ^ 390 ≤ ↑O ∧ 243 * ↑(2 * n) + 2 ^ 390 ≤ ↑O

Room for the Bernstein transform: 243 n + 2^390 ≤ O when n < 2^390, and for 2n.

The vertex-packed quick test

theorem Cayley.Pack.testBit_top {x n : ℕ} (hx : x < 2 ^ (n + 1)) : x.testBit n = decide (2 ^ n ≤ x)

theorem Cayley.Pack.tab_eq (e : ℤ) (tn tp : ℕ) (dn dp : ℕ → ℕ) (hn : tn = packN 640 dn 90) (hp : tp = packN 640 dp 90) : (if 0 ≤ e then tn else tp) * e.natAbs = packN 640 (fun (t : ℕ) => e.natAbs * if 0 ≤ e then dn t else dp t) 90

One table term of the packed sum.

def Cayley.Pack.quickDig (C e00 e01 e02 : ℤ) (n0 n1 n2 t : ℕ) : ℕ

Its slot t.

Equations

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

theorem Cayley.Pack.quickV_eq (C e00 e01 e02 : ℤ) (n0 n1 n2 : ℕ) : K.quickV C e00 e01 e02 n0 n1 n2 = packN 640 (quickDig C e00 e01 e02 n0 n1 n2) 90

theorem Cayley.Pack.quickDig_int (C e00 e01 e02 : ℤ) (n0 n1 n2 : ℕ) (hC : 0 ≤ C) {t : ℕ} (ht : t < 90) : ↑(quickDig C e00 e01 e02 n0 n1 n2 t) = C + ↑BT * (↑(e00.natAbs + e01.natAbs + e02.natAbs) + ↑(n0 + n1 + n2)) - ((vt t).1 * e00 + (vt t).2.1 * e01 + (vt t).2.2 * e02) - ↑((vt t).1.natAbs * n0 + (vt t).2.1.natAbs * n1 + (vt t).2.2.natAbs * n2)

The slot as an integer.

theorem Cayley.Pack.quick_bit (q e00 e01 e02 : ℤ) (n0 n1 n2 : ℕ) (hC : 0 ≤ K.p2 639 + q - K.p2 170 * (↑e00.natAbs + ↑e01.natAbs + ↑e02.natAbs + (↑n0 + ↑n1 + ↑n2))) (hC2 : K.p2 639 + q - K.p2 170 * (↑e00.natAbs + ↑e01.natAbs + ↑e02.natAbs + (↑n0 + ↑n1 + ↑n2)) + 2 * K.p2 170 * (↑e00.natAbs + ↑e01.natAbs + ↑e02.natAbs + (↑n0 + ↑n1 + ↑n2)) < K.p2 640) {t : ℕ} (ht : t < 90) (hb : (K.quickV (K.p2 639 + q - K.p2 170 * (↑e00.natAbs + ↑e01.natAbs + ↑e02.natAbs + (↑n0 + ↑n1 + ↑n2))) e00 e01 e02 n0 n1 n2).testBit (640 * t + 639) = true) : 0 ≤ q - ((vt t).1 * e00 + (vt t).2.1 * e01 + (vt t).2.2 * e02) - ↑((vt t).1.natAbs * n0 + (vt t).2.1.natAbs * n1 + (vt t).2.2.natAbs * n2)

Per-vertex bounds

theorem Cayley.Pack.quick_real {A E0 E1 E2 c0 sl e0 e1 e2 a0 a1 a2 T0 T1 T2 err : ℝ} (hA : c0 - sl ≤ A) (h0 : |E0 - e0| ≤ a0) (h1 : |E1 - e1| ≤ a1) (h2 : |E2 - e2| ≤ a2) (hq : 0 ≤ c0 - sl - err - (T0 * e0 + T1 * e1 + T2 * e2) - (|T0| * a0 + |T1| * a1 + |T2| * a2)) : err ≤ A - (T0 * E0 + T1 * E1 + T2 * E2)

@[reducible, inline]

abbrev Cayley.Pack.pXv : Fin 5 → ℤ

The Kronecker point as a function.

Equations

• Cayley.Pack.pXv i = Cayley.K.pX ↑i

theorem Cayley.Pack.gp_fields_int (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) : have g := K.pGapData b (vt s) w0 w1; PE.ev pXv (gp b s w0 w1).a0 = g.a0 ∧ PE.ev pXv (gp b s w0 w1).a1 = g.a1 ∧ PE.ev pXv (gp b s w0 w1).a2 = g.a2 ∧ PE.ev pXv (gp b s w0 w1).b0 = g.b0 ∧ PE.ev pXv (gp b s w0 w1).b1 = g.b1 ∧ PE.ev pXv (gp b s w0 w1).b2 = g.b2 ∧ PE.ev pXv (gp b s w0 w1).kd = g.kd ∧ PE.ev pXv (gp b s w0 w1).l0 = g.l0 ∧ PE.ev pXv (gp b s w0 w1).l1 = g.l1 ∧ PE.ev pXv (gp b s w0 w1).l2 = g.l2

theorem Cayley.Pack.ints (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) : have g := K.pGapData b (vt s) w0 w1; K.gA g = PE.ev pXv (Ap b s w0 w1) ∧ K.gL g = PE.ev pXv (Lp b s w0 w1) ∧ g.a0.mul g.kd = PE.ev pXv (Ep0 b s w0 w1) ∧ g.a1.mul g.kd = PE.ev pXv (Ep1 b s w0 w1) ∧ g.a2.mul g.kd = PE.ev pXv (Ep2 b s w0 w1) ∧ ∀ (T : ℤ × ℤ × ℤ), K.gF g T.1 T.2.1 T.2.2 = PE.ev pXv (Fp b s w0 w1 T)

theorem Cayley.Pack.err_scale (w0 w1 : ℤ) {sc : ℕ} {Y : ℝ} (j : ℕ) (h : ↑(128 * K.chartKI j * (↑w0.natAbs + ↑w1.natAbs) * K.p2 (sc + 100)) ≤ 2 ^ sc * 2 ^ 160 * Y) : 128 * kapJ j * (1 / 2 ^ 60) * (|↑w0| + |↑w1|) ≤ Y

The error scale: err ≤ F_T at a point gives the per-vertex hypothesis of gap_core.

def Cayley.Pack.G1 (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (t : Fin 5 → ℝ) (tt : ℕ) : Prop

The per-vertex hypothesis of gap_core at box point t.

Equations

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

def Cayley.Pack.G2 (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (t : Fin 5 → ℝ) : Prop

The paired hypothesis of gap_core.

Equations

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

theorem Cayley.Pack.G1_of (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (hj : b.chart < 5) (t : Fin 5 → ℝ) (tt : ℕ) (h : ↑(K.gErr b w0 w1) ≤ PE.ev t (Fp b s w0 w1 (vt tt))) : G1 b s w0 w1 t tt

theorem Cayley.Pack.full_G1 (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (hj : b.chart < 5) (hf : b.face < 6) (hn : K.gapNrmOK b (vt s) w0 w1 = true) {tt : ℕ} (htt : tt < 90) (hfull : K.fullOK b (vt s) w0 w1 (vt tt).1 (vt tt).2.1 (vt tt).2.2 = true) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) : G1 b s w0 w1 t tt

theorem Cayley.Pack.pair_G2 (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (hj : b.chart < 5) (hf : b.face < 6) (hbl : b.chart = 0 ∨ b.chart = 4) (hn : K.gapNrmOK b (vt s) w0 w1 = true) (hp : K.pairOK b (vt s) w0 w1 = true) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) : G2 b s w0 w1 t

theorem Cayley.Pack.Fp_split (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (T : ℤ × ℤ × ℤ) (t : Fin 5 → ℝ) : PE.ev t (Fp b s w0 w1 T) = PE.ev t (Ap b s w0 w1) - (↑T.1 * PE.ev t (Ep0 b s w0 w1) + ↑T.2.1 * PE.ev t (Ep1 b s w0 w1) + ↑T.2.2 * PE.ev t (Ep2 b s w0 w1))

theorem Cayley.Pack.quick_G1 (b : K.KBox) (s : ℕ) (w0 w1 : ℤ) (hj : b.chart < 5) (hf : b.face < 6) (hn : K.gapNrmOK b (vt s) w0 w1 = true) {tt : ℕ} (htt : tt < 90) (hC : 0 ≤ K.p2 639 + K.quickQ b (vt s) w0 w1 - K.p2 170 * (↑(K.quickE b (vt s) w0 w1).1.c0.natAbs + ↑(K.quickE b (vt s) w0 w1).2.1.c0.natAbs + ↑(K.quickE b (vt s) w0 w1).2.2.c0.natAbs + (↑(K.quickE b (vt s) w0 w1).1.abs + ↑(K.quickE b (vt s) w0 w1).2.1.abs + ↑(K.quickE b (vt s) w0 w1).2.2.abs))) (hC2 : K.p2 639 + K.quickQ b (vt s) w0 w1 - K.p2 170 * (↑(K.quickE b (vt s) w0 w1).1.c0.natAbs + ↑(K.quickE b (vt s) w0 w1).2.1.c0.natAbs + ↑(K.quickE b (vt s) w0 w1).2.2.c0.natAbs + (↑(K.quickE b (vt s) w0 w1).1.abs + ↑(K.quickE b (vt s) w0 w1).2.1.abs + ↑(K.quickE b (vt s) w0 w1).2.2.abs)) + 2 * K.p2 170 * (↑(K.quickE b (vt s) w0 w1).1.c0.natAbs + ↑(K.quickE b (vt s) w0 w1).2.1.c0.natAbs + ↑(K.quickE b (vt s) w0 w1).2.2.c0.natAbs + (↑(K.quickE b (vt s) w0 w1).1.abs + ↑(K.quickE b (vt s) w0 w1).2.1.abs + ↑(K.quickE b (vt s) w0 w1).2.2.abs)) < K.p2 640) (hb : (K.quickV (K.p2 639 + K.quickQ b (vt s) w0 w1 - K.p2 170 * (↑(K.quickE b (vt s) w0 w1).1.c0.natAbs + ↑(K.quickE b (vt s) w0 w1).2.1.c0.natAbs + ↑(K.quickE b (vt s) w0 w1).2.2.c0.natAbs + (↑(K.quickE b (vt s) w0 w1).1.abs + ↑(K.quickE b (vt s) w0 w1).2.1.abs + ↑(K.quickE b (vt s) w0 w1).2.2.abs))) (K.quickE b (vt s) w0 w1).1.c0 (K.quickE b (vt s) w0 w1).2.1.c0 (K.quickE b (vt s) w0 w1).2.2.c0 (K.quickE b (vt s) w0 w1).1.abs (K.quickE b (vt s) w0 w1).2.1.abs (K.quickE b (vt s) w0 w1).2.2.abs).testBit (640 * tt + 639) = true) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) : G1 b s w0 w1 t tt

Unfolding the checker

theorem Cayley.Pack.vtestG_sound (b : K.KBox) (hj : b.chart < 5) (hf : b.face < 6) (s : ℕ) (w0 w1 : ℤ) (hn : K.gapNrmOK b (vt s) w0 w1 = true) {tt : ℕ} (htt : tt < 90) (h : K.vtestG b s (vt s) w0 w1 tt (vt tt).1 (vt tt).2.1 (vt tt).2.2 = true) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) : G1 b s w0 w1 t tt ∨ K.gPair b s = some tt ∧ K.pairOK b (vt s) w0 w1 = true

theorem Cayley.Pack.vt_lt_BT {t : ℕ} (ht : t < 90) : |(vt t).1| < ↑BT ∧ |(vt t).2.1| < ↑BT ∧ |(vt t).2.2| < ↑BT

theorem Cayley.Pack.slot_vals {t : ℕ} (ht : t < 90) : K.slot K.tpx t - ↑(2 ^ 170) = (vt t).1 ∧ K.slot K.tpy t - ↑(2 ^ 170) = (vt t).2.1 ∧ K.slot K.tpz t - ↑(2 ^ 170) = (vt t).2.2

theorem Cayley.Pack.vS_eq {s : ℕ} (hs : s < 90) : K.vS s = vt s

theorem Cayley.Pack.vtxIdx_all {P : ℕ × (ℤ × ℤ × ℤ) × ℤ × ℤ × ℤ → Bool} (h : K.vtxIdx.all P = true) {t : ℕ} (ht : t < 90) : P (t, vt t, ↑(vt t).1.natAbs, ↑(vt t).2.1.natAbs, ↑(vt t).2.2.natAbs) = true

theorem Cayley.Pack.pGapOK_vertex (b : K.KBox) (hj : b.chart < 5) (hf : b.face < 6) (hlc : b.c.length = 5) (hlh : b.h.length = 5) (hmag : ∀ (i : Fin 5), |b.c.getD (↑i) 0| + |b.h.getD (↑i) 0| ≤ 2 * 2 ^ b.K) {s : ℕ} {w0 w1 : ℤ} (h : K.pGapOK b s w0 w1 = true) : s < 90 ∧ (w0 ≠ 0 ∨ w1 ≠ 0) ∧ K.gapNrmOK b (vt s) w0 w1 = true ∧ ∀ tt < 90, ∀ (t : Fin 5 → ℝ), (∀ (i : Fin 5), |t i| ≤ 1) → G1 b s w0 w1 t tt ∨ K.gPair b s = some tt ∧ K.pairOK b (vt s) w0 w1 = true

theorem Cayley.Pack.pGapOK_sound (b : K.KBox) (hj : b.chart < 5) (hf : b.face < 6) (hlc : b.c.length = 5) (hlh : b.h.length = 5) (hmag : ∀ (i : Fin 5), |b.c.getD (↑i) 0| + |b.h.getD (↑i) 0| ≤ 2 * 2 ^ b.K) {s : ℕ} {w0 w1 : ℤ} (h : K.pGapOK b s w0 w1 = true) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) (hpt : PtOK b.chart b.face (kpt b t)) : ¬RupPair (outerRot (kpt b t 0) (kpt b t 1)) (outerRot (kpt b t 0) (kpt b t 1) * Qm b.chart (rOf (kblow b.chart) b.face (kpt b t)))

Soundness of a kernel gap leaf.