hex

35.14. HexMinPoly: matrix minimal polynomials🔗

35.14.1. Introduction🔗

HexMinPoly computes minimal polynomials of dense square matrices over fields. The computational layer is Mathlib-free and builds on HexMatrix, HexRowReduce, and HexPoly. HexMinPolyMathlib connects the result to Mathlib's minpoly and characteristic-polynomial theory.

For a matrix A, the minimal polynomial is the monic polynomial of least degree that annihilates every vector. For one vector v, its order polynomial is the monic polynomial of least degree that annihilates just v. The matrix minimal polynomial is the least common multiple of the orders of the standard basis vectors.

35.14.2. Evaluation and Krylov sequences🔗

🔗def
Hex.Matrix.evalVec.{u} {F : Type u} [Lean.Grind.Field F] [DecidableEq F]
  {n : ℕ} (p : Hex.DensePoly F) (A : Hex.Matrix F n n)
  (v : Vector F n) : Vector F n
Hex.Matrix.evalVec.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n : ℕ} (p : Hex.DensePoly F)
  (A : Hex.Matrix F n n)
  (v : Vector F n) : Vector F n

Horner evaluation of p at A, applied to v. This uses only matrix-vector products.

evalVec uses Horner evaluation and never constructs a matrix power or a polynomial-valued matrix. The Krylov operations expose the successive vectors used to discover a first dependency.

🔗def
Hex.Matrix.krylovVec.{u} {F : Type u} [Lean.Grind.Field F] {n : ℕ}
  (A : Hex.Matrix F n n) (v : Vector F n) : ℕ → Vector F n
Hex.Matrix.krylovVec.{u} {F : Type u}
  [Lean.Grind.Field F] {n : ℕ}
  (A : Hex.Matrix F n n)
  (v : Vector F n) : ℕ → Vector F n

A^j v, computed using j matrix-vector products.

🔗def
Hex.Matrix.krylovRows.{u} {F : Type u} [Lean.Grind.Field F] {n : ℕ}
  (A : Hex.Matrix F n n) (v : Vector F n) (r : ℕ) :
  Vector (Vector F n) r
Hex.Matrix.krylovRows.{u} {F : Type u}
  [Lean.Grind.Field F] {n : ℕ}
  (A : Hex.Matrix F n n) (v : Vector F n)
  (r : ℕ) : Vector (Vector F n) r

The first r Krylov vectors, sharing every matrix-vector product.

🔗def
Hex.Matrix.krylovMat.{u} {F : Type u} [Lean.Grind.Field F] {n : ℕ}
  (A : Hex.Matrix F n n) (v : Vector F n) (r : ℕ) : Hex.Matrix F r n
Hex.Matrix.krylovMat.{u} {F : Type u}
  [Lean.Grind.Field F] {n : ℕ}
  (A : Hex.Matrix F n n) (v : Vector F n)
  (r : ℕ) : Hex.Matrix F r n

The r × n matrix whose rows are v, A v, …, A^(r-1) v.

krylovRows A v r computes each new row from the preceding one, sharing all matrix-vector products. krylovMat is the matrix view of the same sequence.

open Hex open scoped Hex namespace HexMinPolyChapterExample def A : Matrix Rat 2 2 := #m[0, 1; 0, 0] def v : Vector Rat 2 := #v[0, 1] #guard A.krylovVec v 1 == #v[1, 0] #guard A.krylovVec v 2 == #v[0, 0] end HexMinPolyChapterExample
🔗def
Hex.Matrix.krylovDeg.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) (v : Vector F n) : ℕ
Hex.Matrix.krylovDeg.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n)
  (v : Vector F n) : ℕ

The rank of the full Krylov matrix, hence the order-polynomial degree.

🔗def
Hex.Matrix.krylovCoeffs?.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) (v : Vector F n) :
  Option (Vector F (A.krylovDeg v))
Hex.Matrix.krylovCoeffs?.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n)
  (v : Vector F n) :
  Option (Vector F (A.krylovDeg v))

