hex

35.7. HexCharPoly: characteristic polynomials🔗

35.7.1. Introduction🔗

Released as hex-char-poly, with the Mathlib correspondence in hex-char-poly-mathlib.

HexCharPoly computes the characteristic polynomial det (xI - A) of a dense square matrix with the division-free Samuelson--Berkowitz algorithm. The computational library is Mathlib-free and works over every commutative ring with decidable equality. Its only Hex dependencies are HexMatrix and HexPoly.

The algorithm does no division or pivoting. It therefore works without assuming that nonzero elements are invertible, and has no failure-producing branch. Its O(n^4) ring-operation cost makes it a portable certified implementation rather than a replacement for a specialized characteristic-polynomial routine on very large matrices.

35.7.2. Representation and public API🔗

Hex.Matrix.berkowitz returns n + 1 coefficients in descending degree order. Entry zero is the coefficient of x^n; entry n is the constant coefficient.

🔗def
Hex.Matrix.berkowitz.{u} {R : Type u} [Lean.Grind.CommRing R] {n : ℕ}
  (A : Hex.Matrix R n n) : Vector R (n + 1)
Hex.Matrix.berkowitz.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ}
  (A : Hex.Matrix R n n) :
  Vector R (n + 1)

The coefficients of the characteristic polynomial of A in descending degree order: entry zero is the coefficient of x^n, and entry n is the constant coefficient.

The user-facing Hex.Matrix.charPoly reverses that vector and stores it as a normalized Hex.DensePoly, whose coefficients are in ascending order.

🔗def
Hex.Matrix.charPoly.{u} {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] {n : ℕ} (A : Hex.Matrix R n n) : Hex.DensePoly R
Hex.Matrix.charPoly.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R]
  {n : ℕ} (A : Hex.Matrix R n n) :
  Hex.DensePoly R

The characteristic polynomial det (x * I - A).

The result is monic, including over the zero ring. Over a nontrivial ring it has stored size n + 1 and degree n.

🔗theorem
Hex.Matrix.charPoly_monic.{u} {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] {n : ℕ} (A : Hex.Matrix R n n) : A.charPoly.Monic
Hex.Matrix.charPoly_monic.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R]
  {n : ℕ} (A : Hex.Matrix R n n) :
  A.charPoly.Monic

The characteristic polynomial is monic, including over the zero ring.

🔗theorem
Hex.Matrix.size_charPoly.{u} {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] {n : ℕ} (h1 : 1 ≠ 0) (A : Hex.Matrix R n n) :
  A.charPoly.size = n + 1
Hex.Matrix.size_charPoly.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R]
  {n : ℕ} (h1 : 1 ≠ 0)
  (A : Hex.Matrix R n n) :
  A.charPoly.size = n + 1

Over a nontrivial coefficient ring, charPoly stores exactly n+1 coefficients.

🔗theorem
Hex.Matrix.degree?_charPoly.{u} {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] {n : ℕ} (h1 : 1 ≠ 0) (A : Hex.Matrix R n n) :
  A.charPoly.degree? = some n
Hex.Matrix.degree?_charPoly.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] {n : ℕ} (h1 : 1 ≠ 0)
  (A : Hex.Matrix R n n) :
  A.charPoly.degree? = some n

Over a nontrivial coefficient ring, charPoly has degree n.

The library also provides the matrix trace and Horner evaluation of a dense polynomial at a square matrix.

🔗def
Hex.Matrix.trace.{u} {R : Type u} [Lean.Grind.CommRing R] {n : ℕ}
  (A : Hex.Matrix R n n) : R
Hex.Matrix.trace.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ}
  (A : Hex.Matrix R n n) : R

The sum of the diagonal entries of a square matrix.

🔗def
Hex.Matrix.evalMatrix.{u} {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] {n : ℕ} (p : Hex.DensePoly R) (A : Hex.Matrix R n n) :
  Hex.Matrix R n n
Hex.Matrix.evalMatrix.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R]
  {n : ℕ} (p : Hex.DensePoly R)
  (A : Hex.Matrix R n n) :
  Hex.Matrix R n n

Horner evaluation of a dense polynomial at a square matrix. A scalar coefficient acts by scaling the identity matrix.

35.7.3. The Berkowitz recursion🔗

The recursion grows trailing principal blocks. At one step, write the new block as [[a, R], [C, B]]. The first column of the lower-triangular Toeplitz step is

1, -a, -(R C), -(R B C), ..., -(R B^(k-1) C).

Successive vectors B^j C are computed iteratively. Multiplying the Toeplitz matrix by the coefficient vector for B produces the coefficient vector for the new bordered block.

🔗def
Hex.Matrix.berkowitzColumn.{u} {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ} (A : Hex.Matrix R n n) (k : ℕ) (hk : k + 1 ≤ n) :
  Vector R (k + 2)
