二階行列式：乘積公式、縮放公式與實數域可逆判準

目標與範圍

對所有 2×2 實矩陣證明 det(AB)=det(A)det(B) 與 det(tM)=t²det(M)，並證明 M 在實數域可逆當且僅當 det(M)≠0。以 A=[[2,1],[−1,3]]、B=[[1,−2],[4,0]] 核對乘積公式並顯示 AB≠BA；以 t=−3 核對縮放公式；求 A⁻¹，並說明 A 雖是整數矩陣且 det(A)=7≠0，卻沒有整數反矩陣；以 C=[[1,2],[3,4]]（det=−2）說明非零行列式不必為正。

只在 MKO 範圍內：2×2 方陣、實數域、通常的行乘列矩陣乘積。完整證明乘積公式、縮放公式與實數域可逆判準；不處理高階行列式、一般環上的可逆判準，也不做 Lean 的 det_fin_two 橋接；不改動 canonical MKO 或英文 edition。

已知條件與符號

• distributive
• mul_comm
• mul_assoc
• matrix_product_def
• mul_inverse_nonzero
• numeric_evaluation

• G1 — 所有矩陣是 2×2 實矩陣，數域是 ℝ；AB 是通常的行乘列乘積，不是逐項乘積（MKO 假設 a1、a3）。
• G2 — 例子：A=[[2,1],[−1,3]]，B=[[1,−2],[4,0]]，t=−3，C=[[1,2],[3,4]]，D=[[2,4],[1,2]]（每個內層括號是一行）。
• G3 — M 在 ℝ 上可逆，指存在實矩陣 X 使 MX=XM=I；「整數反矩陣」指這樣的 X 的元素全為整數。

• \det(M) — 2×2 矩陣 M=[[a,b],[c,d]] 的行列式 ad−bc
• AB — 行乘列的矩陣乘積
• tM — 純量 t 乘矩陣 M
• \operatorname{adj}(M) — 伴隨矩陣 [[d,−b],[−c,a]]
• I — 2×2 單位矩陣

規則與來源

• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
• matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
• 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）。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
• divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_det_def · 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
• matrix_alg · prerequisite — 2×2 矩陣乘法結合：(XY)Z=X(YZ)；I=[[1,0],[0,1]] 滿足 IX=XI=X；純量可提出：X(kY)=(kX)Y=k(XY)；tM 是每個元素乘 t。
• L_det_mul · lemma — 對所有 2×2 實矩陣 A、B：det(AB)=det(A)det(B)。

逐步主鏈

M=\begin{pmatrix}a&b\\c&d\end{pmatrix}

\det(M)=ad-bc

\det(A),\ \det(B)

2\cdot 3-1\cdot(-1)=7,\quad 1\cdot 0-(-2)\cdot 4=8

A=\begin{pmatrix}a&b\\c&d\end{pmatrix},\ B=\begin{pmatrix}e&f\\g&h\end{pmatrix}

AB=\begin{pmatrix}ae+bg&af+bh\\ce+dg&cf+dh\end{pmatrix}

\det(AB)=(ae+bg)(cf+dh)-(af+bh)(ce+dg)

\det(AB)=(ad-bc)(eh-fg)=\det(A)\det(B)

AB

AB=\begin{pmatrix}6&-4\\11&2\end{pmatrix},\ \det(AB)=12+44=56=7\cdot 8

BA

BA=\begin{pmatrix}4&-5\\8&4\end{pmatrix}\neq AB,\ \det(BA)=16+40=56

\det(tM),\ tM=\begin{pmatrix}ta&tb\\tc&td\end{pmatrix}

(ta)(td)-(tb)(tc)=t^2(ad-bc)=t^2\det(M)

-3A=\begin{pmatrix}-6&-3\\3&-9\end{pmatrix}

\det(-3A)=54+9=63=(-3)^2\cdot 7;\ \det(0A)=0

