# Eigenvalues of 2×2 real matrices: characteristic polynomial, discriminant and nonzero eigenvectors [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-eigenvalue/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-eigenvalue-01 · production-20261019-adopted-96 ## 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 uv holds; u0 give uwvw. - 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 S01 · definitionBefore \lambda\in\mathbb{R} After \lambda\ \text{eigenvalue}\iff\exists v\neq 0:\ Mv=\lambda v;\quad K_\lambda=\{v\mid Mv=\lambda v\} Conditions: none Rule: mko_eig_def · Uses: G1 Leaf basis: mko_eig_def + def_unfold State the MKO's definition and the nonzero-eigenvector convention. The kernel K_λ consists of all vectors with Mv=λv (the zero vector included); being an eigenvalue requires a nonzero vector in the kernel. The two must be kept apart: since M0=0=λ0 for every λ, the zero vector alone cannot make any λ an eigenvalue. S02 · equivalentBefore Mv=\lambda v After (M-\lambda I)v=0 Conditions: none Rule: distributive · Uses: S01, matrix_product_def, vec_ops Leaf basis: distributive + matrix_product_def + vec_ops + add_inverse Let v=(x,y)ᵀ. (M−λI)v=((a−λ)x+by, cx+(d−λ)y)ᵀ, which by distributivity equals (ax+by−λx, cx+dy−λy)ᵀ=Mv−λv. So Mv=λv ⇔ Mv−λv=0 ⇔ (M−λI)v=0. Hence K_λ is the null space of M−λI. S03 · equivalentBefore \lambda\ \text{eigenvalue} After \det(M-\lambda I)=0 Conditions: none Rule: L_kernel_det · Uses: S01, S02, L_kernel_det Leaf basis: L_kernel_det + logic_chain By S01 and S02, λ is an eigenvalue ⇔ some nonzero v satisfies (M−λI)v=0. Applying Lemma L_kernel_det to N=M−λI, this is equivalent to det(M−λI)=0. The lemma is proved in S03.1 to S03.3. S04 · equivalentBefore \det(M-\lambda I)=(a-\lambda)(d-\lambda)-bc After \lambda^2-(a+d)\lambda+(ad-bc)=\lambda^2-\operatorname{tr}(M)\lambda+\det(M) Conditions: none Rule: distributive · Uses: S03, G1 Leaf basis: distributive + neg_mul + add_comm + mko_det_inv M−λI=[[a−λ,b],[c,d−λ]], and the definition of the determinant gives the left side. Expand (a−λ)(d−λ)=ad−aλ−dλ+λ², subtract bc and collect terms: λ²−(a+d)λ+(ad−bc). For the example M: tr(M)=4+3=7 and det(M)=4·3−1·2=10, so the characteristic polynomial is λ²−7λ+10. S05 · theorem_applicationBefore \Delta=\operatorname{tr}(M)^2-4\det(M)=49-40 After \Delta=9>0\ \Rightarrow\ \text{two distinct real eigenvalues} Conditions: none Rule: L_disc · Uses: S04, L_disc Leaf basis: L_disc + numeric_evaluation By S03 and S04 the distinct real eigenvalues are exactly the distinct real roots of λ²−7λ+10=0. Δ=7²−4·10=9>0, so by Lemma L_disc (T=7, D=10) there are exactly two distinct real roots. The lemma is proved in S05.1 to S05.4, covering the three cases of MKO assumption a3. S06 · equivalentBefore \lambda=\tfrac{7\pm\sqrt{9}}{2} After \lambda\in\{2,5\},\quad \lambda^2-7\lambda+10=(\lambda-2)(\lambda-5) Conditions: none Rule: sqrt_def · Uses: S05, sqrt_def Leaf basis: sqrt_def + zero_product + numeric_evaluation 3≥0 and 3²=9, so √9=3 by sqrt_def, and the two roots are (7+3)/2=5 and (7−3)/2=2. Cross-check: (λ−2)(λ−5)=λ²−7λ+10. By S03 the set of distinct real eigenvalues of M is {2,5}. S07 · impliesBefore (M-5I)v=\begin{pmatrix}-1&1\\2&-2\end{pmatrix}\begin{pmatrix}x\\y\end{pmatrix}=0 After K_5=\{(t,t)^{\mathsf T}\mid t\in\mathbb{R}\},\ v=(1,1)^{\mathsf T}:\ Mv=(5,5)^{\mathsf T}=5v Conditions: none Rule: exists_intro · Uses: S02, S06, G2 Leaf basis: exists_intro + matrix_product_def + numeric_evaluation (M−5I)v=(−x+y, 2x−2y)ᵀ=0 ⇔ y=x (the second equation is −2 times the first). So K₅ is the line {(t,t)ᵀ}, which contains the zero vector at t=0. Taking t=1 gives the nonzero vector v=(1,1)ᵀ with Mv=(4+1, 2+3)ᵀ=(5,5)ᵀ=5v, so 5 is an eigenvalue and v is an eigenvector. S08 · impliesBefore (M-2I)v=\begin{pmatrix}2&1\\2&1\end{pmatrix}\begin{pmatrix}x\\y\end{pmatrix}=0 After K_2=\{(t,-2t)^{\mathsf T}\mid t\in\mathbb{R}\},\ v=(1,-2)^{\mathsf T}:\ Mv=(2,-4)^{\mathsf T}=2v Conditions: none Rule: exists_intro · Uses: S02, S06, G2 Leaf basis: exists_intro + matrix_product_def + numeric_evaluation (M−2I)v=(2x+y, 2x+y)ᵀ=0 ⇔ y=−2x. Taking x=1 gives v=(1,−2)ᵀ≠0 with Mv=(4−2, 2−6)ᵀ=(2,−4)ᵀ=2v, so 2 is an eigenvalue. S09 · impliesBefore (M-3I)v=\begin{pmatrix}1&1\\2&0\end{pmatrix}\begin{pmatrix}x\\y\end{pmatrix}=0 After K_3=\{0\},\ 3\ \text{not an eigenvalue} Conditions: none Rule: eq_congruence · Uses: S02, S03, S04, G2 Leaf basis: eq_congruence + mul_inverse_nonzero + two_nonzero + numeric_evaluation (M−3I)v=(x+y, 2x)ᵀ=0: from 2x=0 we get x=0, and then x+y=0 gives y=0. So K₃={0}: the zero vector is in the kernel but no nonzero vector is, and 3 is not an eigenvalue. Cross-check: det(M−3I)=1·0−1·2=−2≠0 (S03), and the characteristic polynomial at 3 is 9−21+10=−2≠0 (S04). S10 · impliesBefore (\lambda,v)=(3,0) After M0=0=3\cdot 0\ \text{but}\ v=0\ \Rightarrow\ \text{reject as eigenpair} Conditions: none Rule: mko_eig_def · Uses: S01, S09, G2 Leaf basis: mko_eig_def + mul_zero The candidate eigenpair (3,0) satisfies M0=0=3·0, so 0∈K₃ (a kernel-membership question accepts it); but the nonzero-eigenvector convention requires v≠0, so it must be rejected as an eigenpair (MKO assumption a2). Likewise (5,0) is not an eigenpair, even though 5 is an eigenvalue. S11 · impliesBefore R=\begin{pmatrix}0&-1\\1&0\end{pmatrix} After \lambda^2+1,\ \Delta=0^2-4\cdot 1=-4<0\ \Rightarrow\ \text{no real eigenvalue} Conditions: none Rule: L_disc · Uses: S03, S04, S05, G3 Leaf basis: L_disc + square_nonneg + numeric_evaluation tr(R)=0 and det(R)=0·0−(−1)·1=1, so the characteristic polynomial is λ²+1 and Δ=−4<0. By L_disc (the case Δ<0) there is no real root; directly, λ²+1≥1>0. By S03, R has no real eigenvalue: not every real matrix has a real eigenvalue (MKO assumption a1). S12 · impliesBefore J=\begin{pmatrix}3&1\\0&3\end{pmatrix} After (\lambda-3)^2,\ \Delta=36-36=0\ \Rightarrow\ E(J)=\{3\} Conditions: none Rule: L_disc · Uses: S03, S04, S05, G3 Leaf basis: L_disc + numeric_evaluation + exists_intro tr(J)=6 and det(J)=9, so the characteristic polynomial is λ²−6λ+9=(λ−3)² and Δ=36−36=0. By L_disc (the case Δ=0) there is exactly one distinct real eigenvalue, 3; it is a double root, but the set of distinct eigenvalues lists it once, {3}, and does not count it twice. A nonzero eigenvector is for example (1,0)ᵀ: J(1,0)ᵀ=(3,0)ᵀ. S13 · impliesBefore \text{tasks of the goal} After E(M)=\{2,5\},\ K_3=\{0\},\ (3,0)\ \text{rejected},\ E(R)=\varnothing,\ E(J)=\{3\} Conditions: none Rule: and_intro_elim · Uses: S03, S05, S06, S07, S08, S09, S10, S11, S12 Leaf basis: and_intro_elim Combine: the general results S03 and S05; the distinct real eigenvalues of M are {2,5}, with (1,−2)ᵀ an eigenvector for 2 and (1,1)ᵀ an eigenvector for 5; the candidate 3 has kernel {0} and is not an eigenvalue; (3,0) is not an eigenpair; R has no real eigenvalue; J has exactly one distinct real eigenvalue, 3. ## Substeps and lemmas S03.1 · impliesBefore \det N=ps-qr=0,\ (p,q)\neq(0,0) After v=(q,-p)^{\mathsf T}\neq 0,\ Nv=(pq-qp,\ rq-sp)^{\mathsf T}=(0,\ -\det N)^{\mathsf T}=0 Conditions: \det N=0; (p,q)\neq(0,0) Rule: matrix_product_def · Uses: matrix_product_def, vec_ops Leaf basis: matrix_product_def + vec_ops + neg_mul + mul_comm Case one: the first row is not all zero. Take v=(q,−p)ᵀ; since at least one of p, q is nonzero, v≠0 (vec_ops). Compute Nv: the first component is pq+q(−p)=0 and the second is rq+s(−p)=−(ps−qr)=−det N=0. So v is a nonzero kernel vector. S03.2 · impliesBefore p=q=0 After v=(s,-r)^{\mathsf T}\ \text{if}\ (r,s)\neq(0,0),\ \text{else}\ v=(1,0)^{\mathsf T};\ \ v\neq 0,\ Nv=0 Conditions: p=q=0 Rule: case_analysis · Uses: S03.1, matrix_product_def, vec_ops Leaf basis: case_analysis + matrix_product_def + mul_zero + vec_ops Case two: p=q=0 (then det N=0·s−0·r=0 automatically). If (r,s)≠(0,0), take v=(s,−r)ᵀ≠0: the first component is 0·s+0·(−r)=0 and the second is rs+s(−r)=0. If r=s=0, N is the zero matrix; take v=(1,0)ᵀ, so Nv=0. These cases together with S03.1 cover every N with det N=0, so 'det N=0 ⇒ some nonzero kernel vector' holds. S03.3 · impliesBefore \det N\neq 0,\ Nv=0 After v=N^{-1}(Nv)=N^{-1}0=0 Conditions: \det N\neq 0 Rule: contrapositive · Uses: mko_det_inv, vec_ops Leaf basis: mko_det_inv + contrapositive + mul_zero Prove 'some nonzero kernel vector ⇒ det N=0' by contraposition: suppose det N≠0. By the determinant entry (cited), N is invertible over ℝ. If Nv=0, multiply both sides on the left by N⁻¹: v=N⁻¹(Nv)=N⁻¹0=0. So the kernel contains only the zero vector. S03.1 to S03.3 together prove Lemma L_kernel_det. S05.1 · equivalentBefore \lambda^2-T\lambda+D After \left(\lambda-\tfrac{T}{2}\right)^2-\tfrac{\Delta}{4},\quad \Delta=T^2-4D Conditions: none Rule: distributive · Uses: distributive, frac_rules Leaf basis: distributive + frac_rules + two_nonzero Complete the square: (λ−T/2)²=λ²−Tλ+T²/4 (distributivity, with 2≠0), so (λ−T/2)²−Δ/4=λ²−Tλ+T²/4−(T²−4D)/4=λ²−Tλ+D. S05.2 · impliesBefore \Delta<0 After \left(\lambda-\tfrac{T}{2}\right)^2-\tfrac{\Delta}{4}>0\ \text{for all }\lambda:\ \text{no real root} Conditions: \Delta<0 Rule: square_nonneg · Uses: S05.1, square_nonneg Leaf basis: square_nonneg + order_basics + forall_intro If Δ<0 then −Δ/4>0; also (λ−T/2)²≥0 (square_nonneg), and the sum is positive. So by S05.1, λ²−Tλ+D is greater than 0 for every real λ, and there is no real root. S05.3 · impliesBefore \Delta=0 After \left(\lambda-\tfrac{T}{2}\right)^2=0\iff\lambda=\tfrac{T}{2}:\ \text{exactly one root} Conditions: \Delta=0 Rule: square_nonneg · Uses: S05.1, square_nonneg Leaf basis: square_nonneg + eq_congruence If Δ=0 the equation becomes (λ−T/2)²=0; by square_nonneg (u²=0 ⇔ u=0) this is equivalent to λ=T/2. There is exactly one real root; it is listed once and not counted twice by multiplicity (MKO assumption a3). S05.4 · impliesBefore \Delta>0 After \lambda=\tfrac{T+\sqrt{\Delta}}{2}\ \lor\ \lambda=\tfrac{T-\sqrt{\Delta}}{2},\ \text{two distinct roots} Conditions: \Delta>0 Rule: zero_product · Uses: S05.1, sqrt_def, zero_product Leaf basis: zero_product + sqrt_def + distributive + order_basics If Δ>0 let k=√Δ/2; by sqrt_def k≥0 and k²=Δ/4, and since Δ≠0, k>0. The equation is equivalent to u²−k²=0 with u=λ−T/2, that is (u−k)(u+k)=0; by the zero-product property u=k or u=−k, so λ=(T+√Δ)/2 or λ=(T−√Δ)/2. They differ by 2k>0, so they are distinct, and there are no other real roots. S05.1 to S05.4 together prove Lemma L_disc. ## 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 eigenvectorThe 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 eigenvalueK₃={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 valueThe 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-eigenvalue-01.json)