Coefficients of the first Krylov dependency, in ascending order. The prefix and its next vector are sliced from one shared Krylov array.

🔗def
Hex.Matrix.dependencyPoly.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {d : ℕ} (c : Vector F d) : Hex.DensePoly F
Hex.Matrix.dependencyPoly.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {d : ℕ} (c : Vector F d) :
  Hex.DensePoly F

Assemble x^d - Σ j, c_j x^j from ascending dependency coefficients.

If the dependency coefficients are c₀, ..., c_(d-1), the resulting polynomial is x^d - Σ c_j x^j. The first d rows are independent; their right inverse later becomes the minimality witness in a certificate.

35.14.3. Vector orders and the matrix polynomial🔗

🔗def
Hex.Matrix.vecMinPoly.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) (v : Vector F n) :
  Hex.DensePoly F
Hex.Matrix.vecMinPoly.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n)
  (v : Vector F n) : Hex.DensePoly F

The order polynomial of v. The none branch is unreachable by the Krylov prefix invariant and is kept only to make the function total.

🔗theorem
Hex.Matrix.vecMinPoly_monic.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) (v : Vector F n) :
  (A.vecMinPoly v).Monic
Hex.Matrix.vecMinPoly_monic.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ}
  (A : Hex.Matrix F n n)
  (v : Vector F n) :
  (A.vecMinPoly v).Monic

The vector order polynomial is monic.

🔗theorem
Hex.Matrix.evalVec_vecMinPoly.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) (v : Vector F n) :
  Hex.Matrix.evalVec (A.vecMinPoly v) A v = 0
Hex.Matrix.evalVec_vecMinPoly.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ}
  (A : Hex.Matrix F n n)
  (v : Vector F n) :
  Hex.Matrix.evalVec (A.vecMinPoly v) A
      v =
    0

The vector order polynomial annihilates its vector.

🔗theorem
Hex.Matrix.vecMinPoly_dvd.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) (v : Vector F n)
  (p : Hex.DensePoly F) :
  Hex.Matrix.evalVec p A v = 0 → A.vecMinPoly v ∣ p
Hex.Matrix.vecMinPoly_dvd.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n)
  (v : Vector F n) (p : Hex.DensePoly F) :
  Hex.Matrix.evalVec p A v = 0 →
    A.vecMinPoly v ∣ p

The vector order polynomial divides every annihilator of the vector.

These three laws say that the computed vector order is monic, annihilates the given vector, and divides every other annihilator of that vector.

🔗def
Hex.Matrix.minPoly.{u} {F : Type u} [Lean.Grind.Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n) : Hex.DensePoly F
Hex.Matrix.minPoly.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n) :
  Hex.DensePoly F

The monic generator of the polynomials annihilating A, computed as the least common multiple of the order polynomials of every standard basis vector.

🔗theorem
Hex.Matrix.minPoly_monic.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) : A.minPoly.Monic
Hex.Matrix.minPoly_monic.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n) :
  A.minPoly.Monic

The computed matrix minimal polynomial is monic, including for the empty matrix where it is 1.

🔗theorem
Hex.Matrix.evalVec_minPoly.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) (v : Vector F n) :
  Hex.Matrix.evalVec A.minPoly A v = 0
Hex.Matrix.evalVec_minPoly.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ}
  (A : Hex.Matrix F n n)
  (v : Vector F n) :
  Hex.Matrix.evalVec A.minPoly A v = 0

The minimal polynomial annihilates every vector.

🔗theorem
Hex.Matrix.minPoly_dvd_iff.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) (p : Hex.DensePoly F) :
  A.minPoly ∣ p ↔ ∀ (v : Vector F n), Hex.Matrix.evalVec p A v = 0
Hex.Matrix.minPoly_dvd_iff.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ}
  (A : Hex.Matrix F n n)
  (p : Hex.DensePoly F) :
  A.minPoly ∣ p ↔
    ∀ (v : Vector F n),
      Hex.Matrix.evalVec p A v = 0

