The checker's packed bounds are sound

pLower, qLower and pStats (layouts L3, L5 of Cayley.Checker.KPack) bound polynomial expressions that fit the layout and have coefficient norm below 2^(PW-1).

def Cayley.Pack.L3 : Layout

Radix 3 in every variable.

Equations

• Cayley.Pack.L3 = { r := fun (x : Fin 5) => 3, s := ![1, 3, 9, 27, 81], n := 243 }

def Cayley.Pack.L5 : Layout

Radix 5 in t₀, t₁, 3 in the others.

Equations

• Cayley.Pack.L5 = { r := ![5, 5, 3, 3, 3], s := ![1, 5, 25, 75, 225], n := 675 }

def Cayley.Pack.goodB (L : Layout) : Bool

The mixed-radix facts as a Boolean check.

Equations

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

theorem Cayley.Pack.good_of (L : Layout) (h : goodB L = true) : L.Good

theorem Cayley.Pack.L3_good : L3.Good

theorem Cayley.Pack.L5_good : L5.Good

theorem Cayley.Pack.onesL3_eq : K.onesL3 = packN K.PW (fun (x : ℕ) => 1) L3.n

theorem Cayley.Pack.evensL3_eq : K.evensL3 = packN K.PW (evI L3) L3.n

theorem Cayley.Pack.onesL5_eq : K.onesL5 = packN K.PW (fun (x : ℕ) => 1) L5.n

theorem Cayley.Pack.evensL5_eq : K.evensL5 = packN K.PW (evI L5) L5.n

theorem Cayley.Pack.pX_eq : (fun (i : Fin 5) => K.pX ↑i) = kron L3

theorem Cayley.Pack.qX_eq : (fun (i : Fin 5) => K.qX ↑i) = kron L5

theorem Cayley.Pack.sum_lt_of_nrm {L : Layout} (hL : L.Good) {e : PE} (h : L.Fits e) (hb : e.nrm < O) : (∀ j < L.n, |L.cf e j| < ↑O) ∧ ∑ j ∈ Finset.range L.n, |L.cf e j| < ↑K.pM

theorem Cayley.Pack.pLower_le {e : PE} (h : L3.Fits e) (hb : e.nrm < O) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) : ↑(K.pLower (PE.ev (fun (i : Fin 5) => K.pX ↑i) e)) ≤ PE.ev t e

The packed lower bound (layout L3).

theorem Cayley.Pack.qLower_le {e : PE} (h : L5.Fits e) (hb : e.nrm < O) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) : ↑(K.qLower (PE.ev (fun (i : Fin 5) => K.qX ↑i) e)) ≤ PE.ev t e

The packed lower bound (layout L5).

theorem Cayley.Pack.pStats_sound {e : PE} (h : L3.Fits e) (hb : e.nrm < O) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) : have st := K.pStats (PE.ev (fun (i : Fin 5) => K.pX ↑i) e); ↑st.c0 - ↑st.slack ≤ PE.ev t e ∧ |PE.ev t e - ↑st.c0| ≤ ↑st.abs

The packed statistics (layout L3).