Kronecker-packed kernel checker

A polynomial in t₀, …, t₄ with every exponent ≤ 2 is stored as the integer obtained by evaluating it at tᵢ = 2^(W·3ⁱ). This is a ring homomorphism, so polynomial arithmetic is a handful of big-integer operations, which the kernel evaluates with GMP. Coefficient statistics (constant term, sums of absolute values over a set of monomials) are read off with masks: after adding the offset 2^(W-1) to every slot, slot j holds coeff_j + 2^(W-1), its top bit is the sign, and a horizontal sum of slots is a remainder modulo 2^W - 1.

def Cayley.K.PW : Nat

Slot width in bits.

Equations

• Cayley.K.PW = 400

def Cayley.K.pM : Nat

2^PW - 1.

Equations

• Cayley.K.pM = 2 ^ Cayley.K.PW - 1

Layouts

Layout L3: tᵢ = 2^(PW·3ⁱ) (243 slots, exponents ≤ 2). Layout L5: t₀ = 2^PW, t₁ = 2^(5PW), t₂, t₃, t₄ = 2^(25PW), 2^(75PW), 2^(225PW) (675 slots, exponents ≤ 4 in t₀, t₁ and ≤ 2 in the others).

def Cayley.K.pX (i : Nat) : Int

The variable tᵢ of layout L3.

Equations

• Cayley.K.pX i = ↑(2 ^ (Cayley.K.PW * 3 ^ i))

def Cayley.K.qX (i : Nat) : Int

The variable tᵢ of layout L5.

Equations

• Cayley.K.qX i = ↑(2 ^ (Cayley.K.PW * if i = 0 then 1 else if i = 1 then 5 else 25 * 3 ^ (i - 2)))

def Cayley.K.geo3 (y : Nat) : Nat

1 + y + y² and 1 + y².

Equations

• Cayley.K.geo3 y = (Nat.add 1 y).add (y.mul y)

def Cayley.K.ev3 (y : Nat) : Nat

Equations

• Cayley.K.ev3 y = Nat.add 1 (y.mul y)

def Cayley.K.geo5 (y : Nat) : Nat

1 + y + y² + y³ + y⁴ and 1 + y² + y⁴.

Equations

• Cayley.K.geo5 y = ((y.mul y).mul (Cayley.K.geo3 y)).add (Nat.add 1 y)

def Cayley.K.ev5 (y : Nat) : Nat

Equations

• Cayley.K.ev5 y = Nat.add 1 ((y.mul y).mul (Cayley.K.ev3 y))

def Cayley.K.onesL3 : Nat

Slot indicators (Σ 2^(PW j) over all slots, and over the all-even monomials).

def Cayley.K.evensL3 : Nat

def Cayley.K.onesL5 : Nat

def Cayley.K.evensL5 : Nat

structure Cayley.K.PStats : Type

Statistics of a packed polynomial P: constant term, slack with P ≥ c0 − slack on [-1,1]⁵ (even monomials only count when negative), and abs with |P − c0| ≤ abs.

• c0 : Int
• slack : Nat
• abs : Nat

@[inline]

def Cayley.K.pParts (ones N : Nat) : Nat × Nat

Positive and negative parts of the slots of N = P + offset.

Equations

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

def Cayley.K.pStatsL (ones evens : Nat) (P : Int) : PStats

Equations

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

def Cayley.K.pLowerL (ones evens : Nat) (P : Int) : Int

Lower bound of a packed polynomial on [-1,1]⁵.

Equations

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

def Cayley.K.pStats (P : Int) : PStats

Equations

• Cayley.K.pStats P = Cayley.K.pStatsL Cayley.K.onesL3 Cayley.K.evensL3 P

def Cayley.K.pLower (P : Int) : Int

Equations

• Cayley.K.pLower P = Cayley.K.pLowerL Cayley.K.onesL3 Cayley.K.evensL3 P

def Cayley.K.qLower (P : Int) : Int

Equations

• Cayley.K.qLower P = Cayley.K.pLowerL Cayley.K.onesL5 Cayley.K.evensL5 P

Bernstein coefficients (layout L3)

On [-1,1] the quadratic Bernstein coefficients of a₀ + a₁t + a₂t² are (a₀ − a₁ + a₂, a₀ − a₂, a₀ + a₁ + a₂); baxis i applies this along variable i to every slot, and a polynomial is at least its least Bernstein coefficient. The transform works on the offset encoding (every slot holds coeff + 2^(PW-1)) in Nat arithmetic only, which the kernel evaluates much faster than Int.

