Read-back — HefferonLinAlg_jordan.lean

All declarations live in a namespace HefferonLinAlg. Throughout, $R$ is an arbitrary type (an implicit parameter of every declaration below except kerDim), and the typeclass assumptions carried by each declaration are stated individually; they differ from declaration to declaration and are not uniform across the bundle.

---

1. IsSimilar (definition)

Assumptions: $R$ is a commutative ring; $\iota$ is an arbitrary type that is a finite type and has decidable equality; $A, B$ are $\iota \times \iota$ matrices over $R$.

This defines a proposition, "$A$ is similar to $B$", to mean:

$$\exists\, P \in \mathrm{Mat}_{\iota\times\iota}(R):\quad \det(P) \text{ is a unit of } R \ \ \wedge\ \ P^{-1} A P = B.$$

Three points of literal content. First, the condition on $P$ is that $\det P$ is an invertible element of the ring $R$ (i.e. there is $u \in R$ with $u \cdot \det P = 1$), not that $\det P = 1$ and not merely that $\det P \neq 0$. Second, $P^{-1}$ denotes the total "nonsingular inverse" operation on matrices (adjugate divided by determinant), which returns a junk value — the zero matrix — when the determinant is not invertible; here that junk branch is excluded by the hypothesis, so $P^{-1}$ is a genuine two-sided inverse of $P$. Third, the equation is written in the specific order $P^{-1} A P = B$ (the conjugating matrix on the right, its inverse on the left); no symmetry, reflexivity, transitivity, or any other property of this relation is asserted anywhere in this file. Degenerate case: if $\iota$ is empty, there is exactly one matrix and $\det$ of it is $1$, so the relation holds trivially for the unique $A = B$.

---

2. jordanBlock (definition)

Assumptions: $R$ carries only a distinguished element $0$ and a distinguished element $1$ — no ring, group, or even additive structure is assumed. Inputs: a natural number $m$ and a scalar $\lambda \in R$.

This defines the $m \times m$ matrix $J_m(\lambda)$ indexed by $\{0,1,\dots,m-1\}$ in both coordinates, whose $(i,j)$ entry is

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

where $i = j+1$ is an equation between the underlying natural-number values of the indices. So $\lambda$ sits on the diagonal and $1$ sits on the subdiagonal (the entries immediately below the diagonal); the superdiagonal entries are $0$. The two cases are tested in that order, but they are mutually exclusive as stated, since $i = j$ and $i = j+1$ cannot both hold in $\mathbb{N}$. Nothing is assumed relating $0$ and $1$ in $R$; in particular $R$ may be trivial ($0 = 1$). Degenerate cases: $m = 0$ yields the empty matrix; $m = 1$ yields the $1 \times 1$ matrix $(\lambda)$ with no subdiagonal.

---

3. jordanBlock_apply (theorem, tagged as a simplification lemma)

Assumptions: $R$ has a $0$ and a $1$; $m$ is a natural number (implicit); $\lambda \in R$; $i, j$ are indices in $\{0,\dots,m-1\}$.

The claim is that the $(i,j)$ entry of the matrix $J_m(\lambda)$ of §2 equals $\lambda$ if $i = j$, else $1$ if the natural number $i$ equals the natural number $j+1$, else $0$. This restates the defining formula of §2 verbatim and is proved by definitional unfolding; it asserts no new mathematical content.

---

4. jordanIndex (abbreviation)

Assumptions: none beyond a natural number $k$ (implicit) and a function $sz : \{0,\dots,k-1\} \to \mathbb{N}$.

This names the index type

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

the disjoint union (dependent pair type) whose elements are pairs $(i, a)$ with $i$ a block label in $\{0,\dots,k-1\}$ and $a$ an index in $\{0,\dots,sz(i)-1\}$. Its cardinality is $\sum_{i} sz(i)$. Degenerate cases: if $k = 0$, or if every $sz(i) = 0$, this type is empty; blocks with $sz(i) = 0$ contribute no indices.

---

5. jordanMatrix (definition)

