Semantics of kernel boxes, and the geometric core of a gap leaf

A point of a kernel box b at normalized coordinates t ∈ [-1,1]⁵ is X = (c + h t) / 2^K. gap_core turns two families of real inequalities (one per outer vertex, and the blown-up paired test) into ¬ RupPair.

def Cayley.faceR (face : ℕ) (s0 s1 : ℝ) : Fin 3 → ℝ

The blow-up direction on cube face .

Equations

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

def Cayley.kblow (chart : ℕ) : Bool

Charts 0 and 4 are blown up.

Equations

• Cayley.kblow chart = (decide (chart = 0) || decide (chart = 4))

def Cayley.rOf (blowup : Bool) (face : ℕ) (X : Fin 5 → ℝ) : Fin 3 → ℝ

The Cayley vector of a box point.

Equations

• Cayley.rOf blowup face X = if blowup = true then X 4 • Cayley.faceR face (X 2) (X 3) else ![X 2, X 3, X 4]

noncomputable def Cayley.kpt (b : K.KBox) (t : Fin 5 → ℝ) (i : Fin 5) : ℝ

The real point of a kernel box at normalized coordinates .

Equations

• Cayley.kpt b t i = (↑(b.c.getD (↑i) 0) + ↑(b.h.getD (↑i) 0) * t i) / 2 ^ b.K

structure Cayley.PtOK (chart face : ℕ) (X : Fin 5 → ℝ) : Prop

The pose-validity facts the leaf proofs need about a box point.

• disk : X 0 ^ 2 + X 1 ^ 2 ≤ 1
• rb (i : Fin 3) : |rOf (kblow chart) face X i| ≤ 2
• blow : kblow chart = true → 0 ≤ X 4 ∧ X 4 ≤ 2 ∧ |X 2| ≤ 1 ∧ |X 3| ≤ 1

def Cayley.Bad (chart face : ℕ) (X : Fin 5 → ℝ) : Prop

A box point that would be a reduced Rupert pose.

Equations

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

