Soundness of the packed lower bound

For a polynomial expression e that fits a layout and has nrm e < 2^(PW-12), the checker's mask computation pLowerL applied to e evaluated at the Kronecker point is a lower bound of e on [-1,1]⁵; similarly for the fields of pStatsL.

Masks on packed numbers

theorem Cayley.Pack.land_mask {W n : ℕ} {d m : ℕ → ℕ} (hd : ∀ j < n, d j < 2 ^ W) (hm : ∀ j < n, m j ≤ 1) : packN W d n &&& packN W (fun (j : ℕ) => (2 ^ W - 1) * m j) n = packN W (fun (j : ℕ) => m j * d j) n

theorem Cayley.Pack.packN_ind0 {W n : ℕ} (hn : 0 < n) (a : ℕ) : packN W (fun (j : ℕ) => if j = 0 then a else 0) n = a

The decode

The checker writes Nat.land a b etc.; these are the notations.

theorem Cayley.Pack.nat_land (a b : ℕ) : a.land b = a &&& b

theorem Cayley.Pack.nat_shiftRight (a b : ℕ) : a.shiftRight b = a >>> b

theorem Cayley.Pack.nat_mul (a b : ℕ) : a.mul b = a * b

theorem Cayley.Pack.nat_add (a b : ℕ) : a.add b = a + b

theorem Cayley.Pack.nat_sub (a b : ℕ) : a.sub b = a - b

theorem Cayley.Pack.nat_mod (a b : ℕ) : a.mod b = a % b

theorem Cayley.Pack.pM_eq : K.pM = 2 ^ K.PW - 1

theorem Cayley.Pack.PW_pos : 0 < K.PW

def Cayley.Pack.O : ℕ

The offset 2^(PW-1).

Equations

• Cayley.Pack.O = 2 ^ (Cayley.K.PW - 1)

theorem Cayley.Pack.O_lt : O < 2 ^ K.PW

theorem Cayley.Pack.O_pos : 0 < O

theorem Cayley.Pack.digit_lt {c : ℤ} (hc : |c| < ↑O) : (c + ↑O).toNat < 2 ^ K.PW

Numbers of the form 2^(PW-1) + c with |c| < 2^(PW-1).

def Cayley.Pack.odig (c : ℕ → ℤ) (j : ℕ) : ℕ

Offset digits.

Equations

• Cayley.Pack.odig c j = (c j + ↑Cayley.Pack.O).toNat

theorem Cayley.Pack.odig_lt {c : ℕ → ℤ} {n : ℕ} (hc : ∀ j < n, |c j| < ↑O) (j : ℕ) : j < n → odig c j < 2 ^ K.PW

theorem Cayley.Pack.odig_div {c : ℤ} (hc : |c| < ↑O) : (c + ↑O).toNat / O = if 0 ≤ c then 1 else 0

The sign of an offset digit.

theorem Cayley.Pack.pParts_eq {n : ℕ} (c : ℕ → ℤ) (hc : ∀ j < n, |c j| < ↑O) : K.pParts (packN K.PW (fun (x : ℕ) => 1) n) (packN K.PW (odig c) n) = (packN K.PW (fun (j : ℕ) => (max (c j) 0).toNat) n, packN K.PW (fun (j : ℕ) => (max (-c j) 0).toNat) n)

pParts on offset digits gives the positive and negative parts.

Masks of a layout

def Cayley.Pack.kron (L : Layout) (i : Fin 5) : ℤ

The Kronecker point of a layout.

Equations

• Cayley.Pack.kron L i = 2 ^ (Cayley.K.PW * L.s i)

def Cayley.Pack.evI (L : Layout) (j : ℕ) : ℕ

Slot indicators.

Equations

• Cayley.Pack.evI L j = if L.evSlot j = true then 1 else 0

def Cayley.Pack.oddI (L : Layout) (j : ℕ) : ℕ

Equations

• Cayley.Pack.oddI L j = if L.evSlot j = true then 0 else 1

def Cayley.Pack.nzI (j : ℕ) : ℕ

Equations

• Cayley.Pack.nzI j = if j = 0 then 0 else 1

theorem Cayley.Pack.mask_odd (L : Layout) : K.pM * (packN K.PW (fun (x : ℕ) => 1) L.n - packN K.PW (evI L) L.n) = packN K.PW (fun (j : ℕ) => (2 ^ K.PW - 1) * oddI L j) L.n

theorem Cayley.Pack.mask_nz (L : Layout) (hn : 0 < L.n) : K.pM * packN K.PW (fun (x : ℕ) => 1) L.n - K.pM = packN K.PW (fun (j : ℕ) => (2 ^ K.PW - 1) * nzI j) L.n

theorem Cayley.Pack.mask_evnz (L : Layout) (hn : 0 < L.n) (h0 : L.evSlot 0 = true) : K.pM * (packN K.PW (evI L) L.n - 1) = packN K.PW (fun (j : ℕ) => (2 ^ K.PW - 1) * (evI L j * nzI j)) L.n

The encoding

theorem Cayley.Pack.enc_eq {L : Layout} (hL : L.Good) {e : PE} (h : L.Fits e) (hc : ∀ j < L.n, |L.cf e j| < ↑O) : ((PE.ev (kron L) e).add ↑(2 ^ (K.PW - 1) * packN K.PW (fun (x : ℕ) => 1) L.n)).toNat = packN K.PW (odig (L.cf e)) L.n

