Read-back: HefferonLinAlg.jordanBlocks_unique

What the statement asserts

For every natural number $n$, every $n \times n$ matrix $A$ with complex entries, every pair of natural numbers $k_1, k_2$, and every choice of four functions

$$\mathrm{sz}_1 : \{0,\dots,k_1-1\} \to \mathbb{N}, \qquad \lambda_1 : \{0,\dots,k_1-1\} \to \mathbb{C},$$ $$\mathrm{sz}_2 : \{0,\dots,k_2-1\} \to \mathbb{N}, \qquad \lambda_2 : \{0,\dots,k_2-1\} \to \mathbb{C},$$

if the block data $(\mathrm{sz}_1, \lambda_1)$ is a Jordan form of $A$ and the block data $(\mathrm{sz}_2, \lambda_2)$ is a Jordan form of $A$ — both in the precise sense unfolded below — then the two multisets of size–eigenvalue pairs coincide:

$$\{\!\{\,(\mathrm{sz}_1(i), \lambda_1(i)) \;:\; i = 0,\dots,k_1-1 \,\}\!\} \;=\; \{\!\{\,(\mathrm{sz}_2(j), \lambda_2(j)) \;:\; j = 0,\dots,k_2-1 \,\}\!\}$$

as multisets of elements of $\mathbb{N} \times \mathbb{C}$. All of $n$, $A$, $k_1$, $k_2$, $\mathrm{sz}_1$, $\lambda_1$, $\mathrm{sz}_2$, $\lambda_2$ are implicit arguments universally quantified over; the two Jordan-form hypotheses are the only hypotheses. There is no hypothesis of invertibility, nonzero size, distinctness of eigenvalues, ordering of block sizes, or anything else about $A$.

The named constructions, unfolded

Jordan block. For $m \in \mathbb{N}$ and a scalar $\mu$, $J_m(\mu)$ is the $m \times m$ matrix whose $(i,j)$ entry is

$$\bigl(J_m(\mu)\bigr)_{ij} \;=\; \begin{cases} \mu & \text{if } i = j,\\ 1 & \text{if } i = j+1,\\ 0 & \text{otherwise,}\end{cases}$$

with $i, j$ read as integers in $\{0,\dots,m-1\}$. The $1$'s therefore sit on the subdiagonal (directly below the diagonal), not above it. For $m = 0$ this is the empty matrix.

Index type of a Jordan matrix. Given $k$ and $\mathrm{sz} : \{0,\dots,k-1\} \to \mathbb{N}$, the index set is the disjoint union

$$I(\mathrm{sz}) \;=\; \coprod_{i=0}^{k-1} \{0,\dots,\mathrm{sz}(i)-1\},$$

whose elements are pairs $\langle i, a\rangle$ with $a < \mathrm{sz}(i)$. Its cardinality is $\sum_{i=0}^{k-1} \mathrm{sz}(i)$.

Jordan matrix. $J(\mathrm{sz},\lambda)$ is the matrix indexed by $I(\mathrm{sz}) \times I(\mathrm{sz})$ that is block diagonal with the $i$-th diagonal block equal to $J_{\mathrm{sz}(i)}(\lambda(i))$:

$$J(\mathrm{sz},\lambda)_{\langle i,a\rangle,\,\langle j,b\rangle} \;=\; \begin{cases} \bigl(J_{\mathrm{sz}(i)}(\lambda(i))\bigr)_{ab} & \text{if } i = j,\\ 0 & \text{if } i \neq j.\end{cases}$$

Similarity. For square matrices $X, Y$ over a commutative ring, indexed by the same finite index set, "$X$ is similar to $Y$" means: there exists a matrix $P$ of the same shape such that $\det P$ is a unit (over $\mathbb{C}$: $\det P \neq 0$) and

$$P^{-1} X P \;=\; Y,$$

where $P^{-1}$ is the total matrix-inverse operation, which — because $\det P$ is assumed to be a unit — is the genuine two-sided inverse of $P$. Note the direction: it is $X$ that is conjugated into $Y$.

