Matrices: dimensions, one-based indexing, entrywise addition and transpose

Goal and scope

Let M=[[2,−1,0],[5,3,7]] and N=[[1,4,−2],[0,−3,6]] (each inner bracket is one row). Find their dimensions, read off M(1,2) and M(2,3), and decide whether M(3,1) exists; compute M+N, Mᵀ and Nᵀ; prove (A+B)ᵀ=Aᵀ+Bᵀ and (Aᵀ)ᵀ=A for all real matrices of equal size and check them on M and N; explain why M+Mᵀ is undefined; finally use counterexamples to separate the transpose from reversing the rows and from the inverse matrix, and translate zero-based program indices back to one-based indices.

Stays inside the MKO's scope: real matrices with positive numbers of rows and columns (1 to 5), one-based external indices, entrywise addition of equal-size matrices, and transpose. It fully proves that transpose is compatible with addition and that transposing twice restores the matrix; the matrix product appears only in one counterexample showing that the transpose is not the inverse. It does not treat zero-dimensional matrices, determinants or invertibility in general, and does not build the Lean Fin-index bridge; it does not change the canonical MKO or its English edition.

Givens and symbols

• numeric_evaluation
• function_def
• add_comm
• forall_intro

• G1 — Conventions: real matrices; external row and column indices start at 1; each dimension is from 1 to 5, with nonempty rows of equal length; the concrete matrices such as M,N have integer entries (MKO assumptions a1, a2), while the general transpose identities are proved for real entries.
• G2 — The two rows of M are (2,−1,0) and (5,3,7); the two rows of N are (1,4,−2) and (0,−3,6).
• G3 — A program stores M row by row in a zero-based array a: a[i][j] with 0≤i≤1 and 0≤j≤2. Also a square matrix S with rows (1,2) and (3,4) is used only in a counterexample.

• M(i,j) — the entry in row i and column j; in the MKO's wording 行 means row and 列 means column
• m\times n — the dimensions: m rows and n columns
• M^{\mathsf T} — the transpose of M
• a[i][j] — a zero-based program array index
• A,B — arbitrary real matrices of equal size

Rules and sources

• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• matrix_product_def · prerequisite — Matrix product: for A of size m×n and B of size n×p, (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}. Matrix multiplication is in general not commutative.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_matrix_def · cited — An m×n real matrix M is a table of real entries indexed by row i and column j, with positive integers m,n. External indices in this pulse start at one: M(i,j) is the entry in row i and column j. Matrices of the same dimensions add entrywise. The transpose Mᵀ has dimensions n×m and places M(i,j) at Mᵀ(j,i). · mko-matrix
• matrix_eq · prerequisite — Two matrices are equal ⇔ they have the same dimensions and equal entries at every legal index (i,j).
• L_transpose_sum · lemma — For all m×n real matrices A and B: (A+B)ᵀ=Aᵀ+Bᵀ.
• L_double_transpose · lemma — For every m×n real matrix A: (Aᵀ)ᵀ=A.

Main derivation

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}

Substeps and lemmas

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)

Reverse audits

