The domain-leaf polynomials

numGen, chartGen and orbGen are generic in the arithmetic; maps that commute with the operations commute with them.

def Cayley.K.NM.map {R S : Type} (f : R → S) (N : NM R) : NM S

f applied to every entry.

Equations

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

theorem Cayley.Pack.numGen_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) : K.NM.map f (K.numGen addR subR mulR cR xR b) = K.numGen addS subS mulS cS xS b

theorem Cayley.Pack.trGen_map {R S : Type} (addR mulR : R → R → R) (cR : ℤ → R) (addS mulS : S → S → S) (cS : ℤ → S) (f : R → S) (hadd : ∀ (a b : R), f (addR a b) = addS (f a) (f b)) (hmul : ∀ (a b : R), f (mulR a b) = mulS (f a) (f b)) (hc : ∀ (z : ℤ), f (cR z) = cS z) (X : K.I9) (N : K.NM R) : f (K.trGen addR mulR cR X N) = K.trGen addS mulS cS X (K.NM.map f N)

theorem Cayley.Pack.chartGen_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) (k : ℕ) : f (K.chartGen addR subR mulR cR xR b k) = K.chartGen addS subS mulS cS xS b k

theorem Cayley.Pack.m3_map {R S : Type} (addR mulR : R → R → R) (cR : ℤ → R) (addS mulS : S → S → S) (cS : ℤ → S) (f : R → S) (hadd : ∀ (a b : R), f (addR a b) = addS (f a) (f b)) (hmul : ∀ (a b : R), f (mulR a b) = mulS (f a) (f b)) (hc : ∀ (z : ℤ), f (cR z) = cS z) (M : K.I9) (N : K.NM R) : K.NM.map f (K.m3 addR mulR cR M N) = K.m3 addS mulS cS M (K.NM.map f N)

theorem Cayley.Pack.m3t_map {R S : Type} (f : R → S) (N : K.NM R) : K.NM.map f (K.m3t N) = K.m3t (K.NM.map f N)

theorem Cayley.Pack.frob_map {R S : Type} (addR mulR : R → R → R) (addS mulS : S → S → S) (f : R → S) (hadd : ∀ (a b : R), f (addR a b) = addS (f a) (f b)) (hmul : ∀ (a b : R), f (mulR a b) = mulS (f a) (f b)) (H W : K.NM R) : f (K.frob addR mulR H W) = K.frob addS mulS (K.NM.map f H) (K.NM.map f W)

theorem Cayley.Pack.hGen_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) (u v U : R) : K.NM.map f (K.hGen addR subR mulR cR u v U) = K.hGen addS subS mulS cS (f u) (f v) (f U)

theorem Cayley.Pack.orbGen_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) (e g a : ℕ) : f (K.orbGen addR subR mulR cR xR b e g a).1 = (K.orbGen addS subS mulS cS xS b e g a).1 ∧ f (K.orbGen addR subR mulR cR xR b e g a).2 = (K.orbGen addS subS mulS cS xS b e g a).2

Degrees

def Cayley.Pack.dAdd (a c : Fin 5 → ℕ) : Fin 5 → ℕ

The degree algebra.

Equations

• Cayley.Pack.dAdd a c i = max (a i) (c i)

def Cayley.Pack.dMul (a c : Fin 5 → ℕ) : Fin 5 → ℕ

Equations

• Cayley.Pack.dMul a c i = a i + c i

@[reducible, inline]

abbrev Cayley.Pack.dC : ℤ → Fin 5 → ℕ

Equations

• Cayley.Pack.dC x✝¹ x✝ = 0

def Cayley.Pack.dX (j : Fin 5) : Fin 5 → ℕ

Equations

• Cayley.Pack.dX j i = if j = i then 1 else 0

theorem Cayley.Pack.numGen_deg (b : K.KBox) : K.numGen dAdd dAdd dMul dC dX b = K.numGen dAdd dAdd dMul dC dX { chart := b.chart, face := b.face, K := 0, c := [], h := [] }

The degree instance only sees the chart and the face.

theorem Cayley.Pack.chartGen_deg (b : K.KBox) (k : ℕ) : K.chartGen dAdd dAdd dMul dC dX b k = K.chartGen dAdd dAdd dMul dC dX { chart := b.chart, face := b.face, K := 0, c := [], h := [] } k

theorem Cayley.Pack.orbGen_deg (b : K.KBox) (e g a : ℕ) : K.orbGen dAdd dAdd dMul dC dX b e g a = K.orbGen dAdd dAdd dMul dC dX { chart := b.chart, face := b.face, K := 0, c := [], h := [] } e g a