Hex.Matrix.berkowitzColumn.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ} (A : Hex.Matrix R n n) (k : ℕ)
  (hk : k + 1 ≤ n) : Vector R (k + 2)

The Toeplitz first column for the Berkowitz step at trailing block size k + 1: 1, -a, and -(row dot B^j col) for 0 <= j < k.

🔗def
Hex.Matrix.berkowitzStep.{u} {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ} (A : Hex.Matrix R n n) (k : ℕ) (hk : k + 1 ≤ n)
  (v : Vector R (k + 1)) : Vector R (k + 2)
Hex.Matrix.berkowitzStep.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ}
  (A : Hex.Matrix R n n) (k : ℕ)
  (hk : k + 1 ≤ n)
  (v : Vector R (k + 1)) :
  Vector R (k + 2)

One Berkowitz step, growing the descending coefficient vector from length k + 1 to length k + 2.

The leading coefficient stays one at every intermediate step, and the coefficient of x^(n-1) in the final polynomial is the negated trace.

🔗theorem
Hex.Matrix.berkowitzAux_zero.{u} {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ} (A : Hex.Matrix R n n) (k : ℕ) (hk : k ≤ n) :
  (A.berkowitzAux k hk)[0] = 1
Hex.Matrix.berkowitzAux_zero.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ} (A : Hex.Matrix R n n) (k : ℕ)
  (hk : k ≤ n) :
  (A.berkowitzAux k hk)[0] = 1

Every intermediate descending coefficient vector has leading entry one.

🔗theorem
Hex.Matrix.coeff_charPoly_pred.{u} {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] {n : ℕ} (A : Hex.Matrix R n n) (hn : 0 < n) :
  A.charPoly.coeff (n - 1) = -A.trace
Hex.Matrix.coeff_charPoly_pred.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] {n : ℕ}
  (A : Hex.Matrix R n n) (hn : 0 < n) :
  A.charPoly.coeff (n - 1) = -A.trace

The coefficient of x^(n-1) is the negative trace.

35.7.4. Computing certified concrete results🔗

For a closed Hex.Matrix Int n n, char_poly A is a term containing the computed polynomial and a proof that it equals Hex.Matrix.charPoly applied to A. Bare char_poly closes a direct equality in either orientation.

open Hex open scoped Hex namespace HexCharPolyChapterExample private def A : Hex.Matrix Int 2 2 := #m[1, 2; 3, 4] private def result := char_poly A example : result.poly = #p[-2, -5, 1] := rfl example : Hex.Matrix.charPoly A = #p[-2, -5, 1] := ⊢ A.charPoly = DensePoly.ofCoeffs #[-2, -5, 1] All goals completed! 🐙 example : #p[-2, -5, 1] = Hex.Matrix.charPoly A := ⊢ DensePoly.ofCoeffs #[-2, -5, 1] = A.charPoly All goals completed! 🐙 example : True := ⊢ True poly:DensePoly ℤ := (Matrix.CharPolyResult.ofCheck A #v[1, -5, -2] (DensePoly.ofCoeffs #[-2, -5, 1]) ⋯ ⋯).polycharPoly_eq:A.charPoly = poly⊢ True poly:DensePoly ℤ := (Matrix.CharPolyResult.ofCheck A #v[1, -5, -2] (DensePoly.ofCoeffs #[-2, -5, 1]) ⋯ ⋯).polycharPoly_eq:A.charPoly = polyx✝:A.charPoly = poly⊢ True All goals completed! 🐙 end HexCharPolyChapterExample

The explicit tactic form introduces a transparent poly local definition and a charPoly_eq hypothesis. This is useful when the computed polynomial is an intermediate fact rather than the goal.

Importing HexCharPolyMathlib adds the same interface for a closed Matrix (Fin n) (Fin n) Int. Direct goals use ordinary Mathlib polynomial notation.

