# 二階行列式：乘積公式、縮放公式與實數域可逆判準 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-determinant/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-determinant-01 · production-20261019-adopted-96 ## 目標與範圍 對所有 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)。 ## 逐步主鏈 S01 · definition操作前 M=\begin{pmatrix}a&b\\c&d\end{pmatrix} 操作後 \det(M)=ad-bc 條件：無 規則：mko_det_def · 依賴：G1 葉節點依據：mko_det_def + def_unfold 寫出 MKO 的定義：主對角線乘積 ad 減去另一條對角線乘積 bc。符號與位置都重要：不能改成 ad+bc，也不能取絕對值（MKO 第一段）。 S02 · equivalent操作前 \det(A),\ \det(B) 操作後 2\cdot 3-1\cdot(-1)=7,\quad 1\cdot 0-(-2)\cdot 4=8 條件：無 規則：numeric_evaluation · 依賴：S01, G2 葉節點依據：numeric_evaluation + neg_mul + mko_det_def det(A)=2·3−1·(−1)=6−(−1)=7：減去一個負的乘積等於加上它的相反數。det(B)=1·0−(−2)·4=0−(−8)=8。 S03 · equivalent操作前 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} 條件：無 規則：matrix_product_def · 依賴：G1, matrix_product_def 葉節點依據：matrix_product_def + def_unfold 依矩陣乘法定義，(AB)(i,j)=Σ_{k=1}^{2}A(i,k)B(k,j)：第 i 行與第 j 列的乘積和。例如 (AB)(1,1)=ae+bg，(AB)(2,2)=cf+dh。 S04 · equivalent操作前 \det(AB)=(ae+bg)(cf+dh)-(af+bh)(ce+dg) 操作後 \det(AB)=(ad-bc)(eh-fg)=\det(A)\det(B) 條件：無 規則：L_det_mul · 依賴：S01, S03, L_det_mul 葉節點依據：L_det_mul + mko_det_def 把 S01 的定義套到 S03 的 AB 上得到左式。依引理 L_det_mul，它等於 det(A)det(B)。引理以展開與比較單項式在 S04.1 到 S04.4 證明，對所有實數 a 到 h 成立，所以對所有 2×2 實矩陣成立。 S05 · implies操作前 AB 操作後 AB=\begin{pmatrix}6&-4\\11&2\end{pmatrix},\ \det(AB)=12+44=56=7\cdot 8 條件：無 規則：numeric_evaluation · 依賴：S02, S03, S04, G2 葉節點依據：numeric_evaluation + matrix_product_def + mko_det_def 依 S03 直接計算：(AB)(1,1)=2·1+1·4=6，(AB)(1,2)=2·(−2)+1·0=−4，(AB)(2,1)=(−1)·1+3·4=11，(AB)(2,2)=(−1)(−2)+3·0=2。det(AB)=6·2−(−4)·11=12+44=56，與 det(A)det(B)=7·8=56 相同。這是以實際乘積重算的核對（MKO 第三段）。 S06 · implies操作前 BA 操作後 BA=\begin{pmatrix}4&-5\\8&4\end{pmatrix}\neq AB,\ \det(BA)=16+40=56 條件：無 規則：matrix_product_def · 依賴：S03, S05, G2 葉節點依據：matrix_product_def + numeric_evaluation BA：(1,1)=1·2+(−2)(−1)=4，(1,2)=1·1+(−2)·3=−5，(2,1)=4·2+0·(−1)=8，(2,2)=4·1+0·3=4。左上角 4≠6，所以 BA≠AB；但 det(BA)=4·4−(−5)·8=56=det(AB)。乘積公式只說行列式相等，並不表示 A、B 可交換（MKO 假設 a3）。 S07 · equivalent操作前 \det(tM),\ tM=\begin{pmatrix}ta&tb\\tc&td\end{pmatrix} 操作後 (ta)(td)-(tb)(tc)=t^2(ad-bc)=t^2\det(M) 條件：無 規則：distributive · 依賴：S01, matrix_alg 葉節點依據：mul_comm + mul_assoc + distributive + power_laws tM 的每個元素乘 t。依定義 det(tM)=(ta)(td)−(tb)(tc)；用乘法交換律與結合律，(ta)(td)=t²ad、(tb)(tc)=t²bc；再用分配律提出 t²。每個乘積含兩個元素，所以出現 t²，而不是 t。 S08 · implies操作前 -3A=\begin{pmatrix}-6&-3\\3&-9\end{pmatrix} 操作後 \det(-3A)=54+9=63=(-3)^2\cdot 7;\ \det(0A)=0 條件：無 規則：numeric_evaluation · 依賴：S02, S07, G2 葉節點依據：numeric_evaluation + mko_det_def 直接算：det(−3A)=(−6)(−9)−(−3)·3=54+9=63；依 S07 應為 (−3)²·7=9·7=63，一致。負的 t 經由 t² 作用，行列式不變號（MKO 假設 a2）。t=0 時 0A 是零矩陣，行列式 0=0²·7。 S09 · equivalent操作前 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 條件：無 規則：matrix_product_def · 依賴：S01, matrix_product_def 葉節點依據：matrix_product_def + neg_mul + mul_comm + add_inverse M·adj(M) 的四個元素：(1,1)=ad+b(−c)=ad−bc，(1,2)=a(−b)+ba=0，(2,1)=cd+d(−c)=0，(2,2)=c(−b)+da=ad−bc。adj(M)·M：(1,1)=da+(−b)c=ad−bc，(1,2)=db+(−b)d=0，(2,1)=(−c)a+ac=0，(2,2)=(−c)b+ad=ad−bc。兩個乘積都等於 det(M)·I。 S10 · implies操作前 \det(M)\neq 0 操作後 X=\tfrac{1}{\det(M)}\operatorname{adj}(M):\ MX=XM=I 條件：\det(M)\neq 0 規則：mul_inverse_nonzero · 依賴：S09, matrix_alg, mul_inverse_nonzero, G3 葉節點依據：mul_inverse_nonzero + matrix_alg + frac_rules 若 det(M)≠0，則 1/det(M) 存在。令 X=(1/det(M))·adj(M)。依 matrix_alg 純量可提出：MX=(1/det(M))·(M·adj(M))=(1/det(M))·det(M)·I=I；同理 XM=I。所以 M 在 ℝ 上可逆。 S11 · implies操作前 MX=XM=I 操作後 \det(M)\det(X)=\det(I)=1\ \Rightarrow\ \det(M)\neq 0 條件：無 規則：contradiction · 依賴：S04, matrix_alg, G3 葉節點依據：L_det_mul + mul_zero + contradiction + numeric_evaluation 設 M 在 ℝ 上可逆，MX=I。依 L_det_mul，det(M)det(X)=det(MX)=det(I)=1·1−0·0=1。若 det(M)=0，左邊是 0·det(X)=0，得 0=1，矛盾。所以 det(M)≠0。 S12 · implies操作前 \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 條件：無 規則：iff_intro · 依賴：S10, S11, G2 葉節點依據：iff_intro + numeric_evaluation S10、S11 兩個方向合起來得到實數域可逆判準。例如 D=[[2,4],[1,2]] 的行列式 2·2−4·1=0，所以 D 在 ℝ 上不可逆；確實 D(2,−1)ᵀ=(0,0)ᵀ，非零向量被送到零，不能還原。 S13 · implies操作前 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 條件：\det(A)=7\neq 0 規則：mul_inverse_nonzero · 依賴：S02, S09, S10, G2 葉節點依據：mul_inverse_nonzero + matrix_product_def + numeric_evaluation det(A)=7≠0，依 S10，A⁻¹=(1/7)adj(A)，adj(A)=[[3,−1],[1,2]]。直接核對 A·adj(A)：(1,1)=2·3+1·1=7，(1,2)=2·(−1)+1·2=0，(2,1)=(−1)·3+3·1=0，(2,2)=(−1)(−1)+3·2=7，所以乘以 1/7 後是 I。A⁻¹ 的元素 3/7、−1/7、1/7、2/7 都不是整數。 S14 · implies操作前 AY=YA=I,\ Y\ \text{with integer entries}\ ? 操作後 Y=A^{-1}\ \text{and}\ \tfrac{3}{7}\notin\mathbb{Z}\ \Rightarrow\ \text{no integer inverse} 條件：無 規則：contradiction · 依賴：S13, matrix_alg, G3 葉節點依據：matrix_alg + contradiction + divides_def 反矩陣唯一：若 X=A⁻¹ 且 Y 也滿足 AY=YA=I，則依 matrix_alg 的結合律 X=XI=X(AY)=(XA)Y=IY=Y。所以任何反矩陣都等於 A⁻¹，其 (1,1) 元素是 3/7，不是整數（7 不整除 3）。因此 A 沒有整數反矩陣，雖然 A 的元素都是整數且 det(A)=7≠0。實數域的「非零即可逆」不能原樣搬到整數環（MKO 假設 a1）。 S15 · implies操作前 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} 條件：無 規則：iff_intro · 依賴：S10, S12, G2 葉節點依據：iff_intro + mul_inverse_nonzero + numeric_evaluation det(C)=1·4−2·3=−2，是負數但非零，依 S12 C 可逆；依 S10，C⁻¹=(1/(−2))·[[4,−2],[−3,1]]=[[−2,1],[3/2,−1/2]]。核對 C·C⁻¹：(1,1)=1·(−2)+2·(3/2)=1，(1,2)=1·1+2·(−1/2)=0，(2,1)=3·(−2)+4·(3/2)=0，(2,2)=3·1+4·(−1/2)=1。非零行列式包含正與負，不必等於一（MKO 第一段）。 S16 · implies操作前 \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 條件：無 規則：and_intro_elim · 依賴：S04, S05, S06, S07, S08, S12, S13, S14, S15 葉節點依據：and_intro_elim 合併：乘積公式與縮放公式對所有 2×2 實矩陣成立（S04、S07）；例中 det(AB)=det(BA)=56 但 AB≠BA（S05、S06），det(−3A)=63（S08）；實數域可逆 ⇔ det≠0（S12）；A⁻¹=(1/7)[[3,−1],[1,2]] 不是整數矩陣（S13、S14）；det(C)=−2 的 C 可逆（S15）。 ## 局部子步與引理 S04.1 · equivalent操作前 (ae+bg)(cf+dh) 操作後 acef+adeh+bcfg+bdgh 條件：無 規則：distributive · 依賴：distributive, mul_comm, mul_assoc 葉節點依據：distributive + mul_comm + mul_assoc 用分配律展開成四個乘積：ae·cf、ae·dh、bg·cf、bg·dh；再用乘法交換律與結合律把每個單項式的字母依字母序排列，得 acef、adeh、bcfg、bdgh。 S04.2 · equivalent操作前 (af+bh)(ce+dg) 操作後 acef+adfg+bceh+bdgh 條件：無 規則：distributive · 依賴：distributive, mul_comm, mul_assoc 葉節點依據：distributive + mul_comm + mul_assoc 同樣展開：af·ce=acef、af·dg=adfg、bh·ce=bceh、bh·dg=bdgh。 S04.3 · equivalent操作前 (acef+adeh+bcfg+bdgh)-(acef+adfg+bceh+bdgh) 操作後 adeh+bcfg-adfg-bceh 條件：無 規則：add_inverse · 依賴：S04.1, S04.2 葉節點依據：add_inverse + add_comm + add_assoc + distributive 相減時 acef 與 bdgh 兩項各出現在兩個展開式中，互相抵消（u−u=0）；剩下 adeh+bcfg−adfg−bceh。 S04.4 · equivalent操作前 (ad-bc)(eh-fg) 操作後 adeh-adfg-bceh+bcfg 條件：無 規則：distributive · 依賴：S04.3, distributive 葉節點依據：distributive + neg_mul + mul_comm + mul_assoc 展開右邊：ad·eh=adeh，ad·(−fg)=−adfg，(−bc)·eh=−bceh，(−bc)(−fg)=bcfg（neg_mul）。與 S04.3 的四項逐項相同，所以 det(AB)=det(A)det(B)。S04.1 到 S04.4 合起來證得引理 L_det_mul。 ## 逐步反向審查 - 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-determinant-01.json)