Read-back: separable_iff_resolvent_separable

What the statement asserts. Fix a natural number $N$ and a family of types $S_0, \dots, S_{N-1}$ indexed by $i \in \{0,\dots,N-1\}$, each assumed finite and with decidable equality. Write

for the joint space (in the code, Joint S), itself a finite type with decidable equality. Then for every real matrix $P$ indexed by $\mathcal{J} \times \mathcal{J}$ and every real number $\gamma$ with $0 < \gamma$ and $\gamma < 1$ (two separate strict inequalities), assuming $P$ is a transition matrix, the statement asserts the two-directional equivalence

where $I$ is the identity matrix on $\mathcal{J}$, $\gamma P$ and $(1-\gamma)(\cdot)$ are entrywise scalar multiples, and $(\cdot)^{-1}$ is Mathlib's total matrix inverse (see below). Both directions are asserted; neither is weakened to a one-way implication.

Every non-standard notion, unfolded.

• $P$ is a transition matrix (IsTransitionMatrix), the sole hypothesis on $P$: all entries are nonnegative, $P_{p,q} \ge 0$ for all $p,q \in \mathcal{J}$, and every row sums to one, $\sum_{q \in \mathcal{J}} P_{p,q} = 1$ for all $p$. (Row-stochastic; no irreducibility, aperiodicity, or positivity.)

• Tensor product of local transitions (tensorProdN): given a family $Q = (Q^{(i)})_i$ with $Q^{(i)} \in \mathbb{R}^{S_i \times S_i}$, the matrix $\bigotimes Q$ on $\mathcal{J}$ has entries

• $M$ is separable (IsSeparableN), applied to each side of the equivalence: there exist a natural number $K$, real coefficients $x_0,\dots,x_{K-1}$, and for each $k$ a family of local matrices $Q^{(k,i)} \in \mathbb{R}^{S_i \times S_i}$, such that

  1. every $Q^{(k,i)}$ is a transition matrix (nonnegative entries, rows summing to one), for all $k$ and all $i$;
  2. $\sum_{k=0}^{K-1} x_k = 1$;
  3. $M \;=\; \sum_{k=0}^{K-1} x_k \cdot \big(\bigotimes_i Q^{(k,i)}\big)$ as matrices on $\mathcal{J}$.

  Note that the $x_k$ range over all reals and may be negative: this is a finite affine combination of tensor products, not a convex one. $K$ is finite but unbounded. $K = 0$ is permitted by the quantifier but cannot satisfy condition 2, since the empty sum is $0 \ne 1$; so any witness has $K \ge 1$.

Constrained vs. free variables in the conclusion. Every variable appearing in the conclusion — $N$, the family $S$, the two typeclass instances, the matrix $P$, and the scalar $\gamma$ — is bound by a binder of the theorem; the conclusion has no free variables. Inside each occurrence of "is separable", the witnesses $K$, $(x_k)$, $(Q^{(k,i)})$ are existentially bound and are not required to be the same on the two sides of the equivalence: the statement asserts only that a decomposition exists for one side iff a (possibly completely different) decomposition exists for the other. $\gamma$ is constrained only by $0<\gamma<1$; $P$ only by row-stochasticity.

Joint satisfiability and degenerate cases. The hypotheses are jointly satisfiable, so the statement is not vacuous: e.g. $\gamma = 1/2$ with $P$ the uniform stochastic matrix on any nonempty $\mathcal{J}$. The open interval $0<\gamma<1$ is nonempty. Degenerate instances silently included by the quantifiers:

• $N = 0$: $\mathcal{J} = \prod_{i \in \varnothing} S_i$ is a one-element type, so $P$ is the $1\times1$ matrix $[1]$ (forced by row sums), the empty tensor product is the constant $1$, and both sides of the equivalence hold.
• Some $S_i$ empty with $N \ge 1$: then $\mathcal{J}$ is empty, $P$ is the unique matrix on the empty index type, the transition-matrix condition holds vacuously, and both sides hold (the zero matrix serves as a transition matrix on an empty $S_i$, and a uniform one on each nonempty $S_j$), so the equivalence again holds trivially. Nothing in the statement asserts that $(1-\gamma)(I-\gamma P)^{-1}$ is itself a transition matrix, nor any quantitative relation between the two separable decompositions.

Behaviour of the inverse on non-invertible arguments, and whether a hypothesis rules it out. $(\cdot)^{-1}$ is Mathlib's total matrix inversion: $A^{-1} := \operatorname{Ring.inverse}(\det A)\cdot \operatorname{adj}(A)$, where $\operatorname{Ring.inverse}$ maps non-units to $0$. Over $\mathbb{R}$ this means: if $\det A = 0$ then $A^{-1}$ is the zero matrix — a junk value returned silently rather than an error — and in that case the right-hand side of the equivalence would read "the zero matrix is separable". No hypothesis of this theorem explicitly states that $I - \gamma P$ is invertible; there is no IsUnit (1 - γ • P).det assumption. Invertibility is instead a mathematical consequence of the hypotheses that are present: with $P$ row-stochastic and $0<\gamma<1$, the matrix $I - \gamma P$ has diagonal entries $1 - \gamma P_{p,p} \ge 1-\gamma > 0$ and off-diagonal absolute row sums $\gamma\sum_{q\neq p}P_{p,q} = \gamma(1-P_{p,p})$, and $1-\gamma P_{p,p} > \gamma(1-P_{p,p})$ exactly because $\gamma < 1$; strict diagonal dominance gives $\det(I-\gamma P)\neq 0$ (and on an empty $\mathcal{J}$ the determinant is the empty product $1$). So the junk branch is unreachable under the stated hypotheses, but only derivably so, not by assumption.