Read-back: local_stationary_eq_marginal

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

$$\mathcal{J} \;=\; \prod_i S_i \;=\; \{\,p : p \text{ assigns to each index } i \text{ an element } p_i \in S_i\,\}$$

for the joint space (Joint S), a finite type with decidable equality. The statement quantifies over: a real matrix $P$ indexed by $\mathcal{J}\times\mathcal{J}$; a real-valued function $\mu$ on $\mathcal{J}$; an index $i$; and a real matrix $P^{(i)}$ indexed by $S_i \times S_i$; subject to four hypotheses (all unfolded below). Its conclusion is a single equation scheme: the marginal of $\mu$ onto coordinate $i$ is a stationary distribution of $P^{(i)}$, i.e.

$$\forall\, t \in S_i: \qquad \sum_{s \in S_i} \big(\mu\!\restriction_i\! s\big)\, P^{(i)}_{s,t} \;=\; \mu\!\restriction_i\! t ,$$

where $\mu\!\restriction_i$ denotes the marginal defined below. Note that "is stationary" here is only this left-eigenvector equation with eigenvalue $1$: it carries no nonnegativity claim, no claim that the entries sum to $1$, and no uniqueness claim.

Every non-standard notion, unfolded.

• Marginal of the measure onto coordinate $i$ (marginalDist): for $s \in S_i$,

$$\mu\!\restriction_i\! s \;=\; \sum_{q \in \mathcal{J}} \big[\,q_i = s\,\big]\,\mu(q),$$

the sum of $\mu$ over all joint points whose $i$-th coordinate is $s$ (the bracket is $1$ if the condition holds and $0$ otherwise).

• Marginal of the transition onto coordinate $i$ (marginalN): for $p \in \mathcal{J}$ and $t \in S_i$,

$$m_i(P)(p,t) \;=\; \sum_{q \in \mathcal{J}} \big[\,q_i = t\,\big]\, P_{p,q},$$

the probability mass that the row of $P$ at $p$ puts on the event "coordinate $i$ lands on $t$".

• Hypothesis 1 — $P$ is a transition matrix (IsTransitionMatrix): $P_{p,q} \ge 0$ for all $p,q \in \mathcal{J}$, and $\sum_{q\in\mathcal{J}} P_{p,q} = 1$ for every $p$. (Row-stochastic only; no irreducibility, aperiodicity, or strict positivity.)

• Hypothesis 2 — $\mu$ is a strictly positive distribution (IsPositiveDist): $\mu(p) > 0$ for every $p \in \mathcal{J}$ (strict, everywhere), and $\sum_{p\in\mathcal{J}} \mu(p) = 1$.

• Hypothesis 3 — $\mu$ is stationary for $P$ (IsStationary): $\sum_{p \in \mathcal{J}} \mu(p)\,P_{p,q} = \mu(q)$ for every $q \in \mathcal{J}$.

• Hypothesis 4 — $P^{(i)}$ is the local (marginalised) transition of agent $i$ induced by $P$ under $\mu$ (IsLocalTransitionN), stated in the scaled, division-free form:

$$\forall\, s,t \in S_i: \qquad \big(\mu\!\restriction_i\! s\big)\, P^{(i)}_{s,t} \;=\; \sum_{p\in\mathcal{J}} \big[\,p_i = s\,\big]\,\mu(p)\; m_i(P)(p,t).$$

Both sides are multiplied through by the marginal weight, so no division occurs anywhere in the statement.

Constrained vs. free variables in the conclusion. Every variable occurring in the conclusion — $N$, the family $S$, the two typeclass instances, $\mu$, $i$, and $P^{(i)}$ — is bound by a binder of the theorem, and $t$ (and $s$) inside the stationarity equation are bound by its own universal quantifier; the conclusion contains no free variables. The joint matrix $P$ does not appear in the conclusion, but it is bound and it is what constrains $P^{(i)}$ through Hypothesis 4. Importantly, $P^{(i)}$ carries no hypothesis of its own beyond Hypothesis 4: it is never assumed to have nonnegative entries or rows summing to $1$; it is an arbitrary real $S_i\times S_i$ matrix satisfying the displayed scaled identity. Because $\mu$ is strictly positive and (see below) each $S_j$ is nonempty, every marginal weight $\mu\!\restriction_i\! s$ is strictly positive, so Hypothesis 4 in fact pins $P^{(i)}$ down uniquely as $P^{(i)}_{s,t} = \big(\sum_p [p_i=s]\mu(p)\,m_i(P)(p,t)\big)/\mu\!\restriction_i\! s$.

Joint satisfiability and degenerate cases. The hypotheses are jointly satisfiable, so the statement is not vacuous. A witness: any $N \ge 1$ with all $S_j$ nonempty and finite, $P$ the uniform stochastic matrix on $\mathcal{J}$, $\mu$ the uniform distribution on $\mathcal{J}$ (strictly positive, sums to $1$, stationary for $P$), any index $i$, and $P^{(i)}$ the uniform stochastic matrix on $S_i$, which satisfies Hypothesis 4. More generally, given any $P$ and any strictly positive stationary $\mu$, a matrix $P^{(i)}$ satisfying Hypothesis 4 always exists (by the division formula above, whose denominators are positive). Degenerate configurations that the quantifiers silently exclude or include:

• The hypothesis $\sum_{p}\mu(p) = 1$ forces $\mathcal{J}$ to be nonempty (an empty sum would be $0$), hence forces every $S_j$ to be nonempty.
• The binder $i \in \{0,\dots,N-1\}$ can only be instantiated when $N \ge 1$; for $N = 0$ no such $i$ exists and the statement says nothing.
• Since every $S_j$ is nonempty, for each $s \in S_i$ there is at least one $p \in \mathcal{J}$ with $p_i = s$, so $\mu\!\restriction_i\! s > 0$; no marginal weight can vanish under these hypotheses.

Matrix inversion. No matrix inverse, no division, and no Ring.inverse occurs anywhere in this statement or in any of the definitions it unfolds to; the entire statement is built from finite sums, products of reals, and indicator functions. Consequently the question of what inversion returns on a non-invertible argument does not arise here, and no hypothesis is needed to rule it out. The only operations that could in principle produce junk values in Lean — division and subtraction on $\mathbb{N}$ — are absent: Hypothesis 4 is deliberately written in multiplied-through form precisely so that no quotient by a possibly-zero marginal appears.