39.1. HexPosDef: exact positive-definiteness certificates🔗

HexPosDef computes exact certificates for integer and Gaussian-integer matrices. HexPosDefTheory interprets accepted certificates as Mathlib positive definiteness or its negation and supplies the pos_def tactic. The executable library is Mathlib-free.

39.1.1. Proving positivity🔗

The tactic accepts closed square matrices over integers, rationals, reals with rational entries, and complex numbers with rational components. It recognizes literals, closed matrix functions, and bounded unfolding of definitions, including the Cartan matrices directly.

example : (CartanMatrix.E 8).PosDef := by⊢ (CartanMatrix.E 8).PosDef pos_defAll goals completed! 🐙

The default method uses a lower triangular transform whose congruence with the matrix is a positive diagonal matrix. The kernel checks the transform's list certificate; it does not replay elimination.

For a symmetric real matrix with nonpositive off-diagonal entries, an explicitly selected method instead solves for a positive vector and checks that its matrix product is positive in every coordinate.

example : (CartanMatrix.E 8).PosDef := by⊢ (CartanMatrix.E 8).PosDef
  pos_def (method := .positiveVector)All goals completed! 🐙

An unavailable specialization reports a capability decline. It does not supply a negative result or automatically run the general method.

39.1.2. A symmetrizer supplied by the caller🔗

The E₈ Cartan matrix is already symmetric, so the constant symmetrizer 1 suffices. The existential witness and its coordinate positivity are ordinary Lean proof steps; pos_def proves the matrix assertion.

example : ∃ d : Fin 8 → ℤ, (∀ i, 0 < d i) ∧
    (Matrix.diagonal d * CartanMatrix.E 8).PosDef := by⊢ ∃ d, (∀ (i : Fin 8), 0 < d i) ∧ (Matrix.diagonal d * CartanMatrix.E 8).PosDef
  refine ⟨fun _ => 1, by⊢ ∀ (i : Fin 8), 0 < (fun x => 1) i simpAll goals completed! 🐙, ?_⟩
  have h : (CartanMatrix.E 8).PosDef := by⊢ ∃ d, (∀ (i : Fin 8), 0 < d i) ∧ (Matrix.diagonal d * CartanMatrix.E 8).PosDef pos_defh:(CartanMatrix.E 8).PosDef⊢ ((Matrix.diagonal fun x => 1) * CartanMatrix.E 8).PosDef
  simpa using hAll goals completed! 🐙

39.1.3. Complex matrices and refutations🔗

Gaussian arithmetic retains both components and conjugates certificate vectors where required. The standard complex order is supplied by ComplexOrder.

open scoped ComplexOrder in
example :
    (!![(2 : ℂ), Complex.I; -Complex.I, 2]).PosDef := by⊢ !![2, Complex.I; -Complex.I, 2].PosDef
  pos_defAll goals completed! 🐙

A nonzero vector with zero quadratic value already refutes positive definiteness. It need not be a kernel vector of the whole matrix.

open scoped ComplexOrder in
example :
    ¬ (!![(1 : ℂ), Complex.I; -Complex.I, 1]).PosDef := by⊢ ¬!![1, Complex.I; -Complex.I, 1].PosDef
  pos_defAll goals completed! 🐙

The tactic checks the evidence before reporting an opposite-polarity result and leaves the requested goal unproved.

39.1.4. Executable certificates and correspondence🔗

inductive type

Hex.PosDef.Certificate (R : Type) : Type
Hex.PosDef.Certificate (R : Type) : Type

A classification retains its polarity.

Constructors

Hex.PosDef.Certificate.positive {R : Type}
  (cert : Hex.PosDef.PositiveCert R) :
  Hex.PosDef.Certificate R

Evidence for positive definiteness.

Hex.PosDef.Certificate.negative {R : Type}
  (cert : Hex.PosDef.NegativeCert R) :
  Hex.PosDef.Certificate R

Evidence against positive definiteness.

inductive type

Hex.PosDef.PositiveCert (R : Type) : Type
Hex.PosDef.PositiveCert (R : Type) : Type

A congruence transform, or an integer positive vector.

Constructors

Hex.PosDef.PositiveCert.triangular {R : Type}
  (transform : List (List R)) : Hex.PosDef.PositiveCert R

Leading entries of each row of a lower triangular congruence transform.

Hex.PosDef.PositiveCert.positiveVector {R : Type}
  (vec : List ℤ) : Hex.PosDef.PositiveCert R

A strictly positive integer vector with strictly positive matrix product.

inductive type

Hex.PosDef.NegativeCert (R : Type) : Type
Hex.PosDef.NegativeCert (R : Type) : Type

A coordinate mismatch, or a nonzero vector with nonpositive quadratic value.

Constructors

