The gap-leaf polynomials

gapGen is generic in the arithmetic, so its integer instance (the checker) and its PE instance (polynomial expressions) are related by evaluation, and so is its real instance.

theorem Cayley.Pack.gChart_map {R S : Type} (addR subR mulR : R → R → R) (cR : ℤ → R) (addS subS mulS : S → S → S) (cS : ℤ → S) (f : R → S) (hadd : ∀ (a b : R), f (addR a b) = addS (f a) (f b)) (hsub : ∀ (a b : R), f (subR a b) = subS (f a) (f b)) (hmul : ∀ (a b : R), f (mulR a b) = mulS (f a) (f b)) (hc : ∀ (z : ℤ), f (cR z) = cS z) (chart : ℕ) (y0 y1 y2 : R) : (f (K.gChart subR mulR cR addR chart y0 y1 y2).1, f (K.gChart subR mulR cR addR chart y0 y1 y2).2.1, f (K.gChart subR mulR cR addR chart y0 y1 y2).2.2) = K.gChart subS mulS cS addS chart (f y0) (f y1) (f y2)

theorem Cayley.Pack.gFace_map {R S : Type} (f : R → S) (face : ℕ) (a b c : R) : f (K.gFace face a b c).1 = (K.gFace face (f a) (f b) (f c)).1 ∧ f (K.gFace face a b c).2.1 = (K.gFace face (f a) (f b) (f c)).2.1 ∧ f (K.gFace face a b c).2.2 = (K.gFace face (f a) (f b) (f c)).2.2

theorem Cayley.Pack.gapGen_map {R S : Type} (addR subR mulR : R → R → R) (cR : ℤ → R) (xR : Fin 5 → R) (addS subS mulS : S → S → S) (cS : ℤ → S) (xS : Fin 5 → S) (f : R → S) (hadd : ∀ (a b : R), f (addR a b) = addS (f a) (f b)) (hsub : ∀ (a b : R), f (subR a b) = subS (f a) (f b)) (hmul : ∀ (a b : R), f (mulR a b) = mulS (f a) (f b)) (hc : ∀ (z : ℤ), f (cR z) = cS z) (hx : ∀ (i : Fin 5), f (xR i) = xS i) (b : K.KBox) (s : ℤ × ℤ × ℤ) (w0 w1 : ℤ) : have g := K.gapGen addR subR mulR cR xR b s w0 w1; have g' := K.gapGen addS subS mulS cS xS b s w0 w1; f g.a0 = g'.a0 ∧ f g.a1 = g'.a1 ∧ f g.a2 = g'.a2 ∧ f g.b0 = g'.b0 ∧ f g.b1 = g'.b1 ∧ f g.b2 = g'.b2 ∧ f g.kd = g'.kd ∧ f g.l0 = g'.l0 ∧ f g.l1 = g'.l1 ∧ f g.l2 = g'.l2

theorem Cayley.Pack.gapCore_map {R S : Type} (addR subR mulR : R → R → R) (cR : ℤ → R) (xR : Fin 5 → R) (addS subS mulS : S → S → S) (cS : ℤ → S) (xS : Fin 5 → S) (f : R → S) (hadd : ∀ (a b : R), f (addR a b) = addS (f a) (f b)) (hsub : ∀ (a b : R), f (subR a b) = subS (f a) (f b)) (hmul : ∀ (a b : R), f (mulR a b) = mulS (f a) (f b)) (hc : ∀ (z : ℤ), f (cR z) = cS z) (hx : ∀ (i : Fin 5), f (xR i) = xS i) (chart face : ℕ) (U : R) (cc hh : ℕ → R) (sx sy sz w0 w1 : R) : have g := K.gapCore addR subR mulR cR xR chart face U cc hh sx sy sz w0 w1; have g' := K.gapCore addS subS mulS cS xS chart face (f U) (fun (i : ℕ) => f (cc i)) (fun (i : ℕ) => f (hh i)) (f sx) (f sy) (f sz) (f w0) (f w1); f g.a0 = g'.a0 ∧ f g.a1 = g'.a1 ∧ f g.a2 = g'.a2 ∧ f g.b0 = g'.b0 ∧ f g.b1 = g'.b1 ∧ f g.b2 = g'.b2 ∧ f g.kd = g'.kd ∧ f g.l0 = g'.l0 ∧ f g.l1 = g'.l1 ∧ f g.l2 = g'.l2

The real instance

noncomputable def Cayley.Pack.gapR (b : K.KBox) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) (t : Fin 5 → ℝ) : K.GData ℝ

The gap-leaf data at a real point t.

Equations

