Degenerate residues in the three-axes problem

Finite identities behind the degenerate-residue analysis of s = u⁻² + v⁻² + w⁻² in the free field of F₃ (u = 1 + x, v = 1 + y, w = 1 + z). All matrices are 2×2 over a commutative ring unless stated.

Main results

• sandwich: M A M = tr(A M) • M − det M • adj A; hence, for det M = 0, annihilator_left: (M A M B − M B M A) M = 0 and annihilator_right.
• det_add_adj: det(A + B) = det A + tr(adj A · B) + det B.
• adj_sq_leading, inv_target: the leading coefficient of s along Y = N + εΔ with N square-zero: adj(N + εΔ)² = ε • (τ • 1 − σ • N) + ε² • (adj Δ)².
• realization_det: det [[A+B, A],[A, A+C]] · (det A det B det C) = det(det B det C • adj A + det A det C • adj B + det A det B • adj C).
• D2, D3, comm2_det, comm3: iterated conjugation differences at x = N − 1.
• F2_witness: an explicit rational witness with nonzero determinant.

sandwich, det_add_adj, comm2_det and comm3 are restatements of the 2 × 2 identities of Formalizations.LinearAlgebra.Matrix.FinTwo (cm is ⁅·, ·⁆, disc is Matrix.discr); blk, det4, Nsq and the witness matrices are in Formalizations.RingTheory.FreeField.ThreeAxes.Basic.

theorem ThreeAxes.DegenerateResidue.sandwich {R : Type u_1} [CommRing R] (M A : M2 R) : M * A * M = (A * M).trace • M - Matrix.det M • Matrix.adjugate A

(S) sandwich identity for 2×2 matrices (Matrix.mul_mul_eq_trace_smul_sub_det_smul_adjugate_fin_two).

theorem ThreeAxes.DegenerateResidue.annihilator_left {R : Type u_1} [CommRing R] (M A B : M2 R) (h : Matrix.det M = 0) : (M * A * M * B - M * B * M * A) * M = 0

theorem ThreeAxes.DegenerateResidue.annihilator_right {R : Type u_1} [CommRing R] (M A B : M2 R) (h : Matrix.det M = 0) : M * (A * M * B * M - B * M * A * M) = 0

theorem ThreeAxes.DegenerateResidue.det_add_adj {R : Type u_1} [CommRing R] (A B : M2 R) : Matrix.det (A + B) = Matrix.det A + (Matrix.adjugate A * B).trace + Matrix.det B

(C) determinant of a sum, 2×2 (Matrix.det_add_fin_two).

theorem ThreeAxes.DegenerateResidue.adj_sq_leading {R : Type u_1} [CommRing R] (a b e : R) (D : M2 R) : Matrix.adjugate (Nsq a b + e • D) ^ 2 = e • ((Nsq a b * D).trace • 1 - Matrix.trace D • Nsq a b) + e ^ 2 • Matrix.adjugate D ^ 2

(L) square of the adjugate along the arc: the ε⁰ term vanishes and the ε¹ term is τI − σN.

theorem ThreeAxes.DegenerateResidue.inv_target {R : Type u_1} [CommRing R] (a b t s : R) : (t • 1 + s • Nsq a b) * (t • 1 - s • Nsq a b) = t ^ 2 • 1

theorem ThreeAxes.DegenerateResidue.realization_det {R : Type u_1} [CommRing R] (A B C : M2 R) : (blk A B C).det * (Matrix.det A * Matrix.det B * Matrix.det C) = ((Matrix.det B * Matrix.det C) • Matrix.adjugate A + (Matrix.det A * Matrix.det C) • Matrix.adjugate B + (Matrix.det A * Matrix.det B) • Matrix.adjugate C).det

(H) realization identity, inverse-free form.

def ThreeAxes.DegenerateResidue.Dx {R : Type u_1} [CommRing R] (a b : R) (T : M2 R) : M2 R

(D) conjugation differences at x = N − 1 with N = Nsq a b.

Equations

• ThreeAxes.DegenerateResidue.Dx a b T = T - (ThreeAxes.Nsq a b - 1) * T * -(1 + ThreeAxes.Nsq a b)

theorem ThreeAxes.DegenerateResidue.D2 {R : Type u_1} [CommRing R] (a b : R) (T : M2 R) : Dx a b (Dx a b T) = -2 • (Nsq a b * T * Nsq a b)

theorem ThreeAxes.DegenerateResidue.D3 {R : Type u_1} [CommRing R] (a b : R) (T : M2 R) : Dx a b (Dx a b (Dx a b T)) = 0

def ThreeAxes.DegenerateResidue.cm {R : Type u_1} [CommRing R] (X T : M2 R) : M2 R

Equations

• ThreeAxes.DegenerateResidue.cm X T = X * T - T * X

def ThreeAxes.DegenerateResidue.disc {R : Type u_1} [CommRing R] (X : M2 R) : R

Equations

• ThreeAxes.DegenerateResidue.disc X = Matrix.trace X ^ 2 - 4 * Matrix.det X

theorem ThreeAxes.DegenerateResidue.cm_eq_lie {R : Type u_1} [CommRing R] (X T : M2 R) : cm X T = ⁅X, T⁆

cm is the ring commutator ⁅X, T⁆.

theorem ThreeAxes.DegenerateResidue.disc_eq_discr {R : Type u_1} [CommRing R] (X : M2 R) : disc X = Matrix.discr X

disc is Mathlib's Matrix.discr (Matrix.discr_fin_two).

theorem ThreeAxes.DegenerateResidue.comm2_det {R : Type u_1} [CommRing R] (X T : M2 R) : Matrix.det (cm X (cm X T)) = -disc X * Matrix.det (cm X T)

Matrix.det_lie_lie_eq_neg_discr_mul_det_lie_fin_two, written with cm and disc.

theorem ThreeAxes.DegenerateResidue.comm3 {R : Type u_1} [CommRing R] (X T : M2 R) : cm X (cm X (cm X T)) = disc X • cm X T

Matrix.lie_lie_lie_eq_discr_smul_lie_fin_two, written with cm and disc.

def ThreeAxes.DegenerateResidue.hW : Matrix (Fin 2) (Fin 2) ℚ

h = y u⁻¹ y⁻¹ + v⁻¹ + w⁻¹ at W; Dw = conjugation difference by x = Wx − 1.

Equations

• ThreeAxes.DegenerateResidue.hW = (ThreeAxes.Wy - 1) * ThreeAxes.Wxi * ThreeAxes.Xyi + ThreeAxes.Wyi + ThreeAxes.Wzi

def ThreeAxes.DegenerateResidue.Dw (T : Matrix (Fin 2) (Fin 2) ℚ) : Matrix (Fin 2) (Fin 2) ℚ

Equations

• ThreeAxes.DegenerateResidue.Dw T = T - (ThreeAxes.Wx - 1) * T * ThreeAxes.Xxi

theorem ThreeAxes.DegenerateResidue.F2_witness : ((Wx - 1) * Xxi = 1 ∧ (Wy - 1) * Xyi = 1 ∧ Wx * Wxi = 1 ∧ Wy * Wyi = 1 ∧ Wz * Wzi = 1) ∧ Dw (Dw hW) = !![-203 / 10, 704 / 5; -13 / 10, 203 / 10] ∧ !![-203 / 10, 704 / 5; -13 / 10, 203 / 10].det = -4581 / 20