theorem Cayley.Pack.trGen_dC (X X' : K.I9) (N : K.NM (Fin 5 → ℕ)) : K.trGen dAdd dMul dC X N = K.trGen dAdd dMul dC X' N

theorem Cayley.Pack.m3_dC (X X' : K.I9) (N : K.NM (Fin 5 → ℕ)) : K.m3 dAdd dMul dC X N = K.m3 dAdd dMul dC X' N

theorem Cayley.Pack.orbGen_deg_g (b : K.KBox) (e g a : ℕ) : K.orbGen dAdd dAdd dMul dC dX b e g a = K.orbGen dAdd dAdd dMul dC dX b e 0 a

def Cayley.Pack.dBound (e : ℕ) (i : Fin 5) : ℕ

Degree bounds: t₀, t₁ absent (chart, orbit e = 0) or of degree ≤ 4 (orbit e = 1).

Equations

• Cayley.Pack.dBound e i = if ↑i < 2 then if e = 0 then 0 else 4 else 2

theorem Cayley.Pack.chart_deg_closed (chart : ℕ) : chart < 5 → ∀ face < 6, ∀ k < 5, ∀ (i : Fin 5), K.chartGen dAdd dAdd dMul dC dX { chart := chart, face := face, K := 0, c := [], h := [] } k i ≤ dBound 0 i

theorem Cayley.Pack.orb_deg_closed (chart : ℕ) : chart < 5 → ∀ face < 6, ∀ e < 2, ∀ (i : Fin 5), (K.orbGen dAdd dAdd dMul dC dX { chart := chart, face := face, K := 0, c := [], h := [] } e 0 0).1 i ≤ dBound e i ∧ (K.orbGen dAdd dAdd dMul dC dX { chart := chart, face := face, K := 0, c := [], h := [] } e 0 0).2 i ≤ dBound e i ∧ (K.orbGen dAdd dAdd dMul dC dX { chart := chart, face := face, K := 0, c := [], h := [] } e 0 4).1 i ≤ dBound e i ∧ (K.orbGen dAdd dAdd dMul dC dX { chart := chart, face := face, K := 0, c := [], h := [] } e 0 4).2 i ≤ dBound e i

The real instance

noncomputable def Cayley.Pack.numR (b : K.KBox) (t : Fin 5 → ℝ) : K.NM ℝ

The numerator at a real point.

Equations

• Cayley.Pack.numR b t = Cayley.K.numGen (fun (x1 x2 : ℝ) => x1 + x2) (fun (x1 x2 : ℝ) => x1 - x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) t b

def Cayley.Pack.nmat {R : Type} (N : K.NM R) : Matrix (Fin 3) (Fin 3) R

The matrix of an NM.

Equations

• Cayley.Pack.nmat N = !![N.n00, N.n01, N.n02; N.n10, N.n11, N.n12; N.n20, N.n21, N.n22]

theorem Cayley.Pack.numSc_real (b : K.KBox) : ↑(K.numSc b) = betaSc b

theorem Cayley.Pack.numR_eq (b : K.KBox) (t : Fin 5 → ℝ) : have r := rOf (kblow b.chart) b.face (kpt b t); nmat (numR b t) = betaSc b • cayleyNumeratorMatrix (r 0) (r 1) (r 2) ∧ (numR b t).d = betaSc b * cayleyDenom (r 0) (r 1) (r 2)

noncomputable def Cayley.Pack.imat (X : K.I9) : Matrix (Fin 3) (Fin 3) ℝ

The real matrix of an integer matrix.

Equations

• Cayley.Pack.imat (m00, m01, m02, m10, m11, m12, m20, m21, m22) = !![↑m00, ↑m01, ↑m02; ↑m10, ↑m11, ↑m12; ↑m20, ↑m21, ↑m22]

theorem Cayley.Pack.imat_chartMI (j : ℕ) : imat (K.chartMI j) = chartMR j

theorem Cayley.Pack.trR (X : K.I9) (N : K.NM ℝ) : K.trGen (fun (x1 x2 : ℝ) => x1 + x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) X N = ((imat X).transpose * nmat N).trace

theorem Cayley.Pack.imat_mtm (A B : K.I9) : imat (K.mtm A B) = (imat A).transpose * imat B

theorem Cayley.Pack.chartR_eq (b : K.KBox) (hj : b.chart < 5) (k : ℕ) (hk : k < 5) (t : Fin 5 → ℝ) : have r := rOf (kblow b.chart) b.face (kpt b t); K.chartGen (fun (x1 x2 : ℝ) => x1 + x2) (fun (x1 x2 : ℝ) => x1 - x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) t b k = kapJ b.chart ^ 2 * kapJ k * (betaSc b * cayleyDenom (r 0) (r 1) (r 2)) * (((chartB k).transpose * Qm b.chart r).trace - ((chartB b.chart).transpose * Qm b.chart r).trace)

The chart-test polynomial at a real point.

The orbit polynomials

theorem Cayley.Pack.imat_mmI (A B : K.I9) : imat (K.mmI A B) = imat A * imat B

noncomputable def Cayley.Pack.gHat (g : ℕ) : Matrix (Fin 3) (Fin 3) ℝ

The tabulated symmetry ĝ.

Equations

• Cayley.Pack.gHat g = Cayley.groupTab[g]!.toR

theorem Cayley.Pack.cosTab_getD (g : ℕ) (hg : g < 15) : cosTab.getD g 0 = cosTab[g]!

theorem Cayley.Pack.sinTab_getD (g : ℕ) (hg : g < 15) : sinTab.getD g 0 = sinTab[g]!

theorem Cayley.Pack.tab_e80 (g : ℕ) : g < 15 → (cosTab.getD g 0).e = 80 ∧ (sinTab.getD g 0).e = 80

theorem Cayley.Pack.imat_orbC (g a : ℕ) (hg : g < 15) : imat (K.orbC g a) = chartMR a * 2 ^ 80 • (gHat g).transpose

theorem Cayley.Pack.kapJ_zero : kapJ 0 = 1

theorem Cayley.Pack.chartB_zero_eq : chartB 0 = 1

theorem Cayley.Pack.orbR0 (b : K.KBox) (hj : b.chart < 5) (g : ℕ) (hg : g < 15) (a : ℕ) (ha : a = 0 ∨ a = 4) (t : Fin 5 → ℝ) : have r := rOf (kblow b.chart) b.face (kpt b t); have Q := Qm b.chart r; have K := kapJ 4 * kapJ b.chart * 2 ^ 80 * (betaSc b * cayleyDenom (r 0) (r 1) (r 2)); have F := ((chartB a).transpose * Q * gHat g).trace - if a = 4 then 1 / 8 else 0; (Cayley.K.orbGen (fun (x1 x2 : ℝ) => x1 + x2) (fun (x1 x2 : ℝ) => x1 - x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) t b 0 g a).1 = K * (F - Q.trace) ∧ (Cayley.K.orbGen (fun (x1 x2 : ℝ) => x1 + x2) (fun (x1 x2 : ℝ) => x1 - x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) t b 0 g a).2 = K * (F - ((tauR.transpose * Q).trace - 1 / 8))

The orbit polynomials for e = 0 at a real point.

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

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

theorem Cayley.Pack.nmat_m3 (M : K.I9) (N : K.NM ℝ) : nmat (K.m3 (fun (x1 x2 : ℝ) => x1 + x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) M N) = imat M * nmat N

theorem Cayley.Pack.nmat_m3t {R : Type} (N : K.NM R) : nmat (K.m3t N) = (nmat N).transpose

theorem Cayley.Pack.frob_real (H W : K.NM ℝ) : K.frob (fun (x1 x2 : ℝ) => x1 + x2) (fun (x1 x2 : ℝ) => x1 * x2) H W = ((nmat H).transpose * nmat W).trace

theorem Cayley.Pack.hGen_real (x : Fin 5 → ℝ) (U : ℝ) : nmat (K.hGen (fun (x1 x2 : ℝ) => x1 + x2) (fun (x1 x2 : ℝ) => x1 - x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) (U * x 0) (U * x 1) U) = (U ^ 2 • NoR x).transpose * ZR * U ^ 2 • NoR x

theorem Cayley.Pack.orbR1 (b : K.KBox) (hj : b.chart < 5) (g : ℕ) (hg : g < 15) (a : ℕ) (ha : a = 0 ∨ a = 4) (t : Fin 5 → ℝ) : have r := rOf (kblow b.chart) b.face (kpt b t); have Q := Qm b.chart r; have Do := cayleyDenom (kpt b t 1) (-kpt b t 0) 0; have K := kapJ 4 * kapJ b.chart * 2 ^ 80 * (betaSc b * cayleyDenom (r 0) (r 1) (r 2)) * (2 ^ b.K) ^ 4 * Do ^ 2; have F := ((chartB a).transpose * (Hmat (kpt b t 0) (kpt b t 1) * Q) * gHat g).trace - if a = 4 then 1 / 8 else 0; (Cayley.K.orbGen (fun (x1 x2 : ℝ) => x1 + x2) (fun (x1 x2 : ℝ) => x1 - x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) t b 1 g a).1 = K * (F - Q.trace) ∧ (Cayley.K.orbGen (fun (x1 x2 : ℝ) => x1 + x2) (fun (x1 x2 : ℝ) => x1 - x2) (fun (x1 x2 : ℝ) => x1 * x2) (fun (z : ℤ) => ↑z) t b 1 g a).2 = K * (F - ((tauR.transpose * Q).trace - 1 / 8))

The orbit polynomials for e = 1 at a real point.