• S16 · sufficient_goal_reduction · S02, S03, S04, S06, S07, S09, S11, S12, S13, S14, S15 — Goal G: the items asked for. Sufficient condition H: the conclusions of S02 to S15; H⇒G uses only conjunction. H is derived forwards from G1 to G3; G is never used as a premise.
• S15 · premise_audit · G3, S03, function_def — The correspondence depends on G3's 'row by row, zero-based' storage; if the program stored column by column, the correspondence would change.
• S14 · premise_audit · matrix_product_def, matrix_eq, numeric_evaluation — One unequal entry suffices for SSᵀ≠I; no general invertibility criterion is claimed here.
• S13 · premise_audit · matrix_eq, S07 — Different dimensions suffice for inequality; no entrywise comparison is needed.
• S12 · premise_audit · S02, S07, mko_matrix_def — Addition requires equal dimensions, which fails here; no extended definition by 'padding with zeros' is claimed.
• S11.1 · premise_audit · mko_matrix_def, matrix_eq, forall_intro — It needs equal dimensions and equality at every position; the position is arbitrary.
• S11 · premise_audit · L_double_transpose — The lemma holds for every real matrix, with no side condition.
• S10 · premise_audit · S06, S07, S08, numeric_evaluation — A finite numeric check supports this example only and is not claimed to prove the general lemma.
• S09.2 · premise_audit · S09.1, matrix_eq, mko_matrix_def, forall_intro — It needs equal dimensions (S09.1) and equal entries at every position; checking a few examples could not replace this argument for an arbitrary position.
• S09.1 · premise_audit · mko_matrix_def — Only dimensions are compared here; equality of entries is handled in S09.2.
• S09 · premise_audit · S05, L_transpose_sum — The lemma needs A and B of equal size, otherwise A+B is undefined; S05 confirms this.
• S08 · inverse_equivalence · mko_matrix_def, matrix_eq — As in S07, equal at every position.
• S07 · inverse_equivalence · mko_matrix_def, matrix_eq — At every position (j,i) both sides are M(i,j) and both are 3×2, so they are equal by matrix_eq.
• S06 · inverse_equivalence · mko_matrix_def, numeric_evaluation, matrix_eq — Both sides have the same dimensions and equal entries at every position (N1 to N6), so by matrix_eq they are the same matrix, two-way.
• S05 · premise_audit · S02, mko_matrix_def — Equal dimensions are required for addition; S12 shows that addition is undefined when they differ.
• S04 · premise_audit · S02, mko_matrix_def, order_basics — It uses only the dimensions 2×3 and 3>2; it makes no claim about how a programming language treats out-of-range indices.
• S03 · inverse_equivalence · def_unfold, mko_matrix_def — Reading an entry is unfolding the definition; both sides name the same number, so it is two-way.
• S02 · premise_audit · mko_matrix_def, G2 — It needs rows of equal length; with a row of different length the table would not be a matrix. Dimensions are fixed by the actual numbers of rows and columns, not by the entry values.
• S01 · premise_audit · G1, mko_matrix_def — This step only states the definition; it derives no new fact.

Error controls and negative controls

Row first, then column

One misconception the MKO names is swapping rows and columns. M(1,2)=−1 but M(2,1)=5 (S03). The same holds for dimensions: 2×3 means 2 rows and 3 columns, which differs from 3×2.

Do not mix one-based and zero-based indices

The program entry a[1][2] is row 2, column 3, which corresponds to M(2,3)=7; reading it as M(1,2) would give −1 (S15). External statements are one-based throughout, and each index is reduced by one when moving into the program.

The transpose is neither reversal nor the inverse

Reversing the rows gives R, still 2×3, which cannot equal the 3×2 matrix Mᵀ (S13). For the square matrix S, the top-left entry of SSᵀ is 5≠1, so Sᵀ is not the inverse of S (S14).

• M(2,1)=−1 → reject — M(2,1) is row 2, column 1, which is 5; −1 is M(1,2).
• M+Mᵀ can be added entrywise to give a 2×3 matrix → reject — M is 2×3 and Mᵀ is 3×2; the dimensions differ, so the sum is undefined.
• Mᵀ is M with its rows reversed: [[5,3,7],[2,−1,0]] → reject — The reversed matrix is still 2×3, whereas Mᵀ is 3×2.
• For S=[[1,2],[3,4]], Sᵀ is the inverse of S → reject — SSᵀ=[[5,11],[11,25]]≠I.
• M(3,1)=0, because missing entries count as zero → reject — M has only 2 rows; the index (3,1) is not legal and M(3,1) is undefined.

Result and limitations

M and N are 2×3; M(1,2)=−1 and M(2,3)=7, while M(3,1) is undefined. M+N has rows (3,3,−2) and (5,0,13); Mᵀ is 3×2 with rows (2,5), (−1,3), (0,7). For all real matrices of equal size, (A+B)ᵀ=Aᵀ+Bᵀ and (Aᵀ)ᵀ=A. M+Mᵀ is undefined; reversing the rows still gives a 2×3 matrix, not Mᵀ; SSᵀ≠I, so the transpose is not the inverse. The zero-based a[1][2] is M(2,3).

• S14 uses a single counterexample to show the transpose is not the inverse and establishes no invertibility criterion; invertibility belongs to the determinant entry.
• Zero-dimensional matrices are outside this pulse; the MKO's formal next step (bridging Matrix, Fin indices and transpose) is not done.

Verification and source binding

15 declared checks for this guide; only the listed expressions are covered.

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

Same-source full JSON (formulas, ASTs, controls and revision log)