Hex.PosDef.NegativeCert.notHermitian {R : Type} (i j : ℕ) :
  Hex.PosDef.NegativeCert R

Coordinates witnessing failure of Hermitian symmetry.

Hex.PosDef.NegativeCert.nonpositive {R : Type}
  (vec : List R) : Hex.PosDef.NegativeCert R

A nonzero vector whose quadratic value is real and nonpositive.

Hex.PosDef.Int.certify accepts an executable square integer matrix and an optional method. Hex.PosDef.Gaussian.certify uses the general method. Successful returns have been rechecked against the original rows. Unsupported methods and rejected producer certificates are separate error constructors.

theorem

Hex.PosDef.Int.certify_check {n : ℕ} (B : Hex.Matrix ℤ n n)
  (method : Hex.PosDef.Method) (c : Hex.PosDef.Certificate ℤ)
  (h : Hex.PosDef.Int.certify B method = Except.ok c) :
  Hex.PosDef.Int.check n B.rowLists c = true
Hex.PosDef.Int.certify_check {n : ℕ}
  (B : Hex.Matrix ℤ n n)
  (method : Hex.PosDef.Method)
  (c : Hex.PosDef.Certificate ℤ)
  (h :
    Hex.PosDef.Int.certify B method =
      Except.ok c) :
  Hex.PosDef.Int.check n B.rowLists c =
    true

Successful return implies independent checker acceptance, without an elimination invariant.

theorem

Hex.PosDef.Gaussian.certify_check {n : ℕ}
  (B : Hex.Matrix Hex.PosDef.Gaussian n n)
  (c : Hex.PosDef.Certificate Hex.PosDef.Gaussian)
  (h : Hex.PosDef.Gaussian.certify B = Except.ok c) :
  Hex.PosDef.Gaussian.check n B.rowLists c = true
Hex.PosDef.Gaussian.certify_check {n : ℕ}
  (B : Hex.Matrix Hex.PosDef.Gaussian n n)
  (c :
    Hex.PosDef.Certificate
      Hex.PosDef.Gaussian)
  (h :
    Hex.PosDef.Gaussian.certify B =
      Except.ok c) :
  Hex.PosDef.Gaussian.check n B.rowLists
      c =
    true

Gaussian successful-return self-validation is independent of exact-division correctness.

The checkers validate exact shapes before list dot products. Positive certificates establish positivity for arbitrary test vectors in the target carrier. Negative certificates give either a non-Hermitian coordinate or a nonzero vector with real nonpositive quadratic value. The soundness theorems accept arbitrary certificates, without a producer provenance assumption.

theorem

Hex.PosDefTheory.Int.checkPositive_sound.{u_1} (R : Type u_1)
  [CommRing R] [PartialOrder R] [StarRing R] [IsStrictOrderedRing R]
  [StarOrderedRing R] [CharZero R] [PosMulReflectLT R]
  [NoZeroDivisors R] (n : ℕ) (rows : List (List ℤ))
  (c : Hex.PosDef.PositiveCert ℤ)
  (h : Hex.PosDef.Int.checkPositive n rows c = true) :
  (Hex.PosDefTheory.Lists.matrix (Hex.PosDefTheory.intModel R) n
      rows).PosDef
Hex.PosDefTheory.Int.checkPositive_sound.{u_1}
  (R : Type u_1) [CommRing R]
  [PartialOrder R] [StarRing R]
  [IsStrictOrderedRing R]
  [StarOrderedRing R] [CharZero R]
  [PosMulReflectLT R] [NoZeroDivisors R]
  (n : ℕ) (rows : List (List ℤ))
  (c : Hex.PosDef.PositiveCert ℤ)
  (h :
    Hex.PosDef.Int.checkPositive n rows
        c =
      true) :
  (Hex.PosDefTheory.Lists.matrix
      (Hex.PosDefTheory.intModel R) n
      rows).PosDef

Integer positive certificates are interpreted directly in the target carrier.

theorem

Hex.PosDefTheory.Int.checkNegative_sound.{u_1} (R : Type u_1)
  [CommRing R] [PartialOrder R] [StarRing R] [IsStrictOrderedRing R]
  [CharZero R] (n : ℕ) (rows : List (List ℤ))
  (c : Hex.PosDef.NegativeCert ℤ)
  (h : Hex.PosDef.Int.checkNegative n rows c = true) :
  ¬(Hex.PosDefTheory.Lists.matrix (Hex.PosDefTheory.intModel R) n
        rows).PosDef
Hex.PosDefTheory.Int.checkNegative_sound.{u_1}
  (R : Type u_1) [CommRing R]
  [PartialOrder R] [StarRing R]
  [IsStrictOrderedRing R] [CharZero R]
  (n : ℕ) (rows : List (List ℤ))
  (c : Hex.PosDef.NegativeCert ℤ)
  (h :
    Hex.PosDef.Int.checkNegative n rows
        c =
      true) :
  ¬(Hex.PosDefTheory.Lists.matrix
        (Hex.PosDefTheory.intModel R) n
        rows).PosDef

