Soundness of the kernel domain leaves

The chart test

def Cayley.Pack.chartPE (b : K.KBox) (k : ℕ) : PE

The chart-test expression.

Equations

• Cayley.Pack.chartPE b k = Cayley.K.chartGen Cayley.Pack.PE.add Cayley.Pack.PE.sub Cayley.Pack.PE.mul Cayley.Pack.PE.c Cayley.Pack.PE.x b k

theorem Cayley.Pack.chartPE_int (b : K.KBox) (k : ℕ) : PE.ev pXv (chartPE b k) = K.chartGen Int.add Int.sub Int.mul (fun (z : ℤ) => z) (fun (i : Fin 5) => K.pX ↑i) b k

theorem Cayley.Pack.chartPE_real (b : K.KBox) (k : ℕ) (t : Fin 5 → ℝ) : PE.ev t (chartPE b k) = K.chartGen (fun (x1 x2 : ℝ) => x1 + x2) (fun (x1 x2 : ℝ) => x1 - x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) t b k

theorem Cayley.Pack.chartPE_nrm (b : K.KBox) (k : ℕ) : (chartPE b k).nrm = K.chartGen Nat.add Nat.add Nat.mul Int.natAbs (fun (x : Fin 5) => 1) b k

theorem Cayley.Pack.chartPE_fits (b : K.KBox) (hj : b.chart < 5) (hf : b.face < 6) (k : ℕ) (hk : k < 5) : L3.Fits (chartPE b k)

theorem Cayley.Pack.pChartOK_sound (b : K.KBox) (hj : b.chart < 5) (hf : b.face < 6) {k : ℕ} (hk : k < 5) (h : K.pChartOK b k = true) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) : ((chartB b.chart).transpose * Qm b.chart (rOf (kblow b.chart) b.face (kpt b t))).trace < ((chartB k).transpose * Qm b.chart (rOf (kblow b.chart) b.face (kpt b t))).trace

The orbit test

theorem Cayley.Pack.Hmat_mem_SO3 (u v : ℝ) : Hmat u v ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ

theorem Cayley.Pack.entry_le_one {Z : Matrix (Fin 3) (Fin 3) ℝ} (hZ : Z ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) (a c : Fin 3) : |Z a c| ≤ 1

