Skip to content

Instantly share code, notes, and snippets.

@davidad
Created February 13, 2026 14:25
Show Gist options
  • Select an option

  • Save davidad/9788df827d84cbab6d24555f74e52c90 to your computer and use it in GitHub Desktop.

Select an option

Save davidad/9788df827d84cbab6d24555f74e52c90 to your computer and use it in GitHub Desktop.
\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\title{A Deterministic Certificate for Strict Positive Definiteness via a Triangular Inverse}
\author{}
\date{}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{remark}{Remark}
\begin{document}
\maketitle
\section{Statement}
Let $A\in\mathbb{R}^{n\times n}$ be symmetric. We describe a deterministic certificate of size $\mathcal{O}(n^2)$ that implies $A\succ 0$ and can be verified in $\mathcal{O}(T(A))$ arithmetic operations, where
\[
T(A)\;=\;\sum_{i=1}^n \alpha_i (n-i+1),
\]
and $\alpha_i$ is the number of nonzeros in row $i$ of $A$ (so $T(A)\le \mathrm{nnz}(A)\,n$).
\begin{theorem}[Triangular-inverse certificate for $A\succ 0$]
\label{thm:cert}
Let $A\in\mathbb{R}^{n\times n}$ be symmetric. Suppose there exists a \emph{unit upper-triangular} matrix
$Z\in\mathbb{R}^{n\times n}$ (i.e.\ $Z_{ii}=1$ and $Z_{ij}=0$ for $i>j$) such that
\[
M:=AZ
\]
is \emph{lower-triangular} and has strictly positive diagonal entries $M_{ii}>0$ for all $i$.
Then $A$ is strictly positive definite.
\end{theorem}
\section{Certificate and verification}
\subsection{Certificate construction (prover)}
If $A\succ 0$, it admits an LDL$^\top$ factorization
\[
A = LDL^\top,
\]
where $L$ is unit lower-triangular and $D$ is diagonal with strictly positive entries.
Define the certificate
\[
Z := (L^\top)^{-1}.
\]
Then $Z$ is unit upper-triangular and satisfies $AZ = L D$ (hence $AZ$ is lower-triangular and $(AZ)_{ii}=D_{ii}>0$).
\subsection{Verification algorithm (verifier)}
Given $A$ (stored sparsely) and a dense certificate $Z$, verify:
\begin{enumerate}
\item \textbf{Symmetry:} check $A=A^\top$ (time $\mathcal{O}(\mathrm{nnz}(A))$).
\item \textbf{Structure of $Z$:} check $Z$ is unit upper-triangular (time $\mathcal{O}(n^2)$).
\item \textbf{Triangularity/positivity check:} for each row $i$, compute the entries
\[
(AZ)_{i,j}\quad \text{for } j=i,i+1,\dots,n
\]
and check $(AZ)_{i,i}>0$ and $(AZ)_{i,j}=0$ for all $j>i$.
\end{enumerate}
\paragraph{Work bound.}
Let $J_i=\{k:\;A_{ik}\neq 0\}$ and $\alpha_i=|J_i|$. For fixed $i$ and each $j\ge i$,
\[
(AZ)_{i,j}=\sum_{k\in J_i} A_{ik} Z_{k,j}.
\]
Computing all $(AZ)_{i,j}$ for $j=i,\dots,n$ costs $\mathcal{O}(\alpha_i(n-i+1))$ operations, hence total cost
$\mathcal{O}(T(A))$ with $T(A)=\sum_{i=1}^n \alpha_i(n-i+1)\le \mathrm{nnz}(A)\,n$.
Without any further assumptions, the worst-case bound $T(A)\le \mathrm{nnz}(A)\,n$ can be tight, depending on how
the nonzeros are distributed across rows (and where those rows occur in the ordering).
In particular, since any SPD matrix has all diagonal entries nonzero, $\mathrm{nnz}(A)\ge n$ and hence the average
row sparsity parameter $\alpha=\mathrm{nnz}(A)/n$ satisfies $\alpha\ge 1$. Therefore $\alpha n^2 \le \alpha^2 n^2$,
so $T(A)\le \mathrm{nnz}(A)\,n = \alpha n^2 \le \alpha^2 n^2$. Thus the verifier meets the desired
$\mathcal{O}(\alpha^2 n^2)$ verification-time upper bound.
If one additionally has a uniform per-row bound $\alpha_i\le \alpha_{\max}$ for all $i$, then
\[
T(A)=\sum_{i=1}^n \alpha_i(n-i+1) \le \alpha_{\max}\sum_{i=1}^n (n-i+1)= \alpha_{\max}\frac{n(n+1)}{2}
=\mathcal{O}(\alpha_{\max} n^2).
\]
\begin{remark}[Level-2 BLAS mapping]
For each row $i$, one can form the length-$(n-i+1)$ vector $m^{(i)}=(AZ)_{i,i:n}$ as a sum of $\alpha_i$ scaled
rows of $Z$ restricted to columns $i:n$:
\[
m^{(i)}=\sum_{k\in J_i} A_{ik}\, Z_{k,i:n}.
\]
This is implementable as a sequence of \texttt{saxpy} updates, and is naturally organized around Level-2 BLAS
matrix--vector style kernels (\texttt{sgemv}-like access patterns) depending on the chosen storage layout for $Z$.
\end{remark}
\section{Soundness proof}
\begin{lemma}
\label{lem:diag}
Under the hypotheses of Theorem~\ref{thm:cert}, the matrix $K:=Z^\top A Z$ is diagonal with strictly positive diagonal entries.
\end{lemma}
\begin{proof}
Let $M=AZ$. By assumption, $M$ is lower-triangular with $M_{ii}>0$.
Then
\[
K = Z^\top A Z = Z^\top (AZ)=Z^\top M.
\]
Since $Z$ is upper-triangular, $Z^\top$ is lower-triangular, and the product of two lower-triangular matrices is lower-triangular.
Thus $K$ is lower-triangular.
Because $A$ is symmetric, $K=Z^\top A Z$ is symmetric. A matrix that is both symmetric and lower-triangular must be diagonal.
Moreover, the diagonal of a product of lower-triangular matrices is the product of their diagonals, so
\[
K_{ii} = (Z^\top)_{ii} M_{ii} = 1\cdot M_{ii} > 0.
\]
\end{proof}
\begin{proof}[Proof of Theorem~\ref{thm:cert}]
By Lemma~\ref{lem:diag}, $K=Z^\top A Z$ is diagonal with strictly positive diagonal entries, hence $K\succ 0$.
Since $Z$ is unit triangular it is invertible. For any $x\neq 0$, let $y=Zx\neq 0$; then
\[
x^\top A x = x^\top Z^{-\top} K Z^{-1} x = y^\top K y > 0.
\]
Therefore $A\succ 0$.
\end{proof}
\section{Spectral interpretation}
The certificate is phrased in entrywise terms (triangularity and diagonal positivity), but its content is spectral.
Indeed, the verifier's conditions force the \emph{congruence transform}
\[
K := Z^\top A Z
\]
to be diagonal with strictly positive diagonal entries (Lemma~\ref{lem:diag}), hence $K\succ 0$.
Congruence does not preserve eigenvalues, but it does preserve \emph{inertia} (the numbers of positive, negative, and zero eigenvalues).
Thus $K\succ 0$ implies that $A$ has inertia $(n,0,0)$, equivalently $A\succ 0$.
\paragraph{Quadratic form viewpoint.}
For any $x\neq 0$, letting $y=Zx\neq 0$ gives
\[
x^\top A x = y^\top K y.
\]
Since $K$ is a positive diagonal matrix, $y^\top K y>0$ for all $y\neq 0$, so $x^\top A x>0$ for all $x\neq 0$.
This is exactly the spectral property that all eigenvalues of a symmetric matrix are positive.
\paragraph{Relation to LDL$^\top$.}
In the ``honest'' construction from an LDL$^\top$ factorization $A=LDL^\top$ with $D_{ii}>0$ and $Z=(L^\top)^{-1}$,
one obtains $K=Z^\top A Z = D$. In that case the certificate explicitly exhibits a change of variables that makes the
quadratic form diagonal.
\section{Implementation note: implicit access to dense components}
In some applications, $A$ may be presented implicitly as a combination of a sparse matrix and low-rank/dense terms,
e.g.\ $A=\pm M + aJ + bI$, where $M$ is sparse and $J=\mathbf{1}\mathbf{1}^\top$.
Even though $J$ is dense, multiplying by $J$ is cheap:
\[
Jv = (\mathbf{1}^\top v)\,\mathbf{1},
\]
which can be computed in $\mathcal{O}(n)$ time.
Thus, for any column $z_j$ of the certificate $Z$, the product $Az_j$ can be computed as
\[
Az_j = \pm (Mz_j) + a(\mathbf{1}^\top z_j)\mathbf{1} + b z_j,
\]
costing $\mathcal{O}(\mathrm{nnz}(M)+n)$ time (assuming $Mz_j$ is computed from the sparse representation).
This can be used to implement the verifier without ever explicitly forming the dense matrix $J$.
\section{Numerical analysis in floating-point (IEEE 754) via directed rounding}
IEEE~754 supports directed rounding modes (round-down $\downarrow$, round-up $\uparrow$).
Using them, one can compute \emph{rigorous enclosures} for each dot product and thereby validate a certificate
without any heuristic tolerances.
\subsection{One-pass enclosures using fused multiply-add (FMA)}
\label{sec:dirround-fma}
Assume the platform provides correctly rounded fused multiply-add operations:
\[
\mathrm{fma}(x,y,z) = \mathrm{round}(xy+z),
\]
where ``round'' is according to the currently selected rounding mode.
Fix a row $i$ and a column $j\ge i$. Consider the exact dot product
\[
M_{ij} = \sum_{k\in J_i} A_{ik}Z_{kj}.
\]
Define a running interval $[s^-,s^+]$ initialized to $[0,0]$.
For each term $t_k:=A_{ik}Z_{kj}$, compute a \emph{product enclosure} as
\[
p^-_k := \mathrm{fma}_{\downarrow}(A_{ik},Z_{kj},0),\qquad
p^+_k := \mathrm{fma}_{\uparrow}(A_{ik},Z_{kj},0),
\]
and then update the running sum enclosure by directed rounded additions:
\[
s^- \leftarrow \mathrm{add}_{\downarrow}(s^-,p^-_k),\qquad
s^+ \leftarrow \mathrm{add}_{\uparrow}(s^+,p^+_k).
\]
At the end of the loop, the interval $[s^-,s^+]$ is a \emph{mathematically rigorous enclosure} for $M_{ij}$:
\[
M_{ij}\in [s^-,s^+].
\]
Crucially, this construction is \emph{single-pass}: each nonzero term is processed once, and no explicit error constants
such as $\gamma_m$ are required.
\subsection{Certifying a margin}
\label{sec:dirround-margin}
It is numerically preferable to certify a positive margin $\gamma>0$ by verifying
\[
(A-\gamma I)\succ 0.
\]
This is done by replacing each diagonal entry by $A_{ii}\leftarrow A_{ii}-\gamma$ in the dot products above.
Let $[M^-_{ij},M^+_{ij}]$ be the resulting enclosures for $M^{(\gamma)}=(A-\gamma I)Z$.
A \emph{sufficient} acceptance test is:
\begin{align*}
&\text{for all } i:\qquad M^-_{ii} > 0,\\
&\text{for all } i<j:\qquad 0\in [M^-_{ij},M^+_{ij}].
\end{align*}
The diagonal condition is robust: it proves, in exact arithmetic, that $(A-\gamma I)Z$ has positive diagonal entries.
For the off-diagonal conditions, the ``ideal'' target is $M_{ij}=0$ for $i<j$. A tight enclosure with $0\in[M^-_{ij},M^+_{ij}]$
is exactly the directed-rounding analogue of a tolerance check, but now with a \emph{machine-checked} bound.
In practice, if $A-\gamma I$ is well separated from singularity, the enclosure width is small enough that these checks pass.
\subsection{Interpretation}
If the enclosure checks succeed for some $\gamma>0$, then (in real arithmetic) the computed intervals certify that
the exact matrix $M^{(\gamma)}=(A-\gamma I)Z$ is lower-triangular with strictly positive diagonal, hence
$(A-\gamma I)\succ 0$ and therefore $\lambda_{\min}(A)\ge \gamma$.
\begin{remark}[When FMA or directed rounding is unavailable]
Without FMA and directed rounding control, one can still obtain rigorous enclosures, but typically at higher cost
(e.g.\ two-pass interval dot products, long accumulators, or exact summation techniques).
\end{remark}
\end{document}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment