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

目標與範圍

設 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。

逐步主鏈

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

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

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

M(3,1)

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

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

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

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}

M^{\mathsf T}

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

N^{\mathsf T}

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

(M+N)^{\mathsf T}

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

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

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

M

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}

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}

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

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

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

局部子步與引理

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

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

(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)

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)

逐步反向審查

• 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、反控制與修訂記錄）