def Cayley.K.zL3 (i : Nat) : Nat

Slot indicator of the slots whose digit i is 0.

Equations

• Cayley.K.zL3 i = Cayley.K.onesL3.div (Cayley.K.geo3 (Cayley.K.pX i).toNat)

def Cayley.K.baxis (i N : Nat) : Nat

The Bernstein transform along variable i of an offset-encoded packed polynomial.

Equations

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

def Cayley.K.bern3 (N : Nat) : Nat

The Bernstein coefficients of an offset-encoded packed polynomial.

Equations

• Cayley.K.bern3 N = Cayley.K.baxis 4 (Cayley.K.baxis 3 (Cayley.K.baxis 2 (Cayley.K.baxis 1 (Cayley.K.baxis 0 N))))

def Cayley.K.bernGE (P m : Int) : Bool

Every Bernstein coefficient of the packed polynomial P is at least m.

Equations

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

structure Cayley.K.GData (R : Type) : Type

The per-box polynomials of a gap leaf, over any arithmetic: α₀, α₁, α₂ (outer rows, weighted by w), β = M N(r) S, κD, and the paired inner vector L (blown-up charts).

• a0 : R
• a1 : R
• a2 : R
• b0 : R
• b1 : R
• b2 : R
• kd : R
• l0 : R
• l1 : R
• l2 : R

def Cayley.K.gChart {R : Type} (sub mul : R → R → R) (c : Int → R) (add : R → R → R) (chart : Nat) (y0 y1 y2 : R) : R × R × R

M_j v; the Klein charts are sign flips.

Equations

• One or more equations did not get rendered due to their size.
• Cayley.K.gChart sub mul c add 0 y0 y1 y2 = (y0, y1, y2)
• Cayley.K.gChart sub mul c add 1 y0 y1 y2 = (y0, sub (c 0) y1, sub (c 0) y2)
• Cayley.K.gChart sub mul c add 2 y0 y1 y2 = (sub (c 0) y0, y1, sub (c 0) y2)
• Cayley.K.gChart sub mul c add 3 y0 y1 y2 = (sub (c 0) y0, sub (c 0) y1, y2)

def Cayley.K.gFace {R : Type} (face : Nat) (sg s0 s1 : R) : R × R × R

The blow-up direction on cube face face, with sign entry sg.

Equations

• Cayley.K.gFace face sg s0 s1 = if face / 2 = 0 then (sg, s0, s1) else if face / 2 = 1 then (s1, sg, s0) else (s0, s1, sg)

def Cayley.K.gapCore {R : Type} (add sub mul : R → R → R) (c : Int → R) (x : Fin 5 → R) (chart face : Nat) (U : R) (cc hh : Nat → R) (sx sy sz w0 w1 : R) : GData R

The gap-leaf polynomials, generic in the arithmetic (x i is the variable tᵢ), with the box data (scale U, centres cc, radii hh), the inner vertex and the direction as inputs.

Equations

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

def Cayley.K.gapGen {R : Type} (add sub mul : R → R → R) (c : Int → R) (x : Fin 5 → R) (b : KBox) (S : Int × Int × Int) (w0 w1 : Int) : GData R

The gap-leaf polynomials of box b, inner vertex S and direction (w0, w1).

Equations

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

def Cayley.K.pGapData (b : KBox) (S : Int × Int × Int) (w0 w1 : Int) : GData Int

The gap-leaf data in packed integers.

Equations

• Cayley.K.pGapData b S w0 w1 = Cayley.K.gapGen Int.add Int.sub Int.mul (fun (z : Int) => z) (fun (i : Fin 5) => Cayley.K.pX ↑i) b S w0 w1

def Cayley.K.nrmOK (b : KBox) (w0 w1 : Int) : Bool

The norm guard of a gap leaf: the box scale and the direction are small enough that the coefficient norms of every polynomial the leaf decodes stay below 2^390 (proved once, on the worst box, in Cayley.Pack.gapNrmOK_worst).

Equations

• Cayley.K.nrmOK b w0 w1 = (b.K.ble 16 && w0.natAbs.ble 1024 && w1.natAbs.ble 1024)

def Cayley.K.gapSc (b : KBox) : Nat

