Residues along square-zero directions #

Certificates for the residue / trace-direction mechanism in the three-axes problem. Conventions: Y_j = 1 + x_j evaluated; H0(Y) = [[Yx²+Yy², Yx²],[Yx², Yx²+Yz²]].

Main results #

polar: 2×2 Cayley–Hamilton polarization AB + BA = tr A • B + tr B • A + (tr(AB) − tr A tr B) • 1; polar_traceless.
det_add_smul: det(A + εB) = det A + ε (tr A tr B − tr(AB)) + ε² det B; adjugate_add_smul.
residue_sqzero: tr N = 0, det N = 0 ⇒ det(N + εΔ) = ε (ε det Δ − tr(NΔ)) and adj(N + εΔ) = −N + ε • adj Δ (the residue does not see tr Δ); inv_sub_one_sqzero.
h4_general: the determinant of H0 at A_j = τ_j • 1 + σ_j • N_j in closed form.
arc_det: an exact example along a square-zero arc.
witness: an integer witness on the zero set of det H0, with Y_j ∈ SL₂(ℤ).

polar and det_add_smul are restatements of the 2 × 2 identities of Formalizations.LinearAlgebra.Matrix.FinTwo; blk, det4, Nsq and the witness matrices are in Formalizations.RingTheory.FreeField.ThreeAxes.Basic.

source

theorem ThreeAxes.TraceResidue.polar {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) :

A * B + B * A = A.trace • B + B.trace • A + ((A * B).trace - A.trace * B.trace) • 1

(P) 2×2 Cayley–Hamilton polarization (Matrix.mul_add_mul_eq_trace_smul_add_trace_smul_fin_two).

source

theorem ThreeAxes.TraceResidue.polar_traceless {R : Type u_1} [CommRing R] (N D : Matrix (Fin 2) (Fin 2) R) (hN : N.trace = 0) :

N * D + D * N = D.trace • N + (N * D).trace • 1

(P) traceless case.

source

theorem ThreeAxes.TraceResidue.det_add_smul {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) (e : R) :

(A + e • B).det = A.det + e * (A.trace * B.trace - (A * B).trace) + e ^ 2 * B.det

(D) determinant of a 2×2 pencil (Matrix.det_add_smul_fin_two).

source

theorem ThreeAxes.TraceResidue.adjugate_add_smul {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) (e : R) :

(A + e • B).adjugate = A.adjugate + e • B.adjugate

(D) the 2×2 adjugate is linear.

source

theorem ThreeAxes.TraceResidue.residue_sqzero {R : Type u_1} [CommRing R] (N D : Matrix (Fin 2) (Fin 2) R) (e : R) (hT : N.trace = 0) (hD : N.det = 0) :

(N + e • D).det = e * (e * D.det - (N * D).trace) ∧ (N + e • D).adjugate = -N + e • D.adjugate

(R) residue along a square-zero point: the leading term sees tr(NΔ), not tr Δ.

source

theorem ThreeAxes.TraceResidue.inv_sub_one_sqzero {R : Type u_1} [CommRing R] (N : Matrix (Fin 2) (Fin 2) R) (h : N * N = 0) :

(N - 1) * -(1 + N) = 1

(R) inverse of X = N − 1 when N² = 0.

source

theorem ThreeAxes.TraceResidue.h4_general {R : Type u_1} [CommRing R] (a0 b0 a1 b1 a2 b2 tx ty tz sx sy sz : R) :

(blk (tx • 1 + sx • Nsq a0 b0) (ty • 1 + sy • Nsq a1 b1) (tz • 1 + sz • Nsq a2 b2)).det = (tx * ty + tx * tz + ty * tz) ^ 2 + (a0 * b1 - a1 * b0) ^ 2 * tz ^ 2 * sx * sy + (a0 * b2 - a2 * b0) ^ 2 * ty ^ 2 * sx * sz + (a1 * b2 - a2 * b1) ^ 2 * tx ^ 2 * sy * sz

(H) first coefficient of H0 along a trace-direction arc, general square-zero triple.

source