Integer negative certificates refute positivity independently of production.

theorem

Hex.PosDefTheory.Gaussian.checkPositive_sound (n : ℕ)
  (rows : List (List Hex.PosDef.Gaussian))
  (c : Hex.PosDef.PositiveCert Hex.PosDef.Gaussian)
  (h : Hex.PosDef.Gaussian.checkPositive n rows c = true) :
  (Hex.PosDefTheory.Lists.matrix Hex.PosDefTheory.gaussianModel n
      rows).PosDef
Hex.PosDefTheory.Gaussian.checkPositive_sound
  (n : ℕ)
  (rows : List (List Hex.PosDef.Gaussian))
  (c :
    Hex.PosDef.PositiveCert
      Hex.PosDef.Gaussian)
  (h :
    Hex.PosDef.Gaussian.checkPositive n
        rows c =
      true) :
  (Hex.PosDefTheory.Lists.matrix
      Hex.PosDefTheory.gaussianModel n
      rows).PosDef

Gaussian congruence certificates imply complex positive definiteness.

theorem

Hex.PosDefTheory.Gaussian.checkNegative_sound (n : ℕ)
  (rows : List (List Hex.PosDef.Gaussian))
  (c : Hex.PosDef.NegativeCert Hex.PosDef.Gaussian)
  (h : Hex.PosDef.Gaussian.checkNegative n rows c = true) :
  ¬(Hex.PosDefTheory.Lists.matrix Hex.PosDefTheory.gaussianModel n
        rows).PosDef
Hex.PosDefTheory.Gaussian.checkNegative_sound
  (n : ℕ)
  (rows : List (List Hex.PosDef.Gaussian))
  (c :
    Hex.PosDef.NegativeCert
      Hex.PosDef.Gaussian)
  (h :
    Hex.PosDef.Gaussian.checkNegative n
        rows c =
      true) :
  ¬(Hex.PosDefTheory.Lists.matrix
        Hex.PosDefTheory.gaussianModel n
        rows).PosDef

Non-Hermitian coordinates and Gaussian quadratic witnesses both refute positivity.

Rational quotation uses one positive denominator for the whole matrix. The Theory wrappers transport the checked result along the proved scaling equation. Real and complex entry equalities are proved by scalar normalization; classical equality is not evaluated by the checker.

The unrestricted general producers always return a classification. Their positive outcome is equivalent to positive definiteness of the decoded matrix; the explicitly selected vector method promises soundness on success.

theorem

Hex.PosDefTheory.Int.certify_complete {n : ℕ} (B : Hex.Matrix ℤ n n) :
  ∃ c,
    Hex.PosDef.Int.certify B = Except.ok c ∧
      ((∃ p, c = Hex.PosDef.Certificate.positive p) ↔
        (Hex.PosDefTheory.Lists.matrix (Hex.PosDefTheory.intModel ℤ) n
            B.rowLists).PosDef)
Hex.PosDefTheory.Int.certify_complete
  {n : ℕ} (B : Hex.Matrix ℤ n n) :
  ∃ c,
    Hex.PosDef.Int.certify B =
        Except.ok c ∧
      ((∃ p,
          c =
            Hex.PosDef.Certificate.positive
              p) ↔
        (Hex.PosDefTheory.Lists.matrix
            (Hex.PosDefTheory.intModel ℤ)
            n B.rowLists).PosDef)

The unrestricted integer producer always classifies its input, and returns positive exactly when its integer interpretation is positive definite.

theorem

Hex.PosDefTheory.Gaussian.certify_complete {n : ℕ}
  (B : Hex.Matrix Hex.PosDef.Gaussian n n) :
  ∃ c,
    Hex.PosDef.Gaussian.certify B = Except.ok c ∧
      ((∃ p, c = Hex.PosDef.Certificate.positive p) ↔
        (Hex.PosDefTheory.Lists.matrix Hex.PosDefTheory.gaussianModel n
            B.rowLists).PosDef)
Hex.PosDefTheory.Gaussian.certify_complete
  {n : ℕ}
  (B :
    Hex.Matrix Hex.PosDef.Gaussian n n) :
  ∃ c,
    Hex.PosDef.Gaussian.certify B =
        Except.ok c ∧
      ((∃ p,
          c =
            Hex.PosDef.Certificate.positive
              p) ↔
        (Hex.PosDefTheory.Lists.matrix
            Hex.PosDefTheory.gaussianModel
            n B.rowLists).PosDef)

The unrestricted Gaussian producer always classifies its input, and returns positive exactly when its complex interpretation is positive definite.