Eigenvalues of 2×2 real matrices: characteristic polynomial, discriminant and nonzero eigenvectors

Goal and scope

For 2×2 real matrices prove: λ is a real eigenvalue ⇔ det(M−λI)=0 ⇔ λ²−tr(M)λ+det(M)=0, and the number of distinct real eigenvalues is decided by the sign of Δ=tr(M)²−4det(M) (negative, zero, positive give 0, 1, 2). For M=[[4,1],[2,3]] find all distinct real eigenvalues with nonzero eigenvectors, show that for the candidate λ=3 the kernel is K₃={0} and 3 is not an eigenvalue, and reject the candidate eigenpair (3,0); then contrast with the rotation R=[[0,−1],[1,0]] (Δ<0) and J=[[3,1],[0,3]] (Δ=0).

Stays inside the MKO's scope: the real field, 2×2 matrices, the nonzero-eigenvector convention. It fully proves 'nonzero kernel ⇔ determinant zero', the characteristic-polynomial formula and the discriminant classification; 'nonzero determinant ⇒ invertible' is cited from the determinant entry. It does not treat algebraic multiplicity, eigenbases, diagonalization, Jordan structure or the complex spectrum, and does not build the Lean HasEigenvector bridge; it does not change the canonical MKO or its English edition.

Givens and symbols

• matrix_product_def
• distributive
• square_nonneg
• sqrt_def
• zero_product
• numeric_evaluation

• G1 — Throughout we work over ℝ; M=[[a,b],[c,d]] is a 2×2 real matrix, vectors are column vectors in ℝ², and I=[[1,0],[0,1]] (MKO assumption a1).
• G2 — Example: M=[[4,1],[2,3]]; candidate value λ=3; candidate eigenpair (3,0).
• G3 — Contrasts: R=[[0,−1],[1,0]] and J=[[3,1],[0,3]].

• \lambda — a candidate real eigenvalue
• K_\lambda=\{v\mid Mv=\lambda v\} — the kernel for a candidate λ, always containing the zero vector
• \operatorname{tr}(M) — the trace a+d
• \Delta — the discriminant tr(M)²−4det(M)
• N=\begin{pmatrix}p&q\\r&s\end{pmatrix} — a general 2×2 real matrix in the lemma

Rules and sources

• matrix_product_def · prerequisite — Matrix product: for A of size m×n and B of size n×p, (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}. Matrix multiplication is in general not commutative.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• sqrt_def · prerequisite — Principal square root: for a≥0, √a is the unique real b with b≥0 and b²=a. Negative numbers have no real square root.
• zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• two_nonzero · prerequisite — In the reals 0<1, hence 0<1+1=2, so 2≠0.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_eig_def · cited — For a 2×2 real matrix M, a real λ is an eigenvalue exactly when some nonzero v∈R² satisfies Mv=λv. This pulse uses the nonzero-eigenvector convention. The candidate-scalar kernel Kλ={v:Mv=λv} includes zero even when λ is not an eigenvalue. Distinct real eigenvalues are the distinct real roots of λ²−tr(M)λ+det(M)=0. · mko-eigenvalue
• mko_det_inv · cited — For M=[[a,b],[c,d]] over R, define D(M)=det(M)=ad−bc. M is invertible over R exactly when det(M)≠0. For 2×2 real matrices A,B, det(AB)=det(A)det(B), and det(tM)=t²det(M). · mko-determinant
• vec_ops · prerequisite — Column vectors in ℝ² add and scale componentwise; two vectors are equal ⇔ both components are equal; the zero vector is 0=(0,0)ᵀ, and v≠0 ⇔ at least one component is nonzero.
• L_kernel_det · lemma — For a 2×2 real matrix N: some nonzero v satisfies Nv=0 ⇔ det(N)=0.
• L_disc · lemma — For reals T and D let Δ=T²−4D. The number of distinct real roots of λ²−Tλ+D=0 is 0 if Δ<0, 1 if Δ=0 (λ=T/2), and 2 if Δ>0 (λ=(T±√Δ)/2).

Main derivation

\lambda\in\mathbb{R}

\lambda\ \text{eigenvalue}\iff\exists v\neq 0:\ Mv=\lambda v;\quad K_\lambda=\{v\mid Mv=\lambda v\}

Mv=\lambda v

(M-\lambda I)v=0

\lambda\ \text{eigenvalue}

\det(M-\lambda I)=0

\det(M-\lambda I)=(a-\lambda)(d-\lambda)-bc

\lambda^2-(a+d)\lambda+(ad-bc)=\lambda^2-\operatorname{tr}(M)\lambda+\det(M)

\Delta=\operatorname{tr}(M)^2-4\det(M)=49-40