A polynomial is a multiple of the minimal polynomial exactly when it annihilates every vector.

The last equivalence is the complete user-facing contract: divisibility by the minimal polynomial is exactly the property of annihilating all vectors.

open Hex open scoped Hex namespace HexMinPolyResultExample def A : Matrix Rat 2 2 := #m[0, 1; 0, 0] def v : Vector Rat 2 := #v[0, 1] #guard A.vecMinPoly v == #p[0, 0, 1] #guard A.minPoly == #p[0, 0, 1] example : A.evalVec A.minPoly v = 0 := Hex.Matrix.evalVec_minPoly A v end HexMinPolyResultExample

Closed forms cover the empty matrix, positive-dimensional zero and identity matrices, one-by-one matrices, zero vectors, and nonzero eigenvectors.

Hex.Matrix.minPoly_empty states that the empty matrix has minimal polynomial 1.

🔗theorem
Hex.Matrix.minPoly_zero.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] (n : ℕ) (hn : 0 < n) :
  Hex.Matrix.minPoly 0 = Hex.DensePoly.ofCoeffs #[0, 1]
Hex.Matrix.minPoly_zero.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  (n : ℕ) (hn : 0 < n) :
  Hex.Matrix.minPoly 0 =
    Hex.DensePoly.ofCoeffs #[0, 1]

The zero matrix of positive dimension has minimal polynomial x.

🔗theorem
Hex.Matrix.minPoly_identity.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] (n : ℕ) (hn : 0 < n) :
  (Hex.Matrix.identity n).minPoly = Hex.DensePoly.ofCoeffs #[-1, 1]
Hex.Matrix.minPoly_identity.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] (n : ℕ) (hn : 0 < n) :
  (Hex.Matrix.identity n).minPoly =
    Hex.DensePoly.ofCoeffs #[-1, 1]

A positive-dimensional identity matrix has minimal polynomial x - 1.

🔗theorem
Hex.Matrix.vecMinPoly_eigen.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) (v : Vector F n)
  (a : F) (hv : v ≠ 0) (hA : A * v = a • v) :
  A.vecMinPoly v = Hex.DensePoly.ofCoeffs #[-a, 1]
Hex.Matrix.vecMinPoly_eigen.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ}
  (A : Hex.Matrix F n n) (v : Vector F n)
  (a : F) (hv : v ≠ 0)
  (hA : A * v = a • v) :
  A.vecMinPoly v =
    Hex.DensePoly.ofCoeffs #[-a, 1]

A nonzero eigenvector has the expected linear order polynomial.

35.14.4. Checkable certificates🔗

Hex.Matrix.OrderCert records an order polynomial, its degree, and a right inverse of the independent Krylov prefix. Hex.Matrix.LcmStep records common-factor, cofactor, and Bézout identities for one LCM step. Hex.Matrix.MinPolyCert contains one order witness and one LCM witness for every standard basis vector.

🔗def
Hex.Matrix.checkRightInverse.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n d : ℕ} (K : Hex.Matrix F d n)
  (inv : Hex.Matrix F n d) : Bool
Hex.Matrix.checkRightInverse.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n d : ℕ}
  (K : Hex.Matrix F d n)
  (inv : Hex.Matrix F n d) : Bool

Check K * inv = I one column at a time, using only matrix-vector products.

🔗def
Hex.Matrix.MinPolyCert.check.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n)
  (c : Hex.Matrix.MinPolyCert F n) : Bool
Hex.Matrix.MinPolyCert.check.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ}
  (A : Hex.Matrix F n n)
  (c : Hex.Matrix.MinPolyCert F n) : Bool

The kernel-reducible minimal-polynomial certificate checker. It performs no row reduction, pivot search, or field division.