M\,\operatorname{adj}(M),\ \operatorname{adj}(M)\,M,\ \operatorname{adj}(M)=\begin{pmatrix}d&-b\\-c&a\end{pmatrix}

\begin{pmatrix}ad-bc&0\\0&ad-bc\end{pmatrix}=\det(M)\,I

\det(M)\neq 0

X=\tfrac{1}{\det(M)}\operatorname{adj}(M):\ MX=XM=I

MX=XM=I

\det(M)\det(X)=\det(I)=1\ \Rightarrow\ \det(M)\neq 0

\det(M)\neq 0\Rightarrow\text{invertible},\ \text{invertible}\Rightarrow\det(M)\neq 0

M\ \text{invertible over }\mathbb{R}\iff\det(M)\neq 0;\ \det(D)=2\cdot 2-4\cdot 1=0

A^{-1}

A^{-1}=\tfrac{1}{7}\begin{pmatrix}3&-1\\1&2\end{pmatrix},\ A\cdot\tfrac{1}{7}\begin{pmatrix}3&-1\\1&2\end{pmatrix}=\tfrac{1}{7}\begin{pmatrix}7&0\\0&7\end{pmatrix}=I

AY=YA=I,\ Y\ \text{with integer entries}\ ?

Y=A^{-1}\ \text{and}\ \tfrac{3}{7}\notin\mathbb{Z}\ \Rightarrow\ \text{no integer inverse}

C=\begin{pmatrix}1&2\\3&4\end{pmatrix}

\det(C)=-2\neq 0,\ C^{-1}=\begin{pmatrix}-2&1\\ \tfrac{3}{2}&-\tfrac{1}{2}\end{pmatrix}

\text{tasks of the goal}

\det(AB)=\det A\det B,\ \det(tM)=t^2\det M,\ \text{invertible over }\mathbb{R}\iff\det\neq 0

局部子步與引理

(ae+bg)(cf+dh)

acef+adeh+bcfg+bdgh

(af+bh)(ce+dg)

acef+adfg+bceh+bdgh

(acef+adeh+bcfg+bdgh)-(acef+adfg+bceh+bdgh)

adeh+bcfg-adfg-bceh

(ad-bc)(eh-fg)

adeh-adfg-bceh+bcfg

逐步反向審查

• S16 · sufficient_goal_reduction · S04, S05, S06, S07, S08, S12, S13, S14, S15 — 目標 G：題目要求的各項。足夠條件 H：S04 到 S15 的結論；H⇒G 只用合取。H 由 G1 到 G3 正向推出，沒有把 G 當作前提。
• S15 · premise_audit · S12, numeric_evaluation — 依賴判準與數值核對（N24 到 N28）。
• S14 · premise_audit · S13, matrix_alg, contradiction, divides_def — 需要反矩陣唯一（結合律）與 3/7 不是整數；不宣稱整數環上的一般可逆判準。
• S13 · premise_audit · S10, numeric_evaluation — 數值核對（N20 到 N23）確認 A·A⁻¹=I；A⁻¹·A=I 由 S09、S10 的一般論證保證。
• S12 · premise_audit · S10, S11, iff_intro — 兩個方向各有證明；D 的例子只是說明，不參與證明。
• S11 · premise_audit · L_det_mul, mul_zero, contradiction — 這是「可逆 ⇒ det≠0」方向，只用到乘積公式與 det(I)=1。
• S10 · premise_audit · S09, mul_inverse_nonzero, matrix_alg — 關鍵是除以 det(M)，需要 det(M)≠0 且在可做除法的 ℝ 中；這是「det≠0 ⇒ 可逆」方向。
• S09 · inverse_equivalence · matrix_product_def, neg_mul, mul_comm — 每個元素都是恆等式（N18、N19），雙向成立。
• S08 · premise_audit · S07, numeric_evaluation — 兩種算法（直接與公式）一致（N16、N17），只核對本例。
• S07 · inverse_equivalence · mul_comm, mul_assoc, distributive — 對所有實數 t、a、b、c、d 成立的恆等式（N15），雙向成立。
• S06 · premise_audit · matrix_product_def, numeric_evaluation — 一個不相等的元素就足以推出 BA≠AB。
• S05 · premise_audit · S03, S04, numeric_evaluation — 有限計算只核對本例（N3 到 N8），不取代 S04 的一般證明。
• S04.4 · inverse_equivalence · distributive, neg_mul, mul_comm — 恆等式，雙向成立；N14 在格點上核對同一多項式恆等式。
• S04.3 · inverse_equivalence · add_inverse, add_comm, add_assoc — 加法反元素與重排都是恆等式，雙向成立。
• S04.2 · inverse_equivalence · distributive, mul_comm, mul_assoc — 恆等式，雙向成立。
• S04.1 · inverse_equivalence · distributive, mul_comm, mul_assoc — 所用的都是恆等式，雙向成立。
• S04 · inverse_equivalence · L_det_mul, eq_refl_symm_trans — 兩邊是對所有實數成立的多項式恆等式（N14），等號雙向。
• S03 · inverse_equivalence · matrix_product_def — 這是定義展開，四個位置逐一相等，雙向成立。
• S02 · inverse_equivalence · numeric_evaluation, neg_mul — 精確整數計算（N1、N2），雙向成立。
• S01 · premise_audit · G1, mko_det_def — 此步只寫出定義，不推出新事實。

