# 矩陣：尺寸、一起算索引、逐項加法與轉置

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-matrix/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-matrix-01 · production-20261019-adopted-96



## 目標與範圍

設 M=[[2,−1,0],[5,3,7]]、N=[[1,4,−2],[0,−3,6]]（每個內層括號是一行，row）。求兩者尺寸，讀出 M(1,2)、M(2,3)，判定 M(3,1) 是否存在；求 M+N、Mᵀ、Nᵀ；對任意同尺寸實矩陣證明 (A+B)ᵀ=Aᵀ+Bᵀ 與 (Aᵀ)ᵀ=A，並在 M、N 上核對；說明 M+Mᵀ 無定義；最後以反例區分轉置與「逐行倒序」及「反矩陣」，並把程式的零起算索引對應回一起算索引。

只在 MKO 的範圍內：實矩陣、正的行數與列數（1 到 5）、外部索引從 1 開始、同尺寸逐項加法與轉置。完整證明轉置與加法相容及二次轉置還原；矩陣乘法只在一個反例中用來說明轉置不是反矩陣。不處理零維矩陣、行列式、一般可逆性，也不做 Lean 的 Fin 索引橋接；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- numeric_evaluation
- function_def
- add_comm
- forall_intro


- G1 — 約定：實矩陣；外部行列索引從 1 開始；每邊尺寸 1 至 5，各行等長且非空；M、N 等具體例子的元素為整數（MKO 假設 a1、a2），一般轉置恆等式則對實數元素證明。
- G2 — M 的兩行為 (2,−1,0) 與 (5,3,7)；N 的兩行為 (1,4,−2) 與 (0,−3,6)。
- G3 — 某程式以零起算陣列 a 逐行儲存 M：a[i][j]，0≤i≤1、0≤j≤2。另有方陣 S 的兩行為 (1,2) 與 (3,4)，只用於反例。


- M(i,j) — 第 i 行（row）第 j 列（column）的元素；MKO 用語中「行」指 row、「列」指 column
- m\times n — m 行 n 列的尺寸
- M^{\mathsf T} — M 的轉置
- a[i][j] — 程式中零起算的陣列索引
- A,B — 任意同尺寸實矩陣





## 規則與來源


- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- 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。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_matrix_def · cited — m×n 實矩陣 M 是以行 i 與列 j 指定的實數表，m、n 為正整數。本輪外部索引從1開始，M(i,j) 是第i行第j列元素。同尺寸矩陣逐項相加；轉置 Mᵀ 的尺寸是 n×m，並把 M(i,j) 放到 Mᵀ(j,i)。 · mko-matrix
- matrix_eq · prerequisite — 兩矩陣相等 ⇔ 尺寸相同，且在每個合法索引 (i,j) 上元素相等。
- L_transpose_sum · lemma — 對任意 m×n 實矩陣 A、B：(A+B)ᵀ=Aᵀ+Bᵀ。
- L_double_transpose · lemma — 對任意 m×n 實矩陣 A：(Aᵀ)ᵀ=A。





## 逐步主鏈

S01 · definition操作前

M\in\mathbb{R}^{m\times n}

操作後

M(i,j)\ (1\le i\le m,\ 1\le j\le n);\ (A+B)(i,j)=A(i,j)+B(i,j);\ M^{\mathsf T}(j,i)=M(i,j)

條件：m,n\ge 1

規則：mko_matrix_def · 依賴：G1

葉節點依據：mko_matrix_def + def_unfold

寫出 MKO 的定義：矩陣是由兩個索引指定的實數表，第一個索引是行（row）、第二個是列（column），都從 1 開始。加法只對同尺寸矩陣定義，逐項相加；轉置 Mᵀ 是 n×m，把 M(i,j) 放到位置 (j,i)。



S02 · implies操作前

M=\begin{pmatrix}2&-1&0\\5&3&7\end{pmatrix},\ N=\begin{pmatrix}1&4&-2\\0&-3&6\end{pmatrix}

操作後

M,N\in\mathbb{R}^{2\times 3}

條件：無

規則：mko_matrix_def · 依賴：S01, G2

葉節點依據：mko_matrix_def + numeric_evaluation

M 有 2 行，每行都有 3 個元素（各行等長、非空），所以 M 是 2×3，共 2·3=6 個元素；N 同樣是 2×3。尺寸先寫行數再寫列數，2×3 與 3×2 是不同尺寸。