• Cayley.Pack.gapR b S w0 w1 t = Cayley.K.gapGen (fun (x1 x2 : ℝ) => x1 + x2) (fun (x1 x2 : ℝ) => x1 - x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) t b S w0 w1

def Cayley.Pack.svec (S : ℤ × ℤ × ℤ) : Fin 3 → ℝ

The integer vertex as a real vector.

Equations

• Cayley.Pack.svec S = ![↑S.1, ↑S.2.1, ↑S.2.2]

theorem Cayley.Pack.p2_cast (k : ℕ) : ↑(K.p2 k) = 2 ^ k

theorem Cayley.Pack.gapR_alpha (b : K.KBox) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) (t : Fin 5 → ℝ) (y : Fin 3 → ℝ) : have g := gapR b S w0 w1 t; g.a0 * y 0 + g.a1 * y 1 + g.a2 * y 2 = (2 ^ b.K) ^ 2 * lin (↑w0) (↑w1) ((NoR (kpt b t)).mulVec y)

theorem Cayley.Pack.gChart_real1 (chart : ℕ) (hj : chart < 5) (y0 y1 y2 : ℝ) : (K.gChart (fun (x1 x2 : ℝ) => x1 - x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) (fun (x1 x2 : ℝ) => x1 + x2) chart y0 y1 y2).1 = ∑ j : Fin 3, chartMR chart 0 j * ![y0, y1, y2] j

The real chart application.

theorem Cayley.Pack.gChart_real2 (chart : ℕ) (hj : chart < 5) (y0 y1 y2 : ℝ) : (K.gChart (fun (x1 x2 : ℝ) => x1 - x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) (fun (x1 x2 : ℝ) => x1 + x2) chart y0 y1 y2).2.1 = ∑ j : Fin 3, chartMR chart 1 j * ![y0, y1, y2] j

theorem Cayley.Pack.gChart_real3 (chart : ℕ) (hj : chart < 5) (y0 y1 y2 : ℝ) : (K.gChart (fun (x1 x2 : ℝ) => x1 - x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) (fun (x1 x2 : ℝ) => x1 + x2) chart y0 y1 y2).2.2 = ∑ j : Fin 3, chartMR chart 2 j * ![y0, y1, y2] j

noncomputable def Cayley.Pack.betaSc (b : K.KBox) : ℝ

The scale of β: U⁴ (blown up) or U².

Equations

• Cayley.Pack.betaSc b = if b.chart = 0 ∨ b.chart = 4 then (2 ^ b.K) ^ 4 else (2 ^ b.K) ^ 2

theorem Cayley.Pack.kptm2 (b : K.KBox) (t : Fin 5 → ℝ) : ↑(b.c.getD 2 0) + ↑(b.h.getD 2 0) * t 2 = 2 ^ b.K * kpt b t 2

theorem Cayley.Pack.kptm3 (b : K.KBox) (t : Fin 5 → ℝ) : ↑(b.c.getD 3 0) + ↑(b.h.getD 3 0) * t 3 = 2 ^ b.K * kpt b t 3

theorem Cayley.Pack.kptm4 (b : K.KBox) (t : Fin 5 → ℝ) : ↑(b.c.getD 4 0) + ↑(b.h.getD 4 0) * t 4 = 2 ^ b.K * kpt b t 4

theorem Cayley.Pack.gFace_real (face : ℕ) (U x2 x3 : ℝ) : (K.gFace face (if face % 2 = 0 then U else ↑0 - U) (U * x2) (U * x3)).1 = U * faceR face x2 x3 0 ∧ (K.gFace face (if face % 2 = 0 then U else ↑0 - U) (U * x2) (U * x3)).2.1 = U * faceR face x2 x3 1 ∧ (K.gFace face (if face % 2 = 0 then U else ↑0 - U) (U * x2) (U * x3)).2.2 = U * faceR face x2 x3 2

theorem Cayley.Pack.gapR_beta (b : K.KBox) (hj : b.chart < 5) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) (t : Fin 5 → ℝ) : have g := gapR b S w0 w1 t; have r := rOf (kblow b.chart) b.face (kpt b t); have v := (chartMR b.chart).mulVec ((cayleyNumeratorMatrix (r 0) (r 1) (r 2)).mulVec (svec S)); g.b0 = betaSc b * v 0 ∧ g.b1 = betaSc b * v 1 ∧ g.b2 = betaSc b * v 2 ∧ g.kd = kapJ b.chart * betaSc b * cayleyDenom (r 0) (r 1) (r 2)