🔗theorem
Hex.Matrix.MinPolyCert.check_sound.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n)
  (c : Hex.Matrix.MinPolyCert F n)
  (h : Hex.Matrix.MinPolyCert.check A c = true) :
  c.poly.Monic ∧
    (∀ (v : Vector F n), Hex.Matrix.evalVec c.poly A v = 0) ∧
      ∀ (p : Hex.DensePoly F),
        (∀ (v : Vector F n), Hex.Matrix.evalVec p A v = 0) → c.poly ∣ p
Hex.Matrix.MinPolyCert.check_sound.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ}
  (A : Hex.Matrix F n n)
  (c : Hex.Matrix.MinPolyCert F n)
  (h :
    Hex.Matrix.MinPolyCert.check A c =
      true) :
  c.poly.Monic ∧
    (∀ (v : Vector F n),
        Hex.Matrix.evalVec c.poly A v =
          0) ∧
      ∀ (p : Hex.DensePoly F),
        (∀ (v : Vector F n),
            Hex.Matrix.evalVec p A v =
              0) →
          c.poly ∣ p

A successful certificate proves monicity, annihilation on every vector, and divisibility into every annihilator.

The checker uses matrix-vector products and polynomial ring identities. A successful certificate proves monicity, annihilation on every vector, and divisibility into every other annihilator.

🔗def
Hex.Matrix.minPolyCert.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) :
  Hex.Matrix.MinPolyCert F n
Hex.Matrix.minPolyCert.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n) :
  Hex.Matrix.MinPolyCert F n

Produce a complete basis-wide minimal-polynomial certificate.

🔗theorem
Hex.Matrix.minPolyCert_check.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) :
  Hex.Matrix.MinPolyCert.check A A.minPolyCert = true
Hex.Matrix.minPolyCert_check.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n : ℕ}
  (A : Hex.Matrix F n n) :
  Hex.Matrix.MinPolyCert.check A
      A.minPolyCert =
    true

Certificates produced from row reduction and extended gcd pass the kernel-reducible checker.

open Hex open scoped Hex namespace HexMinPolyCertificateExample def A : Matrix Rat 2 2 := #m[0, 1; 0, 0] example : (A.minPolyCert).check A = true := Hex.Matrix.minPolyCert_check A end HexMinPolyCertificateExample

35.14.5. Complexity and validation🔗

One dense matrix-vector product costs O(n²) field operations. Building a Krylov sequence and reducing its matrix each cost O(n³). Repeating this for the standard basis gives the deterministic matrix algorithm a conservative O(n⁴) field-operation bound.

Required conformance tests exercise the individual Krylov and dependency operations, valid certificates, and deliberately corrupted right-inverse, order, Bézout, and monicity witnesses. Integer and rational fixture results are checked coefficient-for-coefficient against FLINT. Benchmarks separate evaluation, Krylov construction, vector orders, matrix minimal polynomials, certificate production, and certificate checking, with FLINT and PARI as informational comparators.

35.14.6. The Mathlib correspondence🔗

🔗theorem
HexMinPolyMathlib.equiv_minPoly.{u} {F : Type u} [Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) :
  HexPolyMathlib.equiv A.minPoly =
    minpoly F (HexMatrixMathlib.matrixEquiv A)
HexMinPolyMathlib.equiv_minPoly.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n) :
  HexPolyMathlib.equiv A.minPoly =
    minpoly F
      (HexMatrixMathlib.matrixEquiv A)

The executable minimal polynomial is Mathlib's minimal polynomial of the corresponding matrix.

🔗theorem
HexMinPolyMathlib.vectorEquiv_evalVec.{u} {F : Type u} [Field F]
  [DecidableEq F] {n : ℕ} (p : Hex.DensePoly F) (A : Hex.Matrix F n n)
  (v : Vector F n) :
  HexMatrixMathlib.vectorEquiv (Hex.Matrix.evalVec p A v) =
    ((Polynomial.aeval (HexMatrixMathlib.matrixEquiv A))
          (HexPolyMathlib.equiv p)).mulVec
      (HexMatrixMathlib.vectorEquiv v)