theorem Cayley.Pack.trace_mul_approx {Z : Matrix (Fin 3) (Fin 3) ℝ} (hZ : Z ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) {G G' : Matrix (Fin 3) (Fin 3) ℝ} {ε : ℝ} (hG : ∀ (a c : Fin 3), |G a c - G' a c| ≤ ε) : |(Z * G).trace - (Z * G').trace| ≤ 9 * ε

def Cayley.Pack.orbPE (b : K.KBox) (e g a : ℕ) : PE × PE

The orbit-test expressions.

Equations

• Cayley.Pack.orbPE b e g a = Cayley.K.orbGen Cayley.Pack.PE.add Cayley.Pack.PE.sub Cayley.Pack.PE.mul Cayley.Pack.PE.c Cayley.Pack.PE.x b e g a

theorem Cayley.Pack.orbPE_ev {R : Type} [CommRing R] (v : Fin 5 → R) (b : K.KBox) (e g a : ℕ) : PE.ev v (orbPE b e g a).1 = (K.orbGen (fun (x1 x2 : R) => x1 + x2) (fun (x1 x2 : R) => x1 - x2) (fun (x1 x2 : R) => x1 * x2) (fun (z : ℤ) => ↑z) v b e g a).1 ∧ PE.ev v (orbPE b e g a).2 = (K.orbGen (fun (x1 x2 : R) => x1 + x2) (fun (x1 x2 : R) => x1 - x2) (fun (x1 x2 : R) => x1 * x2) (fun (z : ℤ) => ↑z) v b e g a).2

theorem Cayley.Pack.orbPE_nrm (b : K.KBox) (e g a : ℕ) : (orbPE b e g a).1.nrm = (K.orbGen Nat.add Nat.add Nat.mul Int.natAbs (fun (x : Fin 5) => 1) b e g a).1 ∧ (orbPE b e g a).2.nrm = (K.orbGen Nat.add Nat.add Nat.mul Int.natAbs (fun (x : Fin 5) => 1) b e g a).2

theorem Cayley.Pack.orbPE_deg (b : K.KBox) (hj : b.chart < 5) (hf : b.face < 6) (e : ℕ) (he : e < 2) (g a : ℕ) (ha : a = 0 ∨ a = 4) (i : Fin 5) : PE.deg i (orbPE b e g a).1 ≤ dBound e i ∧ PE.deg i (orbPE b e g a).2 ≤ dBound e i

noncomputable def Cayley.Pack.orbK (b : K.KBox) (e : ℕ) (t : Fin 5 → ℝ) : ℝ

The orbit scale.

Equations

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

noncomputable def Cayley.Pack.orbY (b : K.KBox) (e : ℕ) (t : Fin 5 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The orbit element Y.

Equations

• Cayley.Pack.orbY b e t = if e = 0 then 1 else Cayley.Hmat (Cayley.kpt b t 0) (Cayley.kpt b t 1)

theorem Cayley.Pack.L5_fits_of {e : PE} (h : ∀ (i : Fin 5), PE.deg i e ≤ dBound 1 i) : L5.Fits e

theorem Cayley.Pack.L3_fits_of {e : PE} (h : ∀ (i : Fin 5), PE.deg i e ≤ dBound 0 i) : L3.Fits e

theorem Cayley.Pack.orbit_bounds (b : K.KBox) (hj : b.chart < 5) (hf : b.face < 6) {e g a : ℕ} (he : e < 2) (hg : g < 15) (ha : a = 0 ∨ a = 4) (h : K.pOrbitOK b e g a = true) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) : have r := rOf (kblow b.chart) b.face (kpt b t); have Q := Qm b.chart r; have F := ((chartB a).transpose * (orbY b e t * Q) * gHat g).trace - if a = 4 then 1 / 8 else 0; ↑(K.orbErr b e) < orbK b e t * (F - Q.trace) ∧ ↑(K.orbErr b e) < orbK b e t * (F - ((tauR.transpose * Q).trace - 1 / 8))

A passing orbit test bounds both score differences from below.

theorem Cayley.Pack.pOrbitOK_sound (b : K.KBox) (hj : b.chart < 5) (hf : b.face < 6) {e g a : ℕ} (he : e < 2) (hg : g < 15) (ha : a = 0 ∨ a = 4) (h : K.pOrbitOK b e g a = true) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) (hpt : PtOK b.chart b.face (kpt b t)) : Fsc (Qm b.chart (rOf (kblow b.chart) b.face (kpt b t))) < Fsc (orbY b e t * Qm b.chart (rOf (kblow b.chart) b.face (kpt b t)) * gR g)

Soundness of a kernel orbit leaf.

The domain leaf

theorem Cayley.Pack.kpt_ge (b : K.KBox) (t : Fin 5 → ℝ) (ht : ∀ (i : Fin 5), |t i| ≤ 1) (i : Fin 5) (hh : 0 ≤ b.h.getD (↑i) 0) : ↑(b.c.getD (↑i) 0 - b.h.getD (↑i) 0) / 2 ^ b.K ≤ kpt b t i ∧ kpt b t i ≤ ↑(b.c.getD (↑i) 0 + b.h.getD (↑i) 0) / 2 ^ b.K

theorem Cayley.Pack.pDomOK_sound (b : K.KBox) (hj : b.chart < 5) (hf : b.face < 6) (hh : ∀ (i : Fin 5), 0 ≤ b.h.getD (↑i) 0) {code : ℕ} (h : K.pDomOK b code = true) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) (hpt : PtOK b.chart b.face (kpt b t)) : ¬Reduced (kpt b t 0) (kpt b t 1) b.chart (rOf (kblow b.chart) b.face (kpt b t))

Soundness of a kernel domain leaf.