The atom certificate for the 9 × 9 pencil of the three-axes problem

Integer data behind the proof that the 3 × 3 target matrix F of the three-axes problem is an atom (Lemma 7.8(a)). The linear pencil Q = Q₀ + u Q_u + v Q_v + w Q_w is a 9 × 9 linearisation of F; at the point u = v = w = 2 it is invertible with det Q(2,2,2) = 256, and the normalised coefficients K_i = 16 Q(2,2,2)⁻¹ Q_i are integer matrices. The algebra they generate is all of M₉, witnessed by a rank-one element r ℓ (a polynomial without constant term in K_v) together with two bases of words acting on r and on ℓ.

Determinants of the explicit 9 × 9 matrices are not computed by Laplace expansion: each one is certified by an integer factorisation L * M.submatrix σ σ = U with L lower triangular, U upper triangular and σ a permutation (det_eq_of_certificate), checked by decide.

Main results

• det_eq_of_certificate: if L * M.submatrix σ σ = U with L lower and U upper triangular over an integral domain, and ∏ U i i = (∏ L i i) * d with ∏ L i i ≠ 0, then det M = d.
• Q2_mul_K: Q(2,2,2) * K i = 16 • Q i for i = u, v, w; det_Q2: det Q(2,2,2) = 256.
• Kv_identity: K_v² (K_v² − 12 K_v + 48) = 2048 • vecMulVec r ℓ.
• det_wordsR: det [K_ω r]_{ω ∈ R} = 5 * 2 ^ 56; det_wordsO: det [ℓ K_ω]_{ω ∈ O} = 2 ^ 49, with K_ω = K_{ω₁} K_{ω₂} ⋯ (left to right).

Determinants from triangular certificates