Assumptions: $R$ has a $0$ and a $1$; $k$ is a natural number (implicit); $sz$ assigns a natural-number size to each of the $k$ block labels, and $\lambda$ assigns an element of $R$ to each block label.

This defines the block-diagonal matrix indexed by $\mathcal{I}(sz) \times \mathcal{I}(sz)$ (§4) whose $i$-th diagonal block is the $sz(i) \times sz(i)$ matrix $J_{sz(i)}(\lambda(i))$ of §2 and whose off-diagonal blocks are zero:

$$J(sz,\lambda) \;=\; \operatorname{diag}\bigl(J_{sz(0)}(\lambda(0)),\; \dots,\; J_{sz(k-1)}(\lambda(k-1))\bigr).$$

The eigenvalue function $\lambda$ is arbitrary: distinct blocks may carry the same scalar, and no relation among the $\lambda(i)$ is imposed. Sizes are arbitrary naturals, including $0$.

---

6. jordanMatrix_apply_same (theorem, tagged as a simplification lemma)

Assumptions: $R$ has a $0$ and a $1$; $k$ (implicit), $sz$, $\lambda$ as above; $i$ a block label; $a, b$ indices in $\{0,\dots,sz(i)-1\}$.

The claim: the entry of $J(sz,\lambda)$ at row $(i,a)$ and column $(i,b)$ — i.e. two indices lying in the same block $i$ — equals the $(a,b)$ entry of the single Jordan block $J_{sz(i)}(\lambda(i))$.

---

7. jordanMatrix_apply_ne (theorem, tagged as a simplification lemma)

Assumptions: $R$ has a $0$ and a $1$; $k$ (implicit), $sz$, $\lambda$ as above; block labels $i, j$ (implicit); $a$ an index in $\{0,\dots,sz(i)-1\}$, $b$ an index in $\{0,\dots,sz(j)-1\}$; and the explicit hypothesis $i \neq j$.

The claim: whenever the row's block label differs from the column's block label, the entry of $J(sz,\lambda)$ at row $(i,a)$, column $(j,b)$ is $0$.

---

8. IsJordanFormOf (definition)

Assumptions: $R$ is a commutative ring; $\iota$ is a finite type with decidable equality; $k$ is a natural number (implicit); $A$ is an $\iota \times \iota$ matrix over $R$; $sz : \{0,\dots,k-1\} \to \mathbb{N}$ and $\lambda : \{0,\dots,k-1\} \to R$.

This defines the proposition "the block data $(sz,\lambda)$ is a Jordan form of $A$" as the conjunction of:

1. Every block is nonempty: $sz(i) > 0$ for all $i \in \{0,\dots,k-1\}$; and
2. There exists a bijection $e : \iota \xrightarrow{\ \sim\ } \mathcal{I}(sz)$ between the index type of $A$ and the disjoint union of block index sets, such that $A$ is similar (in the exact sense of §1: there exists $P$ over $\iota$ with $\det P$ a unit and $P^{-1} A P$ equal to the target) to the matrix obtained by transporting $J(sz,\lambda)$ along $e$, namely the $\iota \times \iota$ matrix whose $(x,y)$ entry is $J(sz,\lambda)_{e(x),\,e(y)}$.

Several literal points. The bijection is existentially quantified, so no particular ordering of $\iota$ is fixed; but its mere existence forces $|\iota| = \sum_i sz(i)$, so the proposition is unsatisfiable for any block data whose sizes do not sum to the size of $A$. The similarity is stated in the direction "$A$ is similar to the reindexed Jordan matrix", with the conjugator $P$ ranging over $\iota$-indexed matrices with unit determinant. Nothing asserts that the $\lambda(i)$ are eigenvalues, roots of the characteristic polynomial, or otherwise related to $A$ except through this similarity; nothing asserts uniqueness of $(sz,\lambda)$; and no ordering, grouping, or distinctness condition on the blocks is imposed. Degenerate cases: $k = 0$ (no blocks) satisfies condition 1 vacuously and is possible exactly when $\iota$ is empty; conversely condition 1 rules out any block of size $0$, so padding with empty blocks is excluded.