theorem Cayley.Pack.gapR_L (b : K.KBox) (hj : b.chart < 5) (hbl : b.chart = 0 ∨ b.chart = 4) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) (t : Fin 5 → ℝ) : have g := gapR b S w0 w1 t; have c := faceR b.face (kpt b t 2) (kpt b t 3); have v := (chartMR b.chart).mulVec (crossR c (svec S) + kpt b t 4 • crossR c (crossR c (svec S))); g.l0 = (2 ^ b.K) ^ 3 * v 0 ∧ g.l1 = (2 ^ b.K) ^ 3 * v 1 ∧ g.l2 = (2 ^ b.K) ^ 3 * v 2

The three instances

def Cayley.Pack.gapPE (b : K.KBox) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) : K.GData PE

The gap-leaf polynomial expressions.

Equations

• Cayley.Pack.gapPE b S w0 w1 = Cayley.K.gapGen Cayley.Pack.PE.add Cayley.Pack.PE.sub Cayley.Pack.PE.mul Cayley.Pack.PE.c Cayley.Pack.PE.x b S w0 w1

def Cayley.K.GData.get {R : Type} (g : GData R) : Fin 10 → R

A field of the gap data.

Equations

• g.get 0 = g.a0
• g.get 1 = g.a1
• g.get 2 = g.a2
• g.get 3 = g.b0
• g.get 4 = g.b1
• g.get 5 = g.b2
• g.get 6 = g.kd
• g.get 7 = g.l0
• g.get 8 = g.l1
• g.get 9 = g.l2

theorem Cayley.Pack.gapGen_map' {R S : Type} (addR subR mulR : R → R → R) (cR : ℤ → R) (xR : Fin 5 → R) (addS subS mulS : S → S → S) (cS : ℤ → S) (xS : Fin 5 → S) (f : R → S) (hadd : ∀ (a b : R), f (addR a b) = addS (f a) (f b)) (hsub : ∀ (a b : R), f (subR a b) = subS (f a) (f b)) (hmul : ∀ (a b : R), f (mulR a b) = mulS (f a) (f b)) (hc : ∀ (z : ℤ), f (cR z) = cS z) (hx : ∀ (i : Fin 5), f (xR i) = xS i) (b : K.KBox) (s : ℤ × ℤ × ℤ) (w0 w1 : ℤ) (k : Fin 10) : f ((K.gapGen addR subR mulR cR xR b s w0 w1).get k) = (K.gapGen addS subS mulS cS xS b s w0 w1).get k

theorem Cayley.Pack.gapPE_int (b : K.KBox) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) (k : Fin 10) : PE.ev (fun (i : Fin 5) => K.pX ↑i) ((gapPE b S w0 w1).get k) = (K.pGapData b S w0 w1).get k

theorem Cayley.Pack.gapPE_real (b : K.KBox) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) (t : Fin 5 → ℝ) (k : Fin 10) : PE.ev t ((gapPE b S w0 w1).get k) = (gapR b S w0 w1 t).get k

def Cayley.K.gapNrm (b : KBox) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) : GData ℕ

Coefficient-norm bounds of the gap-leaf polynomials (the Nat instance of gapGen).

Equations

• Cayley.K.gapNrm b S w0 w1 = Cayley.K.gapGen Nat.add Nat.add Nat.mul Int.natAbs (fun (x : Fin 5) => 1) b S w0 w1

def Cayley.K.gapNrmOK (b : KBox) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) : Bool

Every polynomial the gap test decodes has coefficient norm below 2^390 (room for the Bernstein transform; outer vertices have coordinates below 2^161).

Equations

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

theorem Cayley.Pack.gapPE_nrm (b : K.KBox) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) (k : Fin 10) : ((gapPE b S w0 w1).get k).nrm = (K.gapNrm b S w0 w1).get k

Degrees

def Cayley.Pack.degB (k : Fin 10) (i : Fin 5) : ℕ

Degree bounds of the gap data fields.

Equations

• Cayley.Pack.degB k i = if ↑k < 3 then if ↑i < 2 then 2 else 0 else if ↑k < 7 then if ↑i < 2 then 0 else 2 else if ↑i < 2 then 0 else if ↑i = 4 then 1 else 2

def Cayley.Pack.gapDeg (b : K.KBox) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) : K.GData (Fin 5 → ℕ)

The degree instance of gapGen.

Equations

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

theorem Cayley.Pack.gapPE_deg (b : K.KBox) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) (k : Fin 10) : (fun (i : Fin 5) => PE.deg i ((gapPE b S w0 w1).get k)) = (gapDeg b S w0 w1).get k

