Matrix interpretations are widely used in automated complexity analysis.
Certifying such analyses boils down to
determining the growth rate of $A^n$ for a fixed non-negative rational
matrix $A$. A direct solution for this task
involves the computation of all eigenvalues of $A$, which
often leads to expensive algebraic number computations.

In this work we formalize
the Perron–Frobenius theorem.
We utilize the theorem to avoid most of the algebraic numbers
needed for certifying complexity analysis,
so that our new algorithm only needs the
rational
arithmetic
when certifying complexity proofs that existing tools can find.
To cover the theorem in its full extent,
we establish a connection between two different Isabelle/HOL
libraries on matrices,
enabling an easy exchange of theorems between both libraries.
This connection crucially relies on the transfer mechanism
in combination with local type definitions, being a non-trivial case study for
these Isabelle tools.