HexMinPolyMathlib.vectorEquiv_evalVec.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n : ℕ} (p : Hex.DensePoly F)
  (A : Hex.Matrix F n n)
  (v : Vector F n) :
  HexMatrixMathlib.vectorEquiv
      (Hex.Matrix.evalVec p A v) =
    ((Polynomial.aeval
            (HexMatrixMathlib.matrixEquiv
              A))
          (HexPolyMathlib.equiv p)).mulVec
      (HexMatrixMathlib.vectorEquiv v)

Horner evaluation at a matrix applied to a vector is Mathlib's aeval followed by mulVec.

🔗theorem
HexMinPolyMathlib.vecMinPoly_dvd_iff.{u} {F : Type u} [Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) (v : Vector F n)
  (p : Polynomial F) :
  HexPolyMathlib.equiv (A.vecMinPoly v) ∣ p ↔
    ((Polynomial.aeval (HexMatrixMathlib.matrixEquiv A)) p).mulVec
        (HexMatrixMathlib.vectorEquiv v) =
      0
HexMinPolyMathlib.vecMinPoly_dvd_iff.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n)
  (v : Vector F n) (p : Polynomial F) :
  HexPolyMathlib.equiv (A.vecMinPoly v) ∣
      p ↔
    ((Polynomial.aeval
              (HexMatrixMathlib.matrixEquiv
                A))
            p).mulVec
        (HexMatrixMathlib.vectorEquiv v) =
      0

The order polynomial generates the annihilator of its vector, transported to Mathlib polynomials.

The bridge also identifies executable LCM with Mathlib's normalized LCM and derives the characteristic-polynomial degree bound.

🔗theorem
HexMinPolyMathlib.equiv_lcm.{u} {F : Type u} [Field F] [DecidableEq F]
  (p q : Hex.DensePoly F) :
  HexPolyMathlib.equiv (p.lcm q) =
    lcm (HexPolyMathlib.equiv p) (HexPolyMathlib.equiv q)
HexMinPolyMathlib.equiv_lcm.{u}
  {F : Type u} [Field F] [DecidableEq F]
  (p q : Hex.DensePoly F) :
  HexPolyMathlib.equiv (p.lcm q) =
    lcm (HexPolyMathlib.equiv p)
      (HexPolyMathlib.equiv q)

The executable monic LCM agrees exactly with Mathlib's normalized LCM.

🔗theorem
HexMinPolyMathlib.minPoly_dvd_charPoly.{u} {F : Type u} [Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) :
  A.minPoly ∣ A.charPoly
HexMinPolyMathlib.minPoly_dvd_charPoly.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n) :
  A.minPoly ∣ A.charPoly

The executable minimal polynomial divides the executable characteristic polynomial.

🔗theorem
HexMinPolyMathlib.degree?_minPoly_le.{u} {F : Type u} [Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) :
  A.minPoly.natDegree ≤ n
HexMinPolyMathlib.degree?_minPoly_le.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n) :
  A.minPoly.natDegree ≤ n

The degree of the executable minimal polynomial is at most the matrix dimension.

Finally, the executable minimal polynomial has the expected invariance laws.

🔗theorem
HexMinPolyMathlib.minPoly_transpose.{u} {F : Type u} [Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) :
  A.transpose.minPoly = A.minPoly
HexMinPolyMathlib.minPoly_transpose.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n) :
  A.transpose.minPoly = A.minPoly

Transposition preserves the executable minimal polynomial.

🔗theorem
HexMinPolyMathlib.minPoly_conj.{u} {F : Type u} [Field F]
  [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n)
  (P : (Hex.Matrix F n n)ˣ) :
  (ConjAct.toConjAct P • A).minPoly = A.minPoly
HexMinPolyMathlib.minPoly_conj.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n : ℕ} (A : Hex.Matrix F n n)
  (P : (Hex.Matrix F n n)ˣ) :
  (ConjAct.toConjAct P • A).minPoly =
    A.minPoly

Conjugation by an invertible matrix preserves the executable minimal polynomial. This is the similarity-invariance law.