Scale exponents of A and of L beyond 2^160.

Equations

• Cayley.K.gapSc b = if b.chart = 0 ∨ b.chart = 4 then 6 * b.K else 4 * b.K

def Cayley.K.gapScL (b : KBox) : Nat

Equations

• Cayley.K.gapScL b = 5 * b.K

The gap leaf

def Cayley.K.gErr (b : KBox) (w0 w1 : Int) : Int

The error allowance of a gap leaf (for A) and of the paired test (for L).

Equations

• Cayley.K.gErr b w0 w1 = 128 * Cayley.K.chartKI b.chart * (↑w0.natAbs + ↑w1.natAbs) * Cayley.K.p2 (Cayley.K.gapSc b + 100)

def Cayley.K.gErrL (b : KBox) (w0 w1 : Int) : Int

Equations

• Cayley.K.gErrL b w0 w1 = 128 * Cayley.K.chartKI b.chart * (↑w0.natAbs + ↑w1.natAbs) * Cayley.K.p2 (Cayley.K.gapScL b + 100)

def Cayley.K.gA (g : GData Int) : Int

A = Σ αₖ βₖ, L = Σ αₖ Lₖ, Eₖ = αₖ κD, F_T = A − (Σ Tₖ αₖ) κD.

Equations

• Cayley.K.gA g = ((g.a0.mul g.b0).add (g.a1.mul g.b1)).add (g.a2.mul g.b2)

def Cayley.K.gL (g : GData Int) : Int

Equations

• Cayley.K.gL g = ((g.a0.mul g.l0).add (g.a1.mul g.l1)).add (g.a2.mul g.l2)

def Cayley.K.gF (g : GData Int) (tx ty tz : Int) : Int

Equations

• Cayley.K.gF g tx ty tz = (Cayley.K.gA g).sub ((((tx.mul g.a0).add (ty.mul g.a1)).add (tz.mul g.a2)).mul g.kd)

def Cayley.K.fullOK (b : KBox) (S : Int × Int × Int) (w0 w1 tx ty tz : Int) : Bool

The exact test against outer vertex T, and the paired test.

Equations

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

def Cayley.K.pairOK (b : KBox) (S : Int × Int × Int) (w0 w1 : Int) : Bool

Equations

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

def Cayley.K.gPair (b : KBox) (s : Nat) : Option Nat

The paired vertex of inner vertex s (blown-up charts).

Equations

• Cayley.K.gPair b s = if b.chart = 0 ∨ b.chart = 4 then Cayley.K.kPair b.chart s else none

def Cayley.K.vtestG (b : KBox) (s : Nat) (S : Int × Int × Int) (w0 w1 : Int) (t : Nat) (tx ty tz : Int) : Bool

The test of outer vertex t after the packed quick test (S is inner vertex s).

Equations

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

def Cayley.K.vS (s : Nat) : Int × Int × Int

Vertex s, read from the packed tables (cheaper in the kernel than indexing vtxI).

Equations

• Cayley.K.vS s = (Cayley.K.slot Cayley.K.tpx s - ↑(2 ^ 170), Cayley.K.slot Cayley.K.tpy s - ↑(2 ^ 170), Cayley.K.slot Cayley.K.tpz s - ↑(2 ^ 170))

def Cayley.K.quickQ (b : KBox) (S : Int × Int × Int) (w0 w1 : Int) : Int

The quick test's constant part c₀(A) − slack(A) − err, and the statistics of Eₖ.

Equations

• Cayley.K.quickQ b S w0 w1 = (Cayley.K.pStats (Cayley.K.gA (Cayley.K.pGapData b S w0 w1))).c0 - ↑(Cayley.K.pStats (Cayley.K.gA (Cayley.K.pGapData b S w0 w1))).slack - Cayley.K.gErr b w0 w1

def Cayley.K.quickE (b : KBox) (S : Int × Int × Int) (w0 w1 : Int) : PStats × PStats × PStats

Equations

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

def Cayley.K.quickV (C e00 e01 e02 : Int) (n0 n1 n2 : Nat) : Nat

The packed quick-test number: slot t is 2^639 + quick_T when the packing bounds hold.

Equations

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

def Cayley.K.pGapOK (b : KBox) (s : Nat) (w0 w1 : Int) : Bool

Packed kernel gap leaf.

Equations

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

Domain leaves