S03 · equivalent操作前

M(1,2),\ M(2,3),\ M(2,1)

操作後

M(1,2)=-1,\ M(2,3)=7,\ M(2,1)=5

條件：1\le i\le 2; 1\le j\le 3

規則：def_unfold · 依賴：S01, S02

葉節點依據：def_unfold + mko_matrix_def

M(1,2) 是第 1 行第 2 個元素 −1；M(2,3) 是第 2 行第 3 個元素 7；M(2,1) 是第 2 行第 1 個元素 5。M(1,2)≠M(2,1)：兩個索引的次序有意義，先行後列。



S04 · implies操作前

M(3,1)

操作後

(3,1)\ \text{is not a legal index of } M

條件：無

規則：mko_matrix_def · 依賴：S01, S02

葉節點依據：mko_matrix_def + order_basics

M 只有 2 行，合法的行索引是 1≤i≤2。3>2，所以 M(3,1) 沒有定義；它不是 0，也不是「最後一行」。取元素前兩個索引都必須落在合法範圍（MKO 第二段）。



S05 · implies操作前

M,N\in\mathbb{R}^{2\times 3}

操作後

M+N\ \text{defined},\ M+N\in\mathbb{R}^{2\times 3}

條件：\dim M=\dim N

規則：mko_matrix_def · 依賴：S01, S02

葉節點依據：mko_matrix_def

加法前先驗尺寸（MKO 假設 a3）：M 與 N 都是 2×3，所以 M+N 有定義，而且也是 2×3。



S06 · equivalent操作前

M+N

操作後

\begin{pmatrix}2+1&-1+4&0+(-2)\\5+0&3+(-3)&7+6\end{pmatrix}=\begin{pmatrix}3&3&-2\\5&0&13\end{pmatrix}

條件：無

規則：mko_matrix_def · 依賴：S05, G2

葉節點依據：mko_matrix_def + numeric_evaluation + matrix_eq

逐項相加：同一位置 (i,j) 的兩個元素相加，共 6 個位置。例如 (M+N)(2,3)=7+6=13，(M+N)(2,2)=3+(−3)=0。



S07 · equivalent操作前

M^{\mathsf T}

操作後

\begin{pmatrix}2&5\\-1&3\\0&7\end{pmatrix}\in\mathbb{R}^{3\times 2}

條件：無

規則：mko_matrix_def · 依賴：S01, S02, S03

葉節點依據：mko_matrix_def + matrix_eq

Mᵀ 是 3×2，Mᵀ(j,i)=M(i,j)：Mᵀ 的第 j 行就是 M 的第 j 列。M 的三列是 (2,5)、(−1,3)、(0,7)，所以 Mᵀ 的三行就是它們。核對：Mᵀ(3,2)=M(2,3)=7，Mᵀ(2,1)=M(1,2)=−1。



S08 · equivalent操作前

N^{\mathsf T}

操作後

\begin{pmatrix}1&0\\4&-3\\-2&6\end{pmatrix}\in\mathbb{R}^{3\times 2}

條件：無

規則：mko_matrix_def · 依賴：S01, S02, G2

葉節點依據：mko_matrix_def + matrix_eq

同理，Nᵀ 的三行是 N 的三列 (1,0)、(4,−3)、(−2,6)。



S09 · theorem_application操作前

(M+N)^{\mathsf T}

操作後

M^{\mathsf T}+N^{\mathsf T}

條件：M,N\in\mathbb{R}^{2\times 3}

規則：L_transpose_sum · 依賴：S05, L_transpose_sum

葉節點依據：L_transpose_sum

M、N 同為 2×3，依引理 L_transpose_sum（A=M、B=N），(M+N)ᵀ=Mᵀ+Nᵀ。引理對所有同尺寸實矩陣在 S09.1、S09.2 證明；S10 再以數字核對本例。



S10 · implies操作前

(M+N)^{\mathsf T},\ M^{\mathsf T}+N^{\mathsf T}

操作後

\begin{pmatrix}3&5\\3&0\\-2&13\end{pmatrix}=\begin{pmatrix}2+1&5+0\\-1+4&3+(-3)\\0+(-2)&7+6\end{pmatrix}

條件：無

規則：numeric_evaluation · 依賴：S06, S07, S08, S09

葉節點依據：numeric_evaluation + matrix_eq