noncomputable def Cayley.NoR (X : Fin 5 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The outer numerator at a box point.

Equations

• Cayley.NoR X = Cayley.cayleyNumeratorMatrix (X 1) (-X 0) 0

noncomputable def Cayley.kapJ (j : ℕ) : ℝ

The chart weights κⱼ and the integer chart matrices Mⱼ = κⱼ Bⱼ, as reals.

Equations

• Cayley.kapJ j = ↑(Cayley.K.chartKI j)

noncomputable def Cayley.chartMR (j : ℕ) : Matrix (Fin 3) (Fin 3) ℝ

Equations

• Cayley.chartMR j = match Cayley.K.chartMI j with | (m00, m01, m02, m10, m11, m12, m20, m21, m22) => !![↑m00, ↑m01, ↑m02; ↑m10, ↑m11, ↑m12; ↑m20, ↑m21, ↑m22]

theorem Cayley.chartMR_eq (j : ℕ) (hj : j < 5) : chartMR j = kapJ j • chartB j

theorem Cayley.kapJ_ge (j : ℕ) : 1 ≤ kapJ j

Real-number facts

theorem Cayley.lin_smul (w0 w1 c : ℝ) (x : Fin 3 → ℝ) : lin w0 w1 (c • x) = c * lin w0 w1 x

theorem Cayley.lin_sub (w0 w1 : ℝ) (x y : Fin 3 → ℝ) : lin w0 w1 (x - y) = lin w0 w1 x - lin w0 w1 y

theorem Cayley.abs_mulVec_le {R : Matrix (Fin 3) (Fin 3) ℝ} (hR : R.transpose * R = 1) {e : Fin 3 → ℝ} {ε : ℝ} (he : ∀ (i : Fin 3), |e i| ≤ ε) (i : Fin 3) : |R.mulVec e i| ≤ 2 * ε

An orthogonal matrix moves each coordinate of an ε-small vector by at most 2ε.

theorem Cayley.abs_lin_mulVec_le {R : Matrix (Fin 3) (Fin 3) ℝ} (hR : R.transpose * R = 1) {e : Fin 3 → ℝ} {ε : ℝ} (he : ∀ (i : Fin 3), |e i| ≤ ε) (w0 w1 : ℝ) : |lin w0 w1 (R.mulVec e)| ≤ 2 * ε * (|w0| + |w1|)

theorem Cayley.gap_identity (w0 w1 : ℝ) (Ro B C : Matrix (Fin 3) (Fin 3) ℝ) (Do κ Dr : ℝ) (y z : Fin 3 → ℝ) : lin w0 w1 ((Do • Ro).mulVec ((κ • B * Dr • C).mulVec y)) - κ * Dr * lin w0 w1 ((Do • Ro).mulVec z) = Do * κ * Dr * (lin w0 w1 ((Ro * (B * C)).mulVec y) - lin w0 w1 (Ro.mulVec z))

theorem Cayley.num_sub_denom (r S : Fin 3 → ℝ) : (cayleyNumeratorMatrix (r 0) (r 1) (r 2)).mulVec S - cayleyDenom (r 0) (r 1) (r 2) • S = 2 • (crossR r S + crossR r (crossR r S))

theorem Cayley.crossR_smul_left (c : ℝ) (a b : Fin 3 → ℝ) : crossR (c • a) b = c • crossR a b

theorem Cayley.faceR_bound (face : ℕ) (s0 s1 : ℝ) (h0 : |s0| ≤ 1) (h1 : |s1| ≤ 1) (i : Fin 3) : |faceR face s0 s1 i| ≤ 1

theorem Cayley.crossR_bound {c e : Fin 3 → ℝ} {δ : ℝ} (hc : ∀ (i : Fin 3), |c i| ≤ 1) (he : ∀ (i : Fin 3), |e i| ≤ δ) (i : Fin 3) : |crossR c e i| ≤ 2 * δ

theorem Cayley.crossR_sub (c x y : Fin 3 → ℝ) : crossR c (x - y) = crossR c x - crossR c y

theorem Cayley.crossR_smul_right (a : ℝ) (c x : Fin 3 → ℝ) : crossR c (a • x) = a • crossR c x

theorem Cayley.chartB_zero_mulVec (v : Fin 3 → ℝ) : (chartB 0).mulVec v = v

The geometric core of a gap leaf

theorem Cayley.gap_core (chart face : ℕ) (hj : chart < 5) (X : Fin 5 → ℝ) (hpt : PtOK chart face X) (s : ℕ) (hs : s < 90) (w0 w1 : ℤ) (hw : w0 ≠ 0 ∨ w1 ≠ 0) (Ŝ : Fin 3 → ℝ) (hS : ∀ (i : Fin 3), |(vtx s - Ŝ) i| ≤ 1 / 2 ^ 60) (Th : ℕ → Fin 3 → ℝ) (hT : ∀ tt < 90, ∀ (i : Fin 3), |(vtx tt - Th tt) i| ≤ 1 / 2 ^ 60) (hv : ∀ tt < 90, 128 * kapJ chart * (1 / 2 ^ 60) * (|↑w0| + |↑w1|) ≤ cayleyDenom (X 1) (-X 0) 0 * kapJ chart * cayleyDenom (rOf (kblow chart) face X 0) (rOf (kblow chart) face X 1) (rOf (kblow chart) face X 2) * (lin (↑w0) (↑w1) ((outerRot (X 0) (X 1) * Qm chart (rOf (kblow chart) face X)).mulVec Ŝ) - lin (↑w0) (↑w1) ((outerRot (X 0) (X 1)).mulVec (Th tt))) ∨ (chart = 0 ∨ chart = 4) ∧ pairOf chart s = some tt ∧ 128 * kapJ chart * (1 / 2 ^ 60) * (|↑w0| + |↑w1|) ≤ 2 * lin (↑w0) (↑w1) ((NoR X).mulVec ((chartMR chart).mulVec (crossR (faceR face (X 2) (X 3)) Ŝ + X 4 • crossR (faceR face (X 2) (X 3)) (crossR (faceR face (X 2) (X 3)) Ŝ))))) : ¬RupPair (outerRot (X 0) (X 1)) (outerRot (X 0) (X 1) * Qm chart (rOf (kblow chart) face X))