theorem Cayley.Pack.gapGen_map2 {R S : Type} (addR subR mulR : R → R → R) (cR : ℤ → R) (xR : Fin 5 → R) (addS subS mulS : S → S → S) (cS : ℤ → S) (xS : Fin 5 → S) (f : R → S) (hadd : ∀ (a b : R), f (addR a b) = addS (f a) (f b)) (hsub : ∀ (a b : R), f (subR a b) = subS (f a) (f b)) (hmul : ∀ (a b : R), f (mulR a b) = mulS (f a) (f b)) (hc : ∀ (z z' : ℤ), f (cR z) = cS z') (hx : ∀ (i : Fin 5), f (xR i) = xS i) (b b' : K.KBox) (hch : b.chart = b'.chart) (hfa : b.face = b'.face) (s s' : ℤ × ℤ × ℤ) (w0 w1 w0' w1' : ℤ) (k : Fin 10) : f ((K.gapGen addR subR mulR cR xR b s w0 w1).get k) = (K.gapGen addS subS mulS cS xS b' s' w0' w1').get k

Two runs on boxes with the same chart and face, when every constant maps to the same value.

theorem Cayley.Pack.gapDeg_data (b : K.KBox) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) (k : Fin 10) : (gapDeg b S w0 w1).get k = (gapDeg { chart := b.chart, face := b.face, K := 0, c := [], h := [] } (0, 0, 0) 0 0).get k

theorem Cayley.Pack.gapDeg_closed (chart : ℕ) : chart < 5 → ∀ face < 6, ∀ (k : Fin 10) (i : Fin 5), (gapDeg { chart := chart, face := face, K := 0, c := [], h := [] } (0, 0, 0) 0 0).get k i ≤ degB k i

theorem Cayley.Pack.gapDeg_le (b : K.KBox) (hj : b.chart < 5) (hf : b.face < 6) (S : ℤ × ℤ × ℤ) (w0 w1 : ℤ) (k : Fin 10) (i : Fin 5) : (gapDeg b S w0 w1).get k i ≤ degB k i

Monotonicity of the norm instance

@[reducible, inline]

abbrev Cayley.Pack.MP : Type

Pairs (a, b) with a ≤ b. Running gapCore on them runs the norm instance on two inputs at once, and keeps every first component below the second.

Equations

• Cayley.Pack.MP = { p : ℕ × ℕ // p.1 ≤ p.2 }

def Cayley.Pack.mpAdd (a b : MP) : MP

Equations

• Cayley.Pack.mpAdd a b = ⟨((↑a).1 + (↑b).1, (↑a).2 + (↑b).2), ⋯⟩

def Cayley.Pack.mpMul (a b : MP) : MP

Equations

• Cayley.Pack.mpMul a b = ⟨((↑a).1 * (↑b).1, (↑a).2 * (↑b).2), ⋯⟩

def Cayley.Pack.mpC (z : ℤ) : MP

Equations

• Cayley.Pack.mpC z = ⟨(z.natAbs, z.natAbs), ⋯⟩

def Cayley.Pack.mpX : Fin 5 → MP

Equations

• Cayley.Pack.mpX x✝ = ⟨(1, 1), Cayley.Pack.mpX._proof_1⟩

theorem Cayley.Pack.gapCore_get {R : Type} (g : K.GData R) (f : R → ℕ) (g' : K.GData ℕ) (h : f g.a0 = g'.a0 ∧ f g.a1 = g'.a1 ∧ f g.a2 = g'.a2 ∧ f g.b0 = g'.b0 ∧ f g.b1 = g'.b1 ∧ f g.b2 = g'.b2 ∧ f g.kd = g'.kd ∧ f g.l0 = g'.l0 ∧ f g.l1 = g'.l1 ∧ f g.l2 = g'.l2) (k : Fin 10) : f (g.get k) = g'.get k

theorem Cayley.Pack.gapNrm_mono (b b' : K.KBox) (hch : b.chart = b'.chart) (hfa : b.face = b'.face) (hK : (K.p2 b.K).natAbs ≤ (K.p2 b'.K).natAbs) (hc : ∀ (i : ℕ), (b.c.getD i 0).natAbs ≤ (b'.c.getD i 0).natAbs) (hh : ∀ (i : ℕ), (b.h.getD i 0).natAbs ≤ (b'.h.getD i 0).natAbs) (S S' : ℤ × ℤ × ℤ) (h1 : S.1.natAbs ≤ S'.1.natAbs) (h2 : S.2.1.natAbs ≤ S'.2.1.natAbs) (h3 : S.2.2.natAbs ≤ S'.2.2.natAbs) (w0 w1 w0' w1' : ℤ) (hw0 : w0.natAbs ≤ w0'.natAbs) (hw1 : w1.natAbs ≤ w1'.natAbs) (k : Fin 10) : (K.gapNrm b S w0 w1).get k ≤ (K.gapNrm b' S' w0' w1').get k

Norm monotonicity. The coefficient-norm bounds grow with the magnitudes of the inputs.