---

9. HasJordanForm (definition)

Assumptions: $R$ is a commutative ring; $\iota$ is a finite type with decidable equality; $A$ is an $\iota \times \iota$ matrix over $R$.

This defines the proposition "$A$ has a Jordan form" as: there exist a natural number $k$, a size function $sz : \{0,\dots,k-1\} \to \mathbb{N}$, and a scalar function $\lambda : \{0,\dots,k-1\} \to R$ such that $(sz,\lambda)$ is a Jordan form of $A$ in the sense of §8 — i.e. all $sz(i) > 0$, and for some bijection $e : \iota \simeq \mathcal{I}(sz)$ and some matrix $P$ over $\iota$ with $\det P$ a unit of $R$, $P^{-1} A P$ equals the matrix with entries $J(sz,\lambda)_{e(x),e(y)}$. This is a definition only; no theorem in this file asserts that any matrix has this property, and in particular no existence theorem over $\mathbb{C}$ or any algebraically closed field is stated.

---

10. jordanBlocks (definition)

Assumptions: none at all on $R$ — no ring, no zero, no one; $R$ is a bare type. Inputs: $k$ (implicit), $sz : \{0,\dots,k-1\} \to \mathbb{N}$, $\lambda : \{0,\dots,k-1\} \to R$.

This defines the multiset (unordered collection with multiplicities) of pairs

$$\bigl\{\!\!\bigl\{\,(sz(0),\lambda(0)),\ (sz(1),\lambda(1)),\ \dots,\ (sz(k-1),\lambda(k-1))\,\bigr\}\!\!\bigr\} \ \in\ \text{Multiset}(\mathbb{N}\times R),$$

obtained by mapping $i \mapsto (sz(i), \lambda(i)$) over all $k$ block labels. It has exactly $k$ elements counted with multiplicity; repeated pairs are kept as repetitions and only the ordering of the blocks is forgotten. This is a construction on arbitrary block data; it is attached to no matrix, and no theorem in this file relates it to IsJordanFormOf, HasJordanForm, or any uniqueness claim.

---

11. kerDim (definition, noncomputable)

Assumptions: $K$ is a field (a fresh type variable, not the $R$ used above); $n$ is a natural number (implicit); $A$ is an $n \times n$ matrix over $K$ indexed by $\{0,\dots,n-1\}$; $\lambda \in K$; $r \in \mathbb{N}$.

This defines the natural number

$$\dim_K \ker\Bigl(\, x \mapsto (A - \lambda I)^{r} x \,\Bigr),$$

that is: form the matrix $A - \lambda \cdot I$ (the scalar $\lambda$ acting on the identity matrix, i.e. the diagonal matrix with $\lambda$ in every diagonal position), raise it to the $r$-th power as a matrix product, view the result as the $K$-linear endomorphism of the coordinate space $K^{n}$ given by multiplication on the standard basis, and take the $K$-dimension of its kernel as a submodule of $K^n$.

Literal points: matrix power is the ordinary product, so $r = 0$ gives the identity matrix, whose kernel is $\{0\}$ and hence $\mathrm{kerDim}(A,\lambda,0) = 0$; $n = 0$ gives the zero space and dimension $0$ for every $r$. The value is the rank/dimension function that returns a natural number (returning $0$ in the degenerate convention for non-finite-dimensional modules, which does not arise here since $K^n$ is finite-dimensional). No theorem in this file states any property of this quantity — no monotonicity in $r$, no stabilization, no relation to block sizes or to any of the Jordan definitions above.

---

Scope note

The file contains three theorems (§3, §6, §7); each is an entry-value computation for the matrices defined in §2 and §5, and each is proved by unfolding definitions. Everything else (§1, §2, §4, §5, §8, §9, §10, §11) is a definition or abbreviation. No statement in the file asserts existence, uniqueness, or invariance of Jordan forms, and no statement connects kerDim or jordanBlocks to IsJordanFormOf or HasJordanForm.