Most vectors are turned by a matrix. A few directions are only stretched. Find them, and the matrix acts as a list of numbers along those directions: powers become easy, trace and determinant become the sum and the product of the numbers, and a recurrence like the Fibonacci numbers acquires a closed form.
The object. A real 2×2 matrix A. Choose its entries and read off the trace T, the determinant D, the discriminant T² − 4D, the eigenvalues (real, repeated or a complex pair), an eigenvector for each real one, and what AN does to a vector as N grows. The button counts the 2,401 matrices with entries from −3 to 3 by the sign of the discriminant.
Apply a matrix to a vector and you usually get a vector pointing somewhere else. Occasionally the answer lies on the same line through the origin: the vector has been stretched, shrunk or flipped, and nothing more. Such a vector is an eigenvector, and the stretch factor is its eigenvalue. If it exists, applying the matrix N times just multiplies by the factor N times, so the long-run behaviour of the system is read off the factor.
ANh = AN−1(ah) = a AN−1h, and induction on N gives aNh. □
Lax’s Example 1 (p.61), A = [[3,2],[1,4]]. The vector (2,−1) is sent to (6−2, 2−4) = (4,−2) = 2(2,−1), so it is an eigenvector with eigenvalue 2. The vector (1,1) is sent to (5,5) = 5(1,1), so it is an eigenvector with eigenvalue 5. They are not multiples of each other, so every vector is a combination b1(2,−1) + b2(1,1), and then AN applied to it is b12N(2,−1) + b25N(1,1). The 5N part dominates. Lax computes A1024 by ten squarings and sees entries above 10700; the script finds that every entry of A1024 has 716 digits, which is consistent with 51024/3 times a small constant.
Lax pp.59–62. Lean: power_eigen, a short induction, compiled. The script checks that (2,−1) and (1,1) are eigenvectors, that det[[2,1],[−1,1]] = 3 (so they are independent), that A = PDP−1 exactly with P = [[2,1],[−1,1]] and D = diag(2,5), that A10 = PD10P−1 exactly, and the digit count of A1024.
The equation Ah = ah says (A − aI)h = 0 with h not zero, which can happen only if A − aI squashes some nonzero vector to zero, that is, only if A − aI is not invertible. Chapter 6 says that happens exactly when its determinant vanishes. So the eigenvalues are the roots of a polynomial in a.
The iff. By Corollary 3 of chapter 6, A − aI is not invertible if and only if its determinant is zero; and a matrix is not invertible if and only if it has a nonzero vector in its nullspace. Hence a nonzero h with (A − aI)h = 0 exists exactly when det(aI − A) = 0 (the sign of the matrix does not change whether the determinant is zero).
The 2×2 case of Theorem 3. For A = [[p,q],[r,s]], det(tI − A) = (t − p)(t − s) − qr = t2 − (p + s)t + (ps − qr). If its roots are a1 and a2 this equals (t − a1)(t − a2) = t2 − (a1 + a2)t + a1a2, so a1 + a2 = p + s = tr A and a1a2 = ps − qr = det A. For Example 1, t2 − 7t + 10 = (t − 2)(t − 5), trace 7 = 2 + 5 and determinant 10 = 2 × 5. For general n the proof is Lax’s (p.65), by expanding the determinant as a sum over permutations: only the product of the diagonal entries contains tn and tn−1, and the constant term is det(−A).
Lean: eigen_iff_det_zero (a proof from Matrix.exists_mulVec_eq_zero_iff), trace_eq_sum_eigenvalues and det_eq_prod_eigenvalues (Mathlib’s Matrix.trace_eq_sum_roots_charpoly_of_splits and the determinant analogue), all compiled. The script checks the iff exhaustively for every 2×2 matrix over F3 and F5 and every 3×3 matrix over F2, for every a in the field; it computes det(tI − A) exactly for 200 random integer 3×3 and 200 random 4×4 matrices (fixed seed) and checks that it is monic, that the coefficient of tn−1 is −tr A and that the constant term is (−1)n det A. The existence argument uses the fundamental theorem of algebra, which is not proved here and which Lean’s file does not state. Control: [[1,2],[2,4]] has characteristic polynomial t2 − 5t, so 0 is an eigenvalue, and its determinant is 0.
Two eigenvectors that belonged to different stretch factors cannot lie on the same line, since on one line the matrix has only one stretch factor. The same idea works for any number: eigenvectors with different eigenvalues never become dependent. So if an n×n matrix has n different eigenvalues, it has n independent eigenvectors, a basis in which the matrix is just a list of numbers.
Theorem 1, two eigenvectors. Suppose Ah = ah and Ak = bk with a ≠ b, and suppose a relation xh + yk = 0 with x, y not both zero. Applying A gives xah + ybk = 0. Subtracting a times the first relation leaves y(b − a)k = 0; since k ≠ 0 and b ≠ a, y = 0. Then xh = 0 and h ≠ 0 give x = 0, a contradiction. For more eigenvectors, Lax takes a relation with the fewest terms and shortens it in the same way (p.64).
Fibonacci. (φ − ψ) = √5, φψ = −1, φ + ψ = 1, so φ and ψ are the roots of t2 − t − 1. The vector (φ, 1) is sent by A to (φ + 1, φ) = φ(φ, 1), since φ + 1 = φ2; similarly for ψ. Write (1, 0) = [(φ, 1) − (ψ, 1)]/√5. Then An(1, 0) = [φn(φ, 1) − ψn(ψ, 1)]/√5, and the second coordinate is (φn − ψn)/√5 = Fn. Since |ψ| < 1, |ψn/√5| ≤ 1/√5 < 1/2 for n ≥ 0. For example, F32 = 2,178,309 (Lax’s Exercise 1). □
Lean: eigenvectors_distinct_independent is Mathlib’s Module.End.eigenvectors_linearIndependent, stated for a linear map on any vector space; compiled. The script checks Theorem 1 exhaustively over a finite field: for every 2×2 matrix over F5 and every 3×3 matrix over F3, eigenvectors of distinct eigenvalues (up to six per eigenspace) are independent. It checks the Fibonacci facts in exact arithmetic in the field Q(√5): φ and ψ are roots of t2 − t − 1; φn − ψn = Fn√5 for n = 0 to 60; the matrix power [[1,1],[1,0]]n is [[Fn+1,Fn],[Fn,Fn−1]] for n = 1 to 60; and F32 = 2,178,309.
For a 2×2 matrix the characteristic polynomial is a quadratic, t2 − Tt + D, and the sign of its discriminant T2 − 4D = (a − d)2 + 4bc settles the picture. Positive: two real stretch factors, two directions. Negative: no real direction at all, as for a rotation, and a complex pair. Zero: one factor, and two possibilities, the matrix is a multiple of the identity, or it has only one direction and is “defective”.
The roots of t2 − Tt + D are (T ± √(T2 − 4D))/2, and T2 − 4D = (a + d)2 − 4(ad − bc) = (a − d)2 + 4bc. This gives the three cases for the roots. For Δ = 0 with the double root λ = (a + d)/2, if A − λI had rank 0 then A = λI; otherwise it has rank 1, so its nullspace is a line. For the rotation by a quarter turn, [[0,−1],[1,0]], Δ = −4, and no real vector is sent to a real multiple of itself; over the complex numbers the eigenvalues are ±i. □
Lean: control_rotation_no_real_eigenvalue, from eigen_iff_det_zero and a square being non-negative; compiled. The script runs over all 2,401 integer matrices with entries from −3 to 3: the characteristic polynomial is t2 − (a + d)t + (ad − bc) in every case; 1,632 have Δ > 0, 127 have Δ = 0 and 642 have Δ < 0; of the 127 repeated cases, 7 are scalar (rank of A − λI is 0) and the other 120 have rank 1, a single eigenvector direction. Controls: the rotation has no eigenvector over F3 (t2 + 1 has no root there) but has eigenvectors over F5, where t2 + 1 = (t − 2)(t − 3); whether eigenvalues exist depends on the field. And [[1,1],[0,1]] has the double eigenvalue 1 but only the line through (1,0).
If h is an eigenvector then A2h = a2h, A3h = a3h, and so any polynomial q(A) multiplies h by q(a). In particular the characteristic polynomial, which is zero at every eigenvalue, kills every eigenvector. If there are enough eigenvectors to span the space, pA(A) is zero on all of it. The surprise of the Cayley–Hamilton theorem is that this holds for every matrix, with or without a full set of eigenvectors.
The 2×2 case by direct computation. For A = [[a,b],[c,d]], A2 = [[a2 + bc, ab + bd],[ac + cd, bc + d2]] and TA = [[a2 + ad, ab + bd],[ac + cd, ad + d2]]. So A2 − TA = [[bc − ad, 0],[0, bc − ad]] = −DI, which is the statement. Then A(TI − A) = TA − A2 = DI, and dividing by D gives the inverse. For general n, Lax’s proof (pp.67–68) multiplies the cofactor matrix of sI − A by sI − A to get pA(s)I and then substitutes s = A.
Spectral mapping, an example. For A = [[3,2],[1,4]] and q(x) = x2 − 3x + 1: q(A) = A2 − 3A + I = [[11,14],[7,18]] − [[9,6],[3,12]] + I = [[3,8],[4,7]], with trace 10 and determinant −11. The eigenvalues are q(2) = −1 and q(5) = 11: their sum is 10 and their product is −11, and q(A) sends (2,−1) to −(2,−1) and (1,1) to 11(1,1).
Lean: cayley_hamilton is Mathlib’s Matrix.aeval_self_charpoly; the file does not state the spectral mapping theorem. The script checks A2 − TA + DI = 0 for all 2,401 integer 2×2 matrices with entries −3..3; pA(A) = 0, in exact rational arithmetic, for 200 random integer 3×3 matrices; the inverse formula for every one of the 2×2 matrices with D ≠ 0; and the spectral mapping example above. Controls: if the constant term of the characteristic polynomial is dropped, A2 − 7A for Example 1 equals −10I, not 0, so the statement needs the whole polynomial; and A + A = 2A has eigenvalues 4 and 10, twice those of A (characteristic polynomial t2 − 14t + 40).
Three things are left out on purpose. The minimal polynomial and the Jordan form, which say what to do when there are not enough eigenvectors (the matrices with Δ = 0 above are the first case), are not in this chapter, and the volume’s plan for them is open. The behaviour of a nonlinear system near a fixed point, where eigenvalues of the Jacobian decide the picture, is not covered; that needs a theorem about linearisation that is not proved here. And the spectral theorem for symmetric matrices, which guarantees real eigenvalues and orthogonal eigenvectors, belongs to the next chapter with inner products. Lax works over the complex numbers throughout, so that every characteristic polynomial has a full set of roots; over the reals, as the rotation shows, it can fail.