Dimension of the span of transition matrices

Proved

MarkovEntanglement.transitionSpan_finrank

by tianyipeng · Aug 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

dimensionlinear-algebraspanstochastic-matrix

Statement

Lemma. Let $\Omega_P \subseteq \mathbb{R}^{m \times m}$ be the linear span of the $m \times m$ transition matrices. Then

\dim(\Omega_P) \;=\; m^2 - m + 1 .

Notes

The transition matrices form an affine set, not a subspace — each row must sum to one — so their span is a proper subspace of all $m \times m$ matrices, of codimension $m - 1$ . A basis is given by the matrices $Z_{ij}$ that put a one at $(i,j)$ and along the diagonal.

The count matters for the entanglement theory: the minimal subspace containing all separable transitions on a product space has dimension $\dim(\Omega_P)^2$ , which is how one sees that separable matrices are a thin subset of all joint transitions — most multi-agent systems are entangled.

Search terms: dimension of the space of stochastic matrices, affine span row-stochastic, codimension of transition matrices.

Preamble

import Mathlib
import Definitions.Def_markov_entanglement_multi

open scoped BigOperators
open MarkovEntanglement

Formal statement

namespace MarkovEntanglement

theorem transitionSpan_finrank (m : ℕ) (hm : 0 < m) :
    Module.finrank ℝ (transitionSpan (Fin m)) = m ^ 2 - m + 1 := by
  sorry

end MarkovEntanglement

Source

Shuze Chen and Tianyi Peng, *Multi-agent Markov Entanglement*, arXiv:2506.02385v3, Lemma 3, p. 34

Read-back

What the Lean code literally says, in plain math · claude-opus-5

Read-back: `transitionSpan_finrank`

What the statement literally asserts

For every natural number $m$ satisfying $0 < m$ , the following holds. Work inside the real vector space $\mathbb{R}^{m \times m}$ of all real matrices whose rows and columns are indexed by $\{0, 1, \dots, m-1\}$ (this ambient space has dimension $m^2$ ). Inside it, consider the set

T_m \;=\; \bigl\{\, P \in \mathbb{R}^{m\times m} \;:\; P_{ij} \ge 0 \text{ for all } i,j, \ \text{ and } \ \textstyle\sum_{j} P_{ij} = 1 \text{ for every } i \,\bigr\},

i.e. the set of row-stochastic matrices: every entry is nonnegative and every row sums to exactly $1$ . (This is the expansion of the bundle's IsTransitionMatrix: a conjunction of entrywise nonnegativity and the row-sum-one condition; no condition is imposed on columns.) Let

\mathrm{transitionSpan}(m) \;=\; \operatorname{span}_{\mathbb{R}} T_m

be the linear span of $T_m$ over $\mathbb{R}$ — the set of all finite $\mathbb{R}$ -linear combinations of row-stochastic matrices, with arbitrary real coefficients (not the convex hull, and not the affine hull: the coefficients are unconstrained). The theorem asserts the exact equality of natural numbers

\dim_{\mathbb{R}} \bigl(\operatorname{span}_{\mathbb{R}} T_m\bigr) \;=\; m^2 - m + 1 ,

where the dimension is the rank of this subspace as a real vector space, and the right-hand side is computed in the natural numbers: the subtraction $m^2 - m$ is truncated (it would return $0$ rather than a negative number), and the addition of $1$ happens after the subtraction, so the expression is $(m^2 - m) + 1$ . This is an equality, not an inequality or a bound.

Every variable in the conclusion

$m$ — the only variable occurring in the conclusion. It is constrained by the single hypothesis $0 < m$ , i.e. $m \ge 1$ . It is otherwise arbitrary and universally quantified: the claim is made simultaneously for every $m \ge 1$ .
There are no other explicit or implicit variables. The only implicit data are the standard structures used to index the matrices ( $\{0,\dots,m-1\}$ is finite and has decidable equality), which exist canonically and impose no restriction.
Since $m \ge 1$ , we have $m^2 \ge m$ , so the truncated subtraction agrees with ordinary integer subtraction and the right-hand side is the ordinary value $m^2 - m + 1 \ge 1$ .

Joint satisfiability of the hypotheses

The hypothesis set consists of the single condition $0 < m$ , which is satisfied by every $m \in \{1, 2, 3, \dots\}$ . The hypotheses are therefore satisfiable, and the theorem is not vacuous: it makes an assertion for infinitely many instances.

Degenerate and edge cases

$m = 0$ is excluded. The hypothesis $0 < m$ removes it. Had it been admitted, the right-hand side would evaluate to $(0 - 0) + 1 = 1$ , while the left-hand side is the dimension of a span inside the zero-dimensional space of matrices indexed by the empty set — and the empty index set admits exactly one matrix (the empty one), which does satisfy the row-stochastic conditions vacuously, so the span is the zero subspace of dimension $0$ .
Smallest permitted value $m = 1$ . The ambient space $\mathbb{R}^{1\times 1}$ is $1$ -dimensional. The row-sum condition forces the unique entry to be $1$ , so $T_1 = \{(1)\}$ , whose linear span is the whole $1$ -dimensional space; its dimension is $1$ . The right-hand side evaluates to $1^2 - 1 + 1 = 1$ .
Next value, for calibration. At $m = 2$ the right-hand side is $2^2 - 2 + 1 = 3$ , asserted about a subspace of the $4$ -dimensional space of $2 \times 2$ real matrices.
Dimension conventions. The rank function used returns $0$ for a module that is not finitely generated; that convention is never triggered here, since the ambient matrix space is finite-dimensional and so is every subspace of it. Consequently the left-hand side is a genuine dimension for every $m \ge 1$ .
The set $T_m$ is nonempty for every $m \ge 1$ (the identity matrix and the uniform matrix with all entries $1/m$ both lie in it), so the span is not the zero subspace.

Human review

Endorsed by Shuze Chen · Aug 7, 2026
Endorsed by tianyipeng · Aug 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph