二階實矩陣的特徵值：特徵多項式、判別式與非零特徵向量

目標與範圍

對 2×2 實矩陣證明：λ 是實特徵值 ⇔ det(M−λI)=0 ⇔ λ²−tr(M)λ+det(M)=0，且互異實特徵值的個數由 Δ=tr(M)²−4det(M) 的正負決定（負、零、正分別為 0、1、2）。以 M=[[4,1],[2,3]] 求出全部互異實特徵值與各自的非零特徵向量，說明候選 λ=3 的核 K₃={0} 而 3 不是特徵值，並拒絕候選特徵對 (3,0)；再以旋轉矩陣 R=[[0,−1],[1,0]]（Δ<0）與 J=[[3,1],[0,3]]（Δ=0）對照。

只在 MKO 範圍內：實數域、2×2 方陣、非零特徵向量慣例。完整證明核非零 ⇔ 行列式為零、特徵多項式公式與判別式分類；行列式非零 ⇒ 可逆引用行列式條目。不處理代數重數、特徵基底、對角化、Jordan 結構或複數譜，也不做 Lean 的 HasEigenvector 橋接；不改動 canonical MKO 或英文 edition。

已知條件與符號

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

• G1 — 全程在實數域，M=[[a,b],[c,d]] 為 2×2 實矩陣，向量為 ℝ² 的列向量；I=[[1,0],[0,1]]（MKO 假設 a1）。
• G2 — 例子：M=[[4,1],[2,3]]；候選值 λ=3；候選特徵對 (3,0)。
• G3 — 對照：R=[[0,−1],[1,0]]，J=[[3,1],[0,3]]。

• \lambda — 候選實數特徵值
• K_\lambda=\{v\mid Mv=\lambda v\} — 候選 λ 的核，恆含零向量
• \operatorname{tr}(M) — 跡 a+d
• \Delta — 判別式 tr(M)²−4det(M)
• N=\begin{pmatrix}p&q\\r&s\end{pmatrix} — 引理中的一般 2×2 實矩陣

規則與來源

• matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
• sqrt_def · prerequisite — 主平方根：對 a≥0，√a 是唯一滿足 b≥0 且 b²=a 的實數 b。負數在實數中沒有平方根。
• zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
• two_nonzero · prerequisite — 實數中 0<1，故 0<1+1=2，所以 2≠0。
• order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_eig_def · cited — 對2×2實矩陣 M，實數 λ 是特徵值當且僅當存在非零 v∈R² 使 Mv=λv。本輪採非零特徵向量慣例；候選 λ 的核 Kλ={v:Mv=λv} 仍包含零向量，即使 λ 並非特徵值。互異實特徵值是 λ²−tr(M)λ+det(M)=0 的互異實根。 · mko-eigenvalue
• mko_det_inv · cited — 對實矩陣 M=[[a,b],[c,d]]，本輪 D(M)=det(M)=ad−bc。M 在實數域可逆當且僅當 det(M)≠0；對同為2×2的實矩陣 A、B，det(AB)=det(A)det(B)，且 det(tM)=t²det(M)。 · mko-determinant
• vec_ops · prerequisite — ℝ² 的列向量逐分量相加與數乘；兩向量相等 ⇔ 兩個分量分別相等；零向量 0=(0,0)ᵀ，v≠0 ⇔ 至少一個分量非零。
• L_kernel_det · lemma — 對 2×2 實矩陣 N：存在非零 v 使 Nv=0 ⇔ det(N)=0。
• L_disc · lemma — 對實數 T、D，令 Δ=T²−4D。方程 λ²−Tλ+D=0 的互異實根個數：Δ<0 時為 0；Δ=0 時為 1（λ=T/2）；Δ>0 時為 2（λ=(T±√Δ)/2）。

逐步主鏈

\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\}

局部子步與引理

\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}

逐步反向審查