The checker's Nat encoding of e at the Kronecker point is the packed offset digits.

The lower bound in closed form

noncomputable def Cayley.Pack.posC (L : Layout) (e : PE) (j : ℕ) : ℕ

Positive and negative parts of the slot coefficients.

Equations

• Cayley.Pack.posC L e j = (max (L.cf e j) 0).toNat

noncomputable def Cayley.Pack.negC (L : Layout) (e : PE) (j : ℕ) : ℕ

Equations

• Cayley.Pack.negC L e j = (max (-L.cf e j) 0).toNat

theorem Cayley.Pack.posC_add_negC (L : Layout) (e : PE) (j : ℕ) : ↑(posC L e j + negC L e j) = |L.cf e j|

theorem Cayley.Pack.posC_lt {L : Layout} {e : PE} {j : ℕ} (hc : |L.cf e j| < ↑O) : posC L e j < 2 ^ K.PW

theorem Cayley.Pack.negC_lt {L : Layout} {e : PE} {j : ℕ} (hc : |L.cf e j| < ↑O) : negC L e j < 2 ^ K.PW

theorem Cayley.Pack.oddI_le (L : Layout) (j : ℕ) : oddI L j ≤ 1

theorem Cayley.Pack.nzI_le (j : ℕ) : nzI j ≤ 1

noncomputable def Cayley.Pack.slackC (L : Layout) (e : PE) : ℕ

The slack of the lower bound.

Equations

• Cayley.Pack.slackC L e = ∑ j ∈ Finset.range L.n, (Cayley.Pack.oddI L j * Cayley.Pack.posC L e j + Cayley.Pack.nzI j * Cayley.Pack.negC L e j)

theorem Cayley.Pack.slackC_le (L : Layout) (e : PE) : ↑(slackC L e) ≤ ∑ j ∈ Finset.range L.n, |L.cf e j|

theorem Cayley.Pack.pLowerL_eq {L : Layout} (hL : L.Good) {e : PE} (h : L.Fits e) (hn : 0 < L.n) (hc : ∀ j < L.n, |L.cf e j| < ↑O) (hS : ∑ j ∈ Finset.range L.n, |L.cf e j| < ↑K.pM) : K.pLowerL (packN K.PW (fun (x : ℕ) => 1) L.n) (packN K.PW (evI L) L.n) (PE.ev (kron L) e) = L.cf e 0 - ↑(slackC L e)

Real-valued bounds

theorem Cayley.Pack.mono_abs_le {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) (k : Fin 5 → ℕ) : |∏ i : Fin 5, t i ^ k i| ≤ 1

theorem Cayley.Pack.mono_nonneg (t : Fin 5 → ℝ) {k : Fin 5 → ℕ} (hk : ∀ (i : Fin 5), Even (k i)) : 0 ≤ ∏ i : Fin 5, t i ^ k i

theorem Cayley.Pack.evSlot_even {L : Layout} {j : ℕ} (h : L.evSlot j = true) (i : Fin 5) : Even (L.dig j i)

theorem Cayley.Pack.evSlot_zero (L : Layout) : L.evSlot 0 = true

theorem Cayley.Pack.dig_zero (L : Layout) (i : Fin 5) : L.dig 0 i = 0

theorem Cayley.Pack.slot_le {L : Layout} {e : PE} {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) (j : ℕ) : (if j = 0 then ↑(L.cf e j) else 0) - ↑(oddI L j * posC L e j + nzI j * negC L e j) ≤ ↑(L.cf e j) * ∏ i : Fin 5, t i ^ L.dig j i

One slot's contribution.

theorem Cayley.Pack.lower_le_ev {L : Layout} (hL : L.Good) {e : PE} (h : L.Fits e) (hn : 0 < L.n) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) : ↑(L.cf e 0 - ↑(slackC L e)) ≤ PE.ev t e

The statistics

noncomputable def Cayley.Pack.absC (L : Layout) (e : PE) : ℕ

The absolute deviation bound.

Equations

• Cayley.Pack.absC L e = ∑ j ∈ Finset.range L.n, Cayley.Pack.nzI j * (Cayley.Pack.posC L e j + Cayley.Pack.negC L e j)

theorem Cayley.Pack.abs_ev_sub_le {L : Layout} (hL : L.Good) {e : PE} (h : L.Fits e) (hn : 0 < L.n) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) : |PE.ev t e - ↑(L.cf e 0)| ≤ ↑(absC L e)

theorem Cayley.Pack.pStatsL_eq {L : Layout} (hL : L.Good) {e : PE} (h : L.Fits e) (hn : 0 < L.n) (hc : ∀ j < L.n, |L.cf e j| < ↑O) (hS : ∑ j ∈ Finset.range L.n, |L.cf e j| < ↑K.pM) : have st := K.pStatsL (packN K.PW (fun (x : ℕ) => 1) L.n) (packN K.PW (evI L) L.n) (PE.ev (kron L) e); st.c0 = L.cf e 0 ∧ st.slack = slackC L e ∧ st.abs = absC L e

The statistics of the checker, in closed form.