錯誤控制與反例

非零不必為正

MKO 的誤解之一是以為可逆需要正的行列式。det(C)=−2<0，但 C 可逆，反矩陣在 S15 明確寫出。判準是 det≠0，不是 det>0，也不是 det=1。

AB 不是逐項乘積

A 與 B 的逐項乘積是 [[2,−2],[−4,0]]，行列式 2·0−(−2)(−4)=−8，不是 56。乘積公式只對行乘列的 AB 成立；而且它不表示 AB=BA（S06）。

可逆判準依賴數域

在 ℝ 上 det(A)=7≠0 足以可逆；但 A⁻¹ 的元素是 3/7 等分數，而反矩陣唯一，所以 A 沒有整數反矩陣（S14）。忽略數域是 MKO 列出的誤解。

• det(C)=−2<0，所以 C 不可逆 → reject — 判準是 det≠0；C⁻¹=[[−2,1],[3/2,−1/2]] 存在。
• 逐項乘積 [[2,−2],[−4,0]] 的行列式等於 det(A)det(B) → reject — 它的行列式是 −8，而 det(A)det(B)=56。
• det(AB)=det(BA)，所以 AB=BA → reject — AB 的左上角是 6，BA 的左上角是 4。
• det(−3A)=−3·det(A)=−21 → reject — 2×2 時 det(tM)=t²det(M)，所以是 9·7=63。
• A 的元素是整數且 det(A)=7≠0，所以 A 有整數反矩陣 → reject — 唯一的反矩陣 (1/7)[[3,−1],[1,2]] 含非整數 3/7。

結論與限制

對所有 2×2 實矩陣，det(AB)=det(A)det(B)、det(tM)=t²det(M)，且 M 在 ℝ 上可逆當且僅當 det(M)≠0。例中 det(A)=7、det(B)=8、det(AB)=det(BA)=56 而 AB≠BA；det(−3A)=63；A⁻¹=(1/7)[[3,−1],[1,2]]，A 沒有整數反矩陣；det(C)=−2，C 可逆。

• 本稿只處理 2×2；高階行列式與整數環上的一般可逆判準不在範圍內。
• matrix_alg（矩陣乘法結合、單位矩陣、純量可提出）作為前提使用，未在本稿逐項證明。
• MKO 的 formal next（det_fin_two、det_mul、det_smul 與實數域 inverse 的橋接）未做。

驗證及來源綁定

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

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

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