theorem ThreeAxes.AtomCertificate.prod_diag_mul_det_of_mul_eq {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {R : Type u_2} [CommRing R] {L M U : Matrix n n R} (h : L * M = U) (hL : L.IsLowerTriangular) (hU : U.IsUpperTriangular) : (∏ i : n, L i i) * M.det = ∏ i : n, U i i

theorem ThreeAxes.AtomCertificate.det_eq_of_certificate {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {R : Type u_2} [CommRing R] [IsDomain R] {L M U : Matrix n n R} (σ : Equiv.Perm n) (d : R) (h : L * M.submatrix ⇑σ ⇑σ = U) (hL : L.IsLowerTriangular) (hU : U.IsUpperTriangular) (hd : ∏ i : n, U i i = (∏ i : n, L i i) * d) (h0 : ∏ i : n, L i i ≠ 0) : M.det = d

The pencil

def ThreeAxes.AtomCertificate.Q0 : Matrix (Fin 9) (Fin 9) ℤ

The constant coefficient Q₀ of the pencil.

Equations

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

def ThreeAxes.AtomCertificate.Qu : Matrix (Fin 9) (Fin 9) ℤ

The coefficient Q_u of u.

Equations

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

def ThreeAxes.AtomCertificate.Qv : Matrix (Fin 9) (Fin 9) ℤ

The coefficient Q_v of v.

Equations

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

def ThreeAxes.AtomCertificate.Qw : Matrix (Fin 9) (Fin 9) ℤ

The coefficient Q_w of w.

Equations

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

inductive ThreeAxes.AtomCertificate.Letter : Type

The three variables of the pencil.

• u : Letter
• v : Letter
• w : Letter

@[instance_reducible]

instance ThreeAxes.AtomCertificate.instDecidableEqLetter : DecidableEq Letter

Equations

• ThreeAxes.AtomCertificate.instDecidableEqLetter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ThreeAxes.AtomCertificate.Q : Letter → Matrix (Fin 9) (Fin 9) ℤ

The coefficient of a variable.

Equations

• ThreeAxes.AtomCertificate.Q ThreeAxes.AtomCertificate.Letter.u = ThreeAxes.AtomCertificate.Qu
• ThreeAxes.AtomCertificate.Q ThreeAxes.AtomCertificate.Letter.v = ThreeAxes.AtomCertificate.Qv
• ThreeAxes.AtomCertificate.Q ThreeAxes.AtomCertificate.Letter.w = ThreeAxes.AtomCertificate.Qw

def ThreeAxes.AtomCertificate.Q2 : Matrix (Fin 9) (Fin 9) ℤ

The pencil at u = v = w = 2.

Equations

• ThreeAxes.AtomCertificate.Q2 = ThreeAxes.AtomCertificate.Q0 + 2 • (ThreeAxes.AtomCertificate.Qu + ThreeAxes.AtomCertificate.Qv + ThreeAxes.AtomCertificate.Qw)

The normalised coefficients K_i = 16 Q(2,2,2)⁻¹ Q_i

def ThreeAxes.AtomCertificate.Ku : Matrix (Fin 9) (Fin 9) ℤ

K_u = 16 Q(2,2,2)⁻¹ Q_u.

Equations

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

def ThreeAxes.AtomCertificate.Kv : Matrix (Fin 9) (Fin 9) ℤ

K_v = 16 Q(2,2,2)⁻¹ Q_v.

Equations

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

def ThreeAxes.AtomCertificate.Kw : Matrix (Fin 9) (Fin 9) ℤ

K_w = 16 Q(2,2,2)⁻¹ Q_w.

Equations

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

def ThreeAxes.AtomCertificate.K : Letter → Matrix (Fin 9) (Fin 9) ℤ

The normalised coefficient of a variable.

Equations

• ThreeAxes.AtomCertificate.K ThreeAxes.AtomCertificate.Letter.u = ThreeAxes.AtomCertificate.Ku
• ThreeAxes.AtomCertificate.K ThreeAxes.AtomCertificate.Letter.v = ThreeAxes.AtomCertificate.Kv
• ThreeAxes.AtomCertificate.K ThreeAxes.AtomCertificate.Letter.w = ThreeAxes.AtomCertificate.Kw

theorem ThreeAxes.AtomCertificate.Q2_mul_K (i : Letter) : Q2 * K i = 16 • Q i

K_i = 16 Q(2,2,2)⁻¹ Q_i, stated without inverses.

det Q(2,2,2) = 256

def ThreeAxes.AtomCertificate.σQ2 : Equiv.Perm (Fin 9)

The permutation of the certificate for Q(2,2,2).

Equations

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

def ThreeAxes.AtomCertificate.LQ2 : Matrix (Fin 9) (Fin 9) ℤ

Lower triangular factor of the certificate for Q(2,2,2).

Equations

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

def ThreeAxes.AtomCertificate.UQ2 : Matrix (Fin 9) (Fin 9) ℤ

Upper triangular factor of the certificate for Q(2,2,2).

Equations

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

theorem ThreeAxes.AtomCertificate.det_Q2 : Q2.det = 256

The rank-one element: identity (7.1)

def ThreeAxes.AtomCertificate.r : Fin 9 → ℤ

The column vector r.

Equations

• ThreeAxes.AtomCertificate.r = ![0, 0, -1, 0, 0, 0, -2, 4, 1]

def ThreeAxes.AtomCertificate.ℓ : Fin 9 → ℤ

The row vector ℓ.

Equations

• ThreeAxes.AtomCertificate.ℓ = ![2, 0, -2, 0, 2, 0, 0, 3, 0]

theorem ThreeAxes.AtomCertificate.Kv_identity : Kv * Kv * (Kv * Kv - 12 • Kv + 48 • 1) = 2048 • Matrix.vecMulVec r ℓ

K_v² (K_v² − 12 K_v + 48) = 2048 r ℓ: the rank-one matrix r ℓ is a polynomial without constant term in K_v.

The two bases of words: identities (7.2)

def ThreeAxes.AtomCertificate.word (ω : List Letter) : Matrix (Fin 9) (Fin 9) ℤ

K_ω = K_{ω₁} K_{ω₂} ⋯ (left to right).

Equations

• ThreeAxes.AtomCertificate.word ω = (List.map ThreeAxes.AtomCertificate.K ω).prod

def ThreeAxes.AtomCertificate.wordsR : Fin 9 → List Letter

The words R = (∅, u, uu, vu, wu, uuu, vuu, uvu, vvu).

Equations

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

def ThreeAxes.AtomCertificate.wordsO : Fin 9 → List Letter

The words O = (∅, u, w, uu, uv, wu, ww, uuu, uuv).

Equations

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

def ThreeAxes.AtomCertificate.matR : Matrix (Fin 9) (Fin 9) ℤ

The matrix with columns K_ω r, ω ∈ R.

Equations

• ThreeAxes.AtomCertificate.matR = Matrix.of fun (i j : Fin 9) => (ThreeAxes.AtomCertificate.word (ThreeAxes.AtomCertificate.wordsR j)).mulVec ThreeAxes.AtomCertificate.r i

def ThreeAxes.AtomCertificate.matO : Matrix (Fin 9) (Fin 9) ℤ

The matrix with rows ℓ K_ω, ω ∈ O.

Equations

• ThreeAxes.AtomCertificate.matO = Matrix.of fun (i j : Fin 9) => Matrix.vecMul ThreeAxes.AtomCertificate.ℓ (ThreeAxes.AtomCertificate.word (ThreeAxes.AtomCertificate.wordsO i)) j

def ThreeAxes.AtomCertificate.σR : Equiv.Perm (Fin 9)

The permutation of the certificate for matR.

Equations

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

def ThreeAxes.AtomCertificate.LR : Matrix (Fin 9) (Fin 9) ℤ

Lower triangular factor of the certificate for matR.

Equations

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

def ThreeAxes.AtomCertificate.UR : Matrix (Fin 9) (Fin 9) ℤ

Upper triangular factor of the certificate for matR.

Equations

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

def ThreeAxes.AtomCertificate.σO : Equiv.Perm (Fin 9)

The permutation of the certificate for matO.

Equations

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

def ThreeAxes.AtomCertificate.LO : Matrix (Fin 9) (Fin 9) ℤ

Lower triangular factor of the certificate for matO.

Equations

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

def ThreeAxes.AtomCertificate.UO : Matrix (Fin 9) (Fin 9) ℤ

Upper triangular factor of the certificate for matO.

Equations

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

theorem ThreeAxes.AtomCertificate.det_matR : matR.det = 5 * 2 ^ 56

det [K_ω r]_{ω ∈ R} = 5 · 2⁵⁶.

theorem ThreeAxes.AtomCertificate.det_matO : matO.det = 2 ^ 49

det [ℓ K_ω]_{ω ∈ O} = 2⁴⁹.