\Delta=9>0\ \Rightarrow\ \text{two distinct real eigenvalues}

\lambda=\tfrac{7\pm\sqrt{9}}{2}

\lambda\in\{2,5\},\quad \lambda^2-7\lambda+10=(\lambda-2)(\lambda-5)

(M-5I)v=\begin{pmatrix}-1&1\\2&-2\end{pmatrix}\begin{pmatrix}x\\y\end{pmatrix}=0

K_5=\{(t,t)^{\mathsf T}\mid t\in\mathbb{R}\},\ v=(1,1)^{\mathsf T}:\ Mv=(5,5)^{\mathsf T}=5v

(M-2I)v=\begin{pmatrix}2&1\\2&1\end{pmatrix}\begin{pmatrix}x\\y\end{pmatrix}=0

K_2=\{(t,-2t)^{\mathsf T}\mid t\in\mathbb{R}\},\ v=(1,-2)^{\mathsf T}:\ Mv=(2,-4)^{\mathsf T}=2v

(M-3I)v=\begin{pmatrix}1&1\\2&0\end{pmatrix}\begin{pmatrix}x\\y\end{pmatrix}=0

K_3=\{0\},\ 3\ \text{not an eigenvalue}

(\lambda,v)=(3,0)

M0=0=3\cdot 0\ \text{but}\ v=0\ \Rightarrow\ \text{reject as eigenpair}

R=\begin{pmatrix}0&-1\\1&0\end{pmatrix}

\lambda^2+1,\ \Delta=0^2-4\cdot 1=-4<0\ \Rightarrow\ \text{no real eigenvalue}

J=\begin{pmatrix}3&1\\0&3\end{pmatrix}

(\lambda-3)^2,\ \Delta=36-36=0\ \Rightarrow\ E(J)=\{3\}

\text{tasks of the goal}

E(M)=\{2,5\},\ K_3=\{0\},\ (3,0)\ \text{rejected},\ E(R)=\varnothing,\ E(J)=\{3\}

Substeps and lemmas

\det N=ps-qr=0,\ (p,q)\neq(0,0)

v=(q,-p)^{\mathsf T}\neq 0,\ Nv=(pq-qp,\ rq-sp)^{\mathsf T}=(0,\ -\det N)^{\mathsf T}=0

p=q=0

v=(s,-r)^{\mathsf T}\ \text{if}\ (r,s)\neq(0,0),\ \text{else}\ v=(1,0)^{\mathsf T};\ \ v\neq 0,\ Nv=0

\det N\neq 0,\ Nv=0

v=N^{-1}(Nv)=N^{-1}0=0

\lambda^2-T\lambda+D

\left(\lambda-\tfrac{T}{2}\right)^2-\tfrac{\Delta}{4},\quad \Delta=T^2-4D

\Delta<0

\left(\lambda-\tfrac{T}{2}\right)^2-\tfrac{\Delta}{4}>0\ \text{for all }\lambda:\ \text{no real root}

\Delta=0

\left(\lambda-\tfrac{T}{2}\right)^2=0\iff\lambda=\tfrac{T}{2}:\ \text{exactly one root}

\Delta>0

\lambda=\tfrac{T+\sqrt{\Delta}}{2}\ \lor\ \lambda=\tfrac{T-\sqrt{\Delta}}{2},\ \text{two distinct roots}

Reverse audits