"$(\mathrm{sz}, \lambda)$ is a Jordan form of $A$." For $A$ indexed by $\{0,\dots,n-1\}$, this is the conjunction of two conditions:

1. Every block is nonempty: $\mathrm{sz}(i) > 0$ for all $i \in \{0,\dots,k-1\}$.
2. There exists a bijection $e : \{0,\dots,n-1\} \xrightarrow{\ \sim\ } I(\mathrm{sz})$ such that $A$ is similar (in the sense just given, as matrices indexed by $\{0,\dots,n-1\}$) to the matrix obtained from $J(\mathrm{sz},\lambda)$ by relabelling its rows and columns along $e$ — i.e. to the matrix $M$ with $M_{ab} = J(\mathrm{sz},\lambda)_{e(a),\,e(b)}$. Explicitly: there exist $e$ and a matrix $P$ over $\mathbb{C}$ indexed by $\{0,\dots,n-1\}$ with $\det P \neq 0$ and $P^{-1} A P = M$.

The bijection $e$ and the conjugator $P$ are existentially quantified separately inside each hypothesis; nothing links the ones supplied by the first hypothesis to the ones supplied by the second.

The multiset of blocks. $\mathrm{jordanBlocks}(\mathrm{sz},\lambda)$ is the multiset obtained by running $i$ over all of $\{0,\dots,k-1\}$ and collecting the pairs $(\mathrm{sz}(i), \lambda(i))$, keeping repetitions. It has exactly $k$ elements counted with multiplicity; the pair $(\mathrm{sz}(i), \lambda(i))$ appears once for each index $i$ producing it.

What the conclusion does and does not say

• Multiset equality means: the two collections contain the same size–eigenvalue pairs with the same multiplicities. Size and eigenvalue are matched jointly, not separately — the pair $(3, 5)$ on one side must be answered by a pair $(3,5)$ on the other, not merely by "some block of size $3$" and "some block with eigenvalue $5$".
• Because a multiset's cardinality is preserved, the conclusion in particular forces $k_1 = k_2$; equivalently, it is logically the same as the existence of a bijection $\sigma$ from $\{0,\dots,k_1-1\}$ to $\{0,\dots,k_2-1\}$ with $\mathrm{sz}_1(i) = \mathrm{sz}_2(\sigma(i))$ and $\lambda_1(i) = \lambda_2(\sigma(i))$ for all $i$.
• It says nothing about the ordering of the blocks, and nothing about the bijections $e$ or the conjugating matrices $P$ appearing in the two hypotheses; no relation between them is claimed.
• It does not assert that a Jordan form exists for any given $A$, nor that the $\lambda$'s are eigenvalues of $A$, nor that eigenvalues appearing in different blocks are distinct, nor that block sizes are listed in any order. It is a conditional statement: if two such block descriptions are given, they agree as multisets.

Degenerate and boundary cases covered by the quantifiers

• $n = 0$: $A$ is the empty matrix. A bijection $\{0,\dots,n-1\} \simeq I(\mathrm{sz})$ requires $\sum_i \mathrm{sz}(i) = n$; combined with condition 1 ($\mathrm{sz}(i) > 0$ for every $i$), $n = 0$ forces $k = 0$ and hence both multisets are empty.
• $k = 0$: allowed for either hypothesis; condition 1 is then vacuously true, $I(\mathrm{sz})$ is empty, and the resulting multiset is empty. As above, this is compatible with the hypotheses only when $n = 0$.
• Size-zero blocks are excluded by condition 1, so a block description may not be padded with empty blocks carrying arbitrary eigenvalues.
• Dimension constraint: more generally, each hypothesis silently forces $n = \sum_{i=0}^{k-1} \mathrm{sz}(i)$, via the existence of the bijection $e$.
• Repeated pairs: the multiset construction keeps duplicates, so two distinct indices with the same size and the same eigenvalue contribute two copies.
• The hypotheses are simultaneous assumptions about a single fixed $A$; if for a particular $A$ no such data exists, the statement holds vacuously for that $A$.

Note on the artifact

The declaration is stated with its proof omitted (the proof body is a placeholder), so the file contains the statement above and no argument for it.