open Matrix Polynomial namespace HexCharPolyMathlibChapterExample private def A : Matrix (Fin 2) (Fin 2) Int := !![1, 2; 3, 4] example : A.charpoly = X ^ 2 - 5 * X - 2 := ⊢ A.charpoly = X ^ 2 - 5 * X - 2 All goals completed! 🐙 example : X ^ 2 - 5 * X - 2 = A.charpoly := ⊢ X ^ 2 - 5 * X - 2 = A.charpoly All goals completed! 🐙 example : True := ⊢ True poly:ℤ[X] := (HexCharPolyMathlib.CharPolyResult.ofCheck A { data := #v[1, 2, 3, 4] } #v[1, -5, -2] (DensePoly.ofCoeffs #[-2, -5, 1]) ⋯ ⋯ ⋯).polycharPoly_eq:A.charpoly = poly⊢ True poly:ℤ[X] := (HexCharPolyMathlib.CharPolyResult.ofCheck A { data := #v[1, 2, 3, 4] } #v[1, -5, -2] (DensePoly.ofCoeffs #[-2, -5, 1]) ⋯ ⋯ ⋯).polycharPoly_eq:A.charpoly = polyx✝:A.charpoly = poly⊢ True All goals completed! 🐙 end HexCharPolyMathlibChapterExample

The term and tactic currently support integer matrices only. The matrix, its dimension, and a polynomial appearing in a direct equality must be closed and definitionally transparent. Mathlib polynomial goals may use X, C, integer numerals, addition, subtraction, multiplication, negation, and natural-literal powers; transparent named definitions built from those forms are unfolded.

Compiled evaluation discovers the coefficients and intermediate values. The emitted term separately certifies the scalar dot products, matrix-vector products, Berkowitz steps, and final coefficients. For a Mathlib matrix it additionally certifies every materialized entry and then uses the correspondence theorem below. The compiled evaluator is not trusted, and Mathlib's noncomputable Matrix.charpoly is not evaluated.

35.7.5. The Mathlib correspondence🔗

HexCharPolyMathlib identifies the executable polynomial with Mathlib's Matrix.charpoly after transporting both the matrix and polynomial through their equivalences.

🔗theorem
HexCharPolyMathlib.equiv_charPoly.{u} {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ} (A : Hex.Matrix R n n) :
  HexPolyMathlib.equiv A.charPoly =
    (HexMatrixMathlib.matrixEquiv A).charpoly
HexCharPolyMathlib.equiv_charPoly.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ}
  (A : Hex.Matrix R n n) :
  HexPolyMathlib.equiv A.charPoly =
    (HexMatrixMathlib.matrixEquiv
        A).charpoly

The executable characteristic polynomial agrees with Mathlib's characteristic polynomial under the dense-polynomial equivalence.

This correspondence supplies the determinant interpretation of evaluation and Cayley--Hamilton without adding Mathlib or a determinant dependency to the computational package.

🔗theorem
HexCharPolyMathlib.eval_charPoly.{u} {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ} (A : Hex.Matrix R n n) (t : R) :
  A.charPoly.eval t = (t • Hex.Matrix.identity n - A).det
HexCharPolyMathlib.eval_charPoly.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ}
  (A : Hex.Matrix R n n) (t : R) :
  A.charPoly.eval t =
    (t • Hex.Matrix.identity n - A).det

Evaluating the executable characteristic polynomial is taking the determinant of the scalar shift.

🔗theorem
HexCharPolyMathlib.evalMatrix_charPoly.{u} {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ} (A : Hex.Matrix R n n) :
  Hex.Matrix.evalMatrix A.charPoly A = 0
HexCharPolyMathlib.evalMatrix_charPoly.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ}
  (A : Hex.Matrix R n n) :
  Hex.Matrix.evalMatrix A.charPoly A = 0

Cayley--Hamilton for the executable characteristic polynomial and matrix objects.

The constant coefficient is the signed determinant, and transposition and conjugation by an explicitly supplied inverse preserve the polynomial.

🔗theorem
HexCharPolyMathlib.coeff_zero_charPoly.{u} {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ} (A : Hex.Matrix R n n) :
  A.charPoly.coeff 0 = (-1) ^ n * A.det
HexCharPolyMathlib.coeff_zero_charPoly.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ}
  (A : Hex.Matrix R n n) :
  A.charPoly.coeff 0 = (-1) ^ n * A.det

The constant characteristic-polynomial coefficient is the signed determinant.

🔗theorem
HexCharPolyMathlib.charPoly_transpose.{u} {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ} (A : Hex.Matrix R n n) :
  A.transpose.charPoly = A.charPoly
HexCharPolyMathlib.charPoly_transpose.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ}
  (A : Hex.Matrix R n n) :
  A.transpose.charPoly = A.charPoly

Transposition preserves the executable characteristic polynomial.

🔗theorem
HexCharPolyMathlib.charPoly_conj.{u} {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ} (A U V : Hex.Matrix R n n)
  (h : U * V = Hex.Matrix.identity n) :
  (U * A * V).charPoly = A.charPoly
HexCharPolyMathlib.charPoly_conj.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ}
  (A U V : Hex.Matrix R n n)
  (h : U * V = Hex.Matrix.identity n) :
  (U * A * V).charPoly = A.charPoly

Conjugation by a pair of mutually inverse square matrices preserves the executable characteristic polynomial.

35.7.6. Cross-references🔗

  • HexMatrix supplies the dense matrix type and arithmetic used by the recursion.

  • HexPoly supplies the normalized dense polynomial representation.

  • HexDeterminant supplies the Mathlib-free Leibniz determinant used to state the evaluation law in the correspondence package.

  • HexBareiss is the fraction-free executable route for integer determinants; it computes a determinant rather than the complete characteristic polynomial.