直接轉置 S06 的 M+N，三行是 (3,5)、(3,0)、(−2,13)；把 S07、S08 逐項相加也得到同樣的 3×2 矩陣。這是對本例的數值核對，與 S09 的一般結論一致；一般結論的根據是 S09.2，不是這次計算。



S11 · theorem_application操作前

(M^{\mathsf T})^{\mathsf T}

操作後

M

條件：無

規則：L_double_transpose · 依賴：S07, L_double_transpose

葉節點依據：L_double_transpose

依引理 L_double_transpose，(Mᵀ)ᵀ=M：把 S07 的 3×2 矩陣再轉置，三行 (2,5)、(−1,3)、(0,7) 變回三列，得到原本的 2×3 矩陣 M。引理在 S11.1 證明。



S12 · implies操作前

M+M^{\mathsf T},\ M\in\mathbb{R}^{2\times 3},\ M^{\mathsf T}\in\mathbb{R}^{3\times 2}

操作後

M+M^{\mathsf T}\ \text{undefined}

條件：2\neq 3

規則：mko_matrix_def · 依賴：S02, S07, S05

葉節點依據：mko_matrix_def + numeric_evaluation

M 是 2×3，Mᵀ 是 3×2；因為 2≠3，兩者尺寸不同，逐項加法無法讓所有位置完整配對（例如 M(1,3) 存在，但 Mᵀ(1,3) 不存在），所以 M+Mᵀ 沒有定義。只有方陣（m=n）的轉置才保持尺寸。



S13 · implies操作前

R=\begin{pmatrix}5&3&7\\2&-1&0\end{pmatrix}\ \text{(rows of } M\text{ reversed)}

操作後

R\in\mathbb{R}^{2\times 3},\ M^{\mathsf T}\in\mathbb{R}^{3\times 2}\ \Rightarrow\ R\neq M^{\mathsf T}

條件：無

規則：matrix_eq · 依賴：S07, G2, matrix_eq

葉節點依據：matrix_eq

把 M 的兩行倒序得到 R，R 仍是 2×3；Mᵀ 是 3×2。尺寸不同，依 matrix_eq，R≠Mᵀ。轉置交換的是行與列的角色，不是行的先後次序（MKO 假設 a3）。



S14 · implies操作前

S=\begin{pmatrix}1&2\\3&4\end{pmatrix},\ S^{\mathsf T}=\begin{pmatrix}1&3\\2&4\end{pmatrix}

操作後

SS^{\mathsf T}=\begin{pmatrix}5&11\\11&25\end{pmatrix}\neq I

條件：無

規則：matrix_product_def · 依賴：G3, matrix_product_def, matrix_eq

葉節點依據：matrix_product_def + matrix_eq + numeric_evaluation

若 Sᵀ 是 S 的反矩陣，SSᵀ 必須是單位矩陣 I。依矩陣乘法定義：(SSᵀ)(1,1)=1·1+2·2=5，(SSᵀ)(1,2)=1·3+2·4=11，(SSᵀ)(2,1)=3·1+4·2=11，(SSᵀ)(2,2)=3·3+4·4=25。左上角 5≠1，所以 SSᵀ≠I，Sᵀ 不是 S 的反矩陣。轉置只搬動元素，對每個矩陣都有定義；反矩陣是另一個概念。



S15 · implies操作前

a[i][j],\ 0\le i\le 1,\ 0\le j\le 2

操作後

a[i][j]=M(i+1,\,j+1);\ a[1][2]=M(2,3)=7

條件：無

規則：function_def · 依賴：G3, S03, function_def

葉節點依據：function_def + numeric_evaluation

零起算陣列逐行儲存 M，所以陣列位置 (i,j) 對應外部索引 (i+1, j+1)；這是兩個索引範圍之間的雙射。a[1][2] 因此是 M(2,3)=7，而不是 M(1,2)=−1。外部敘述一律用一起算索引（MKO 假設 a1），程式內部的零起算索引必須先加一再對應。



S16 · implies操作前

\text{tasks of the goal}

操作後

M,N\in\mathbb{R}^{2\times 3},\ M^{\mathsf T}\in\mathbb{R}^{3\times 2},\ (M+N)^{\mathsf T}=M^{\mathsf T}+N^{\mathsf T}

條件：無

規則：and_intro_elim · 依賴：S02, S03, S04, S06, S07, S09, S10, S11, S12, S13, S14, S15

葉節點依據：and_intro_elim