• S13 · sufficient_goal_reduction · S03, S05, S06, S07, S08, S09, S10, S11, S12 — Goal G: the items asked for. Sufficient condition H: the conclusions of S03 to S12; H⇒G uses only conjunction. H is derived forwards from G1 to G3; G is never used as a premise.
• S12 · premise_audit · S03, L_disc, numeric_evaluation — Only the number of distinct real eigenvalues, 1, is claimed; no algebraic multiplicity or eigenbasis is established.
• S11 · premise_audit · S03, L_disc, square_nonneg — This guide works over ℝ only and does not discuss complex eigenvalues.
• S10 · premise_audit · S01, mko_eig_def — The only reason for rejection is v=0; kernel membership and being an eigenpair are different questions.
• S09 · premise_audit · S02, S03, eq_congruence, mul_inverse_nonzero — Solving the equations directly and the determinant criterion agree (N16, N17). The zero vector in the kernel does not create an eigenvalue.
• S08 · premise_audit · S02, exists_intro, numeric_evaluation — Direct computation (N13 to N15) confirms it; the eigenvector is not unique, and any nonzero multiple also works.
• S07 · premise_audit · S02, exists_intro, numeric_evaluation — Being an eigenvalue needs only one nonzero vector; computing Mv directly (N11, N12) confirms it independently.
• S06 · inverse_equivalence · sqrt_def, zero_product, numeric_evaluation — The factorization and the zero-product property give the same two roots in both directions (N7 to N10).
• S05.4 · premise_audit · S05.1, sqrt_def, zero_product, distributive — The zero-product property is two-way, so these two values are roots and the only ones; Δ need not be a perfect square (MKO third paragraph).
• S05.3 · premise_audit · S05.1, square_nonneg — u²=0 ⇔ u=0 holds both ways, so the root exists and is unique.
• S05.2 · premise_audit · S05.1, square_nonneg, order_basics — The conclusion is for every real λ; the argument makes no assumption about λ.
• S05.1 · inverse_equivalence · distributive, frac_rules, two_nonzero — An identity for all reals λ, T, D (N4), two-way.
• S05 · premise_audit · S03, S04, L_disc — It needs the equivalence of S03 to turn the eigenvalue question into a root question; the lemma counts distinct roots, not multiplicities.
• S04 · inverse_equivalence · distributive, neg_mul, add_comm — A polynomial identity (N1), two-way.
• S03.3 · premise_audit · mko_det_inv, contrapositive, vec_ops — It relies on the real-field invertibility criterion of the determinant entry and associativity of matrix multiplication; N⁻¹0=0 because each component is a sum of products with zero.
• S03.2 · premise_audit · S03.1, case_analysis, matrix_product_def — The three cases (first row nonzero; first row zero but second row nonzero; all zero) exhaust every possibility.
• S03.1 · premise_audit · matrix_product_def, vec_ops, neg_mul — The second component vanishes exactly because det N=0; the first row being nonzero guarantees v≠0.
• S03 · inverse_equivalence · L_kernel_det, S02 — Both directions of the lemma are proved (S03.1 and S03.2 for ⇐, S03.3 for ⇒).
• S02 · inverse_equivalence · distributive, vec_ops, add_inverse — Subtracting λv from both sides and adding it back undo each other, so it is two-way.
• S01 · premise_audit · G1, mko_eig_def — This step only states the definition; it derives no new fact.

Error controls and negative controls

The zero vector is not an eigenvector

The first misconception identified in the MKO is treating the zero vector as an eigenvector. M0=λ0 holds for every λ; if v=0 were allowed, every real number would be an 'eigenvalue'. So (3,0) must be rejected (S10), and 3 is indeed not an eigenvalue (S09).

A kernel containing zero does not make an eigenvalue

K₃={0} is nonempty, but it contains only the zero vector; an eigenvalue needs a nonzero vector in the kernel. Kernel-membership questions accept the zero vector and eigenpair questions reject it, and the two kinds of question must be kept apart (MKO assumption a2).

A double root counts as one distinct value

The characteristic polynomial (λ−3)² of J has the double root 3, but there is only one distinct real eigenvalue (S12). Counting it as two distinct values by multiplicity is a misconception the MKO lists.

• M·0=3·0, so 3 is an eigenvalue of M → reject — A nonzero vector is needed; K₃={0} and det(M−3I)=−2≠0.
• K₃ is nonempty, so 3 is an eigenvalue → reject — K₃ contains only the zero vector; every kernel K_λ contains the zero vector.
• J=[[3,1],[0,3]] has two distinct real eigenvalues because its characteristic polynomial is quadratic → reject — Δ=0 and the only root is 3; there is one distinct value.
• Every 2×2 real matrix has at least one real eigenvalue → reject — The characteristic polynomial λ²+1 of R=[[0,−1],[1,0]] has no real root.

Result and limitations

For 2×2 real matrices, λ is a real eigenvalue ⇔ det(M−λI)=0 ⇔ λ²−tr(M)λ+det(M)=0; the number of distinct real eigenvalues is 0, 1, 2 for Δ<0, Δ=0, Δ>0. The distinct real eigenvalues of M=[[4,1],[2,3]] are {2,5}, with eigenvectors (1,−2)ᵀ and (1,1)ᵀ; K₃={0}, so 3 is not an eigenvalue and (3,0) is not an eigenpair. R has no real eigenvalue (Δ=−4), and J has only 3 (Δ=0).

• S03.3 cites 'det≠0 ⇒ invertible over ℝ' from the determinant entry and uses associativity of matrix multiplication; these are not re-proved here.
• Algebraic multiplicity, eigenbases, general diagonalization and the complex spectrum are outside this guide; the MKO's formal next step (binding HasEigenvector and eigenspace) is not done.

Verification and source binding

25 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 27f8549732baa2c4dbec3325cb1a0a6e4dda2523f6dd6b29511686514a143988
• original source SHA-256: 27f8549732baa2c4dbec3325cb1a0a6e4dda2523f6dd6b29511686514a143988
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)