• S13 · sufficient_goal_reduction · S03, S05, S06, S07, S08, S09, S10, S11, S12 — 目標 G：題目要求的各項。足夠條件 H：S03 到 S12 的結論；H⇒G 只用合取。H 由 G1 到 G3 正向推出，沒有把 G 當作前提。
• S12 · premise_audit · S03, L_disc, numeric_evaluation — 只宣稱互異實特徵值的個數為 1；不建立代數重數或特徵基底。
• S11 · premise_audit · S03, L_disc, square_nonneg — 本稿只在實數域工作，不討論複數特徵值。
• S10 · premise_audit · S01, mko_eig_def — 拒絕的理由只是 v=0；核會員與特徵對是兩個不同的問題。
• S09 · premise_audit · S02, S03, eq_congruence, mul_inverse_nonzero — 直接解方程與行列式判準兩種方法一致（N16、N17）。核中有零向量不構成特徵值。
• S08 · premise_audit · S02, exists_intro, numeric_evaluation — 直接計算（N13 到 N15）確認；特徵向量不唯一，任何非零倍數也可以。
• S07 · premise_audit · S02, exists_intro, numeric_evaluation — 特徵值只需找到一個非零向量；直接計算 Mv（N11、N12）獨立確認。
• S06 · inverse_equivalence · sqrt_def, zero_product, numeric_evaluation — 分解式與零乘積性質雙向給出同樣兩根（N7 到 N10）。
• S05.4 · premise_audit · S05.1, sqrt_def, zero_product, distributive — 零乘積性質是雙向的，所以這兩個值確實是根，且只有它們；不要求 Δ 是完全平方（MKO 第三段）。
• S05.3 · premise_audit · S05.1, square_nonneg — u²=0 ⇔ u=0 兩向都成立，所以根存在且唯一。
• S05.2 · premise_audit · S05.1, square_nonneg, order_basics — 結論是對所有實數 λ；論證沒有對 λ 加任何假設。
• S05.1 · inverse_equivalence · distributive, frac_rules, two_nonzero — 對所有實數 λ、T、D 成立的恆等式（N4），雙向成立。
• S05 · premise_audit · S03, S04, L_disc — 需要 S03 的等價把特徵值問題化為求根問題；引理只計互異根，不計重數。
• S04 · inverse_equivalence · distributive, neg_mul, add_comm — 多項式恆等式（N1），雙向成立。
• S03.3 · premise_audit · mko_det_inv, contrapositive, vec_ops — 依賴行列式條目的實數域可逆判準與矩陣乘法結合律；N⁻¹0=0 是每個分量乘零之和。
• S03.2 · premise_audit · S03.1, case_analysis, matrix_product_def — 三種情況（第一行非零、第一行為零但第二行非零、全零）窮盡所有可能。
• S03.1 · premise_audit · matrix_product_def, vec_ops, neg_mul — 第二分量為零正是用到 det N=0；第一行不全為零保證 v≠0。
• S03 · inverse_equivalence · L_kernel_det, S02 — 引理兩個方向都有證明（S03.1、S03.2 為 ⇐，S03.3 為 ⇒）。
• S02 · inverse_equivalence · distributive, vec_ops, add_inverse — 兩邊同減 λv 或同加 λv，互為反運算，雙向成立。
• S01 · premise_audit · G1, mko_eig_def — 此步只寫出定義，不推出新事實。

錯誤控制與反例

零向量不是特徵向量

MKO 的第一個誤解是把零向量當特徵向量。M0=λ0 對每個 λ 都成立；若允許 v=0，每個實數都會是「特徵值」。所以 (3,0) 必須拒絕（S10），而 3 確實不是特徵值（S09）。

核含零不等於特徵值存在

K₃={0} 非空，但只含零向量；特徵值要求核中有非零向量。核會員題接受零向量，特徵對題拒絕零向量，兩類問題要分開（MKO 假設 a2）。

二重根只算一個互異值

J 的特徵多項式 (λ−3)² 有二重根 3，但互異實特徵值只有一個（S12）。把它按重數算成兩個互異值是 MKO 列出的誤解。

• M·0=3·0，所以 3 是 M 的特徵值 → reject — 需要非零向量；K₃={0}，det(M−3I)=−2≠0。
• K₃ 非空，所以 3 是特徵值 → reject — K₃ 只含零向量；每個 λ 的核都含零向量。
• J=[[3,1],[0,3]] 有兩個互異實特徵值，因為特徵多項式是二次 → reject — Δ=0，唯一的根是 3；互異值只有一個。
• 每個 2×2 實矩陣都至少有一個實特徵值 → reject — R=[[0,−1],[1,0]] 的特徵多項式 λ²+1 沒有實根。

結論與限制

對 2×2 實矩陣，λ 是實特徵值 ⇔ det(M−λI)=0 ⇔ λ²−tr(M)λ+det(M)=0；互異實特徵值個數在 Δ<0、Δ=0、Δ>0 時分別為 0、1、2。M=[[4,1],[2,3]] 的互異實特徵值為 {2,5}，特徵向量 (1,−2)ᵀ、(1,1)ᵀ；K₃={0}，3 不是特徵值，(3,0) 不是特徵對。R 無實特徵值（Δ=−4），J 只有 3（Δ=0）。

• S03.3 引用行列式條目的「det≠0 ⇒ 在 ℝ 上可逆」與矩陣乘法結合律；它們在本稿中未重新證明。
• 代數重數、特徵基底、一般對角化與複數譜不在本稿範圍；MKO 的 formal next（HasEigenvector／eigenspace 綁定）未做。

驗證及來源綁定

25 個本稿宣告算術檢查；只支持所列算式。

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

同源完整 JSON（含公式、AST、反控制與修訂記錄）