合併各步：尺寸 2×3，M(1,2)=−1、M(2,3)=7，M(3,1) 不存在；M+N、Mᵀ、Nᵀ 如上；(A+B)ᵀ=Aᵀ+Bᵀ 與 (Aᵀ)ᵀ=A 對所有同尺寸實矩陣已證並在本例核對；M+Mᵀ 無定義；轉置不是倒序也不是反矩陣；a[1][2]=M(2,3)。







## 局部子步與引理

S09.1 · implies操作前

A,B\in\mathbb{R}^{m\times n}

操作後

(A+B)^{\mathsf T},\ A^{\mathsf T}+B^{\mathsf T}\in\mathbb{R}^{n\times m}

條件：無

規則：mko_matrix_def · 依賴：mko_matrix_def

葉節點依據：mko_matrix_def

A+B 是 m×n，所以 (A+B)ᵀ 是 n×m。Aᵀ、Bᵀ 都是 n×m，尺寸相同，所以 Aᵀ+Bᵀ 有定義且是 n×m。兩邊尺寸一致。



S09.2 · implies操作前

(A+B)^{\mathsf T}(j,i)

操作後

(A+B)(i,j)=A(i,j)+B(i,j)=A^{\mathsf T}(j,i)+B^{\mathsf T}(j,i)=(A^{\mathsf T}+B^{\mathsf T})(j,i)

條件：1\le j\le n; 1\le i\le m

規則：matrix_eq · 依賴：S09.1, matrix_eq, forall_intro

葉節點依據：matrix_eq + mko_matrix_def + forall_intro + eq_refl_symm_trans

取任意合法位置 (j,i)。依轉置定義、加法定義、再用一次轉置定義（兩次）與加法定義，得到等式鏈。這個位置是任意的，沒有其他假設，依 forall_intro 對所有位置成立；配合 S09.1 的尺寸相同，依 matrix_eq 得 (A+B)ᵀ=Aᵀ+Bᵀ。S09.1 與 S09.2 合起來證得引理 L_transpose_sum。



S11.1 · implies操作前

A\in\mathbb{R}^{m\times n}

操作後

(A^{\mathsf T})^{\mathsf T}\in\mathbb{R}^{m\times n},\ (A^{\mathsf T})^{\mathsf T}(i,j)=A^{\mathsf T}(j,i)=A(i,j)

條件：無

規則：matrix_eq · 依賴：mko_matrix_def, matrix_eq

葉節點依據：matrix_eq + mko_matrix_def + forall_intro

Aᵀ 是 n×m，所以 (Aᵀ)ᵀ 是 m×n，與 A 同尺寸。對任意合法 (i,j)，兩次使用轉置定義得 (Aᵀ)ᵀ(i,j)=Aᵀ(j,i)=A(i,j)。依 matrix_eq，(Aᵀ)ᵀ=A。這證得引理 L_double_transpose。







## 逐步反向審查