@[reducible, inline]

abbrev Cayley.K.I9 : Type

Equations

• Cayley.K.I9 = (Int × Int × Int × Int × Int × Int × Int × Int × Int)

structure Cayley.K.NM (R : Type) : Type

A 3×3 matrix of polynomials and a scalar.

• n00 : R
• n01 : R
• n02 : R
• n10 : R
• n11 : R
• n12 : R
• n20 : R
• n21 : R
• n22 : R
• d : R

def Cayley.K.numGen {R : Type} (add sub mul : R → R → R) (c : Int → R) (x : Fin 5 → R) (b : KBox) : NM R

The Cayley numerator N(r) and the denominator D of a box, generic in the arithmetic.

Equations

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

def Cayley.K.numSc (b : KBox) : Int

The scale R² of N (U⁴ blown up, U² plain).

Equations

• Cayley.K.numSc b = if b.chart = 0 ∨ b.chart = 4 then Cayley.K.p2 b.K * Cayley.K.p2 b.K * (Cayley.K.p2 b.K * Cayley.K.p2 b.K) else Cayley.K.p2 b.K * Cayley.K.p2 b.K

def Cayley.K.trGen {R : Type} (add mul : R → R → R) (c : Int → R) (X : I9) (N : NM R) : R

tr(Xᵀ N) = Σ X_ab N_ab for an integer matrix X.

Equations

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

def Cayley.K.chartGen {R : Type} (add sub mul : R → R → R) (c : Int → R) (x : Fin 5 → R) (b : KBox) (k : Nat) : R

The chart-test polynomial κⱼ tr((Mⱼᵀ M_k)ᵀ N) − κ_k tr((Mⱼᵀ Mⱼ)ᵀ N).

Equations

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

def Cayley.K.orbC (g a : Nat) : I9

C = M_a · 2^80 R̂z(g)ᵀ (integer).

Equations

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

def Cayley.K.m3 {R : Type} (add mul : R → R → R) (c : Int → R) (M : I9) (N : NM R) : NM R

M N for an integer matrix M (the scalar is kept).

Equations

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

def Cayley.K.m3t {R : Type} (N : NM R) : NM R

Transpose.

Equations

• Cayley.K.m3t N = { n00 := N.n00, n01 := N.n10, n02 := N.n20, n10 := N.n01, n11 := N.n11, n12 := N.n21, n20 := N.n02, n21 := N.n12, n22 := N.n22, d := N.d }

def Cayley.K.frob {R : Type} (add mul : R → R → R) (H W : NM R) : R

Σ_ab H_ab W_ab.

Equations

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

def Cayley.K.hGen {R : Type} (add sub mul : R → R → R) (c : Int → R) (u v U : R) : NM R

H = N_oᵀ diag(-1,-1,1) N_o for the outer numerator N_o = N(v, -u, 0)·U².

Equations

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

def Cayley.K.orbGen {R : Type} (add sub mul : R → R → R) (c : Int → R) (x : Fin 5 → R) (b : KBox) (e g a : Nat) : R × R

The two orbit-test polynomials (score of the orbit element minus the scores of Q).

Equations

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

def Cayley.K.qXv (i : Fin 5) : Int

The variables of layout L5.

Equations

• Cayley.K.qXv i = Cayley.K.qX ↑i

def Cayley.K.chartNrmOK (b : KBox) (k : Nat) : Bool

The norm guard of a domain polynomial (the Nat instance).

Equations

• Cayley.K.chartNrmOK b k = (Cayley.K.chartGen Nat.add Nat.add Nat.mul Int.natAbs (fun (x : Fin 5) => 1) b k).blt (2 ^ 399)

def Cayley.K.orbNrmOK (b : KBox) (e g a : Nat) : Bool

Equations

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

def Cayley.K.pChartOK (b : KBox) (k : Nat) : Bool

Kernel chart test: chart k beats the box's chart j on the whole box.

Equations

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

def Cayley.K.orbErr (b : KBox) (e : Nat) : Int

The orbit-test error allowance.

Equations

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

def Cayley.K.pOrbitOK (b : KBox) (e g a : Nat) : Bool

Kernel orbit test: the orbit element H^e Q ĝ_g (score base a) beats Q.

Equations

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

def Cayley.K.pDomOK (b : KBox) (code : Nat) : Bool

Packed kernel domain leaf.

Equations

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