- S16 · sufficient_goal_reduction · S02, S03, S04, S06, S07, S09, S11, S12, S13, S14, S15 — 目標 G：題目要求的各項。足夠條件 H：S02 到 S15 的結論；H⇒G 只用合取。H 由 G1 到 G3 正向推出，沒有把 G 當作前提。
- S15 · premise_audit · G3, S03, function_def — 對應關係依賴 G3 所說的「逐行儲存、零起算」；若程式改為逐列儲存，對應也會改變。
- S14 · premise_audit · matrix_product_def, matrix_eq, numeric_evaluation — 一個不相等的元素就足以推出 SSᵀ≠I；本稿不宣稱任何一般的可逆性判準。
- S13 · premise_audit · matrix_eq, S07 — 尺寸不同就足以推出不相等；不需逐項比較。
- S12 · premise_audit · S02, S07, mko_matrix_def — 加法的前提是尺寸相同，這裡不成立；不宣稱任何「補零」的延伸定義。
- S11.1 · premise_audit · mko_matrix_def, matrix_eq, forall_intro — 需要尺寸相同與每個位置相等；位置是任意的。
- S11 · premise_audit · L_double_transpose — 引理對所有實矩陣成立，沒有附加條件。
- S10 · premise_audit · S06, S07, S08, numeric_evaluation — 有限的數值核對只支持本例，不宣稱它證明一般引理。
- S09.2 · premise_audit · S09.1, matrix_eq, mko_matrix_def, forall_intro — 需要尺寸相同（S09.1）與每個位置元素相等；只檢查有限個例子不足以代替這個對任意位置的論證。
- S09.1 · premise_audit · mko_matrix_def — 只比較尺寸；元素相等在 S09.2 處理。
- S09 · premise_audit · S05, L_transpose_sum — 引理需要 A、B 同尺寸，否則 A+B 無定義；這由 S05 確認。
- S08 · inverse_equivalence · mko_matrix_def, matrix_eq — 與 S07 相同，逐位置相等。
- S07 · inverse_equivalence · mko_matrix_def, matrix_eq — 對每個位置 (j,i) 兩邊都是 M(i,j)，尺寸都是 3×2，依 matrix_eq 相等。
- S06 · inverse_equivalence · mko_matrix_def, numeric_evaluation, matrix_eq — 兩邊尺寸相同、各位置元素相等（N1 到 N6），依 matrix_eq 是同一矩陣，雙向成立。
- S05 · premise_audit · S02, mko_matrix_def — 尺寸相同是加法的必要條件；S12 顯示尺寸不同時加法沒有定義。
- S04 · premise_audit · S02, mko_matrix_def, order_basics — 只用到尺寸 2×3 與 3>2；不宣稱程式語言對越界索引的行為。
- S03 · inverse_equivalence · def_unfold, mko_matrix_def — 讀取元素就是展開定義，兩邊指同一個數，雙向成立。
- S02 · premise_audit · mko_matrix_def, G2 — 需要各行等長；若某行長度不同，就不是矩陣。尺寸由實際行列數決定，與元素數值無關。
- S01 · premise_audit · G1, mko_matrix_def — 此步只寫出定義，不推出新事實。





## 錯誤控制與反例

先行後列，不可顛倒MKO 的誤解之一是行列顛倒。M(1,2)=−1，但 M(2,1)=5（S03）。尺寸也一樣：2×3 是 2 行 3 列，與 3×2 不同。

一起算與零起算不可混用程式陣列 a[1][2] 是第 2 行第 3 列，對應 M(2,3)=7；若直接當成 M(1,2) 會讀到 −1（S15）。外部敘述一律一起算，換到程式時每個索引減一。

轉置不是倒序，也不是反矩陣逐行倒序的 R 仍是 2×3，不可能等於 3×2 的 Mᵀ（S13）。對方陣 S，SSᵀ 的左上角是 5≠1，所以 Sᵀ 不是 S 的反矩陣（S14）。


- M(2,1)=−1 → reject — M(2,1) 是第 2 行第 1 列，等於 5；−1 是 M(1,2)。
- M+Mᵀ 可以逐項相加，得到一個 2×3 矩陣 → reject — M 是 2×3、Mᵀ 是 3×2，尺寸不同，加法無定義。
- Mᵀ 就是把 M 的行倒序：[[5,3,7],[2,−1,0]] → reject — 倒序後仍是 2×3，而 Mᵀ 是 3×2。
- 對 S=[[1,2],[3,4]]，Sᵀ 是 S 的反矩陣 → reject — SSᵀ=[[5,11],[11,25]]≠I。
- M(3,1)=0，因為不存在的元素視為零 → reject — M 只有 2 行，索引 (3,1) 不合法，M(3,1) 沒有定義。





## 結論與限制

M、N 都是 2×3；M(1,2)=−1、M(2,3)=7，M(3,1) 無定義。M+N 的兩行是 (3,3,−2)、(5,0,13)；Mᵀ 是 3×2，三行 (2,5)、(−1,3)、(0,7)。對所有同尺寸實矩陣，(A+B)ᵀ=Aᵀ+Bᵀ 且 (Aᵀ)ᵀ=A。M+Mᵀ 無定義；逐行倒序得到的仍是 2×3 矩陣，不是 Mᵀ；SSᵀ≠I，所以轉置不是反矩陣。零起算的 a[1][2] 是 M(2,3)。


- S14 只用一個反例說明轉置不是反矩陣，不建立任何可逆性判準；可逆性屬於行列式條目。
- 零維矩陣不在本輪論域；MKO 的 formal next（Matrix、Fin 索引與 transpose 的橋接）未做。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 11d27b132fd8b4c156a7d9df045c5b76fa1ae688439164a3b668eba604457062
- original source SHA-256: ab1824ca602b6e508a8860bde242742b7d3d7b9592baf70d2bfaeb895c821baf
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-matrix-01.json)