Read-back — markov_entanglement_multi.lean

All declarations live in the namespace MarkovEntanglement and are definitions only: the file contains no theorem, no lemma, and no proof. Nothing below is asserted to hold; each item merely introduces a name for a term or for a predicate. Doc-comments in the source (e.g. claims that a quantity "is a norm", "is zero exactly when the reward decomposes", or that a construction "is the right notion") are prose annotations and carry no formal content; they are not part of what the code asserts and are not reproduced as claims here.

Standing context

The file is developed under the ambient variables

• $N \in \mathbb{N}$ — the number of agents, indexed by $i \in \mathrm{Fin}\,N = \{0,1,\dots,N-1\}$;
• $S : \mathrm{Fin}\,N \to \mathbf{Type}$ — a family of local state–action types, one per agent;
• the typeclass assumptions $S_i$ is a finite type for every $i$ and $S_i$ has decidable equality for every $i$.

These are implicit (respectively instance) arguments of every declaration below whose statement mentions $S$; they are not arguments of muNorm, muTVDist or transitionSpan, which carry their own index-type assumptions. No declaration assumes that $N > 0$, that any $S_i$ is nonempty, or that any $S_i$ is inhabited.

The only object imported from the two-agent file and actually used here is

$$\mathrm{IsTransitionMatrix}(P) \;:\equiv\; \Big(\forall i,j:\; P_{ij} \ge 0\Big) \;\wedge\; \Big(\forall i:\; \textstyle\sum_j P_{ij} = 1\Big),$$

i.e. a square real matrix over a finite index type with nonnegative entries whose every row sums to $1$. (The imported file also supplies IsPositiveDist, IsStationary, IsBellmanQ, tvDist, marginalA/marginalB, IsLocalTransitionA/B, tensorProd, IsSeparable, agentTVDistA/B, entanglementA/B; none of these are referenced in this file.) Throughout, "matrix over $X$" means a function $X \times X \to \mathbb{R}$; no finiteness or stochasticity of a matrix is ever assumed unless IsTransitionMatrix is explicitly invoked. Real-valued infima are taken with Mathlib's $\inf$ on $\mathbb{R}$, which returns the junk value $0$ when the set is empty or is not bounded below.

---

1. Joint

Assumptions: $N$ (implicit); $S$ explicit; the two family-wide typeclass assumptions on $S$.

$\mathrm{Joint}(S)$ is an abbreviation for the dependent product type

$$\mathrm{Joint}(S) \;=\; \prod_{i \in \mathrm{Fin} N} S_i,$$

i.e. the type of functions $p$ assigning to each agent $i$ a local state–action pair $p_i \in S_i$. It is a plain type abbreviation and asserts nothing.

Degenerate cases. If $N = 0$ the product is over the empty index set, so $\mathrm{Joint}(S)$ is a one-element type (the empty function), not empty. If some $S_j$ is empty, $\mathrm{Joint}(S)$ is empty, and then every function out of it is the unique empty function and every sum indexed by it is $0$.

2. tensorProdN

Assumptions: $N$, $S$ implicit; $S_i$ finite with decidable equality for each $i$. Input: a family $P = (P^{(i)})_{i}$ where $P^{(i)}$ is a matrix over $S_i$ — with no hypothesis that any $P^{(i)}$ is a transition matrix.

The definition produces the matrix over $\mathrm{Joint}(S)$

$$\bigl(\mathrm{tensorProdN}(P)\bigr)_{p,q} \;=\; \prod_{i \in \mathrm{Fin} N} P^{(i)}_{p_i,\, q_i}, \qquad p,q \in \mathrm{Joint}(S).$$

Degenerate cases. For $N = 0$ the product is empty and equals $1$, so the result is the $1 \times 1$ matrix with entry $1$ on the singleton $\mathrm{Joint}(S)$, regardless of $P$. Entries may be negative or exceed $1$, since the $P^{(i)}$ are arbitrary real matrices.

3. IsSeparableN

Assumptions: $N$, $S$ implicit; $S_i$ finite with decidable equality for each $i$. Input: a matrix $P$ over $\mathrm{Joint}(S)$, arbitrary (not assumed stochastic, nonnegative, or anything else).

$P$ is separable means: there exist a natural number $K$, real coefficients $x_0,\dots,x_{K-1}$, and for each $k < K$ a family $(P^{(k,i)})_{i}$ of matrices $P^{(k,i)}$ over $S_i$, such that

1. every $P^{(k,i)}$ is a transition matrix: $P^{(k,i)}_{st} \ge 0$ for all $s,t$ and $\sum_t P^{(k,i)}_{st} = 1$ for all $s$;
2. $\sum_{k<K} x_k = 1$;
3. exact matrix equality

$$P_{p,q} \;=\; \sum_{k<K} x_k \prod_{i} P^{(k,i)}_{p_i,\,q_i} \quad \text{for all } p,q \in \mathrm{Joint}(S).$$

The coefficients $x_k$ are only required to sum to $1$; they may be negative and are not required to lie in $[0,1]$, so this is an affine (not convex) combination. The word "entangled" appears only in the doc-comment; no separate predicate for it is defined.

Degenerate cases. $K$ ranges over all of $\mathbb{N}$ including $K = 0$, but $K = 0$ forces $0 = 1$, so any witness has $K \ge 1$. If $N = 0$, $\mathrm{Joint}(S)$ is a singleton and the condition reduces to $P_{\ast\ast} = \sum_k x_k \cdot 1 = 1$; so the predicate holds precisely for the $1\times 1$ matrix $[1]$. If some $S_j$ is empty, then $\mathrm{Joint}(S)$ is empty, every matrix over it is the unique empty matrix, condition 1 is vacuous for that $j$, and the predicate holds for the unique $P$ (take $K=1$, $x_0=1$).

4. muNorm

Assumptions: an arbitrary type $\iota$ with the assumption that $\iota$ is finite; no decidability assumption; $S$, $N$ play no role. Inputs: two functions $\mu, x : \iota \to \mathbb{R}$.

$$\mathrm{muNorm}(\mu, x) \;=\; \sum_{i \in \iota} \mu_i \,|x_i|.$$

Degenerate cases. $\mu$ is an arbitrary real function: it is not assumed nonnegative, nor normalized to sum to $1$. If some $\mu_i < 0$ the value can be negative and the quantity is neither a norm nor a seminorm. If $\iota$ is empty the value is $0$ for all inputs.

5. muTVDist

Assumptions: an arbitrary finite type $\iota$; no decidability assumption. Inputs: $\mu : \iota \to \mathbb{R}$ and two matrices $P, Q$ over $\iota$, neither assumed stochastic.

$$\mathrm{muTVDist}(\mu, P, Q) \;=\; \sum_{i \in \iota} \mu_i \left( \tfrac12 \sum_{j \in \iota} \bigl|P_{ij} - Q_{ij}\bigr| \right).$$

This is a $\mu$-weighted sum over rows of the row-wise total variation distance, in contrast to the imported tvDist, which takes a supremum over rows.

Degenerate cases. $\mu$ is unconstrained (may be negative, may not sum to $1$), so the value can be negative and can fail symmetry-independent properties of a metric such as nonnegativity; it is symmetric in $P,Q$ and vanishes when $P = Q$ regardless of $\mu$. Empty $\iota$ gives $0$. This definition is not used by any other declaration in the file.

6. marginalN

Assumptions: $N$, $S$ implicit; $S_i$ finite (needed to sum over $\mathrm{Joint}(S)$) and $S_i$ decidably equal (needed for the test $q_i = t$). Inputs: an agent index $i \in \mathrm{Fin}\,N$, a matrix $P$ over $\mathrm{Joint}(S)$ (arbitrary), a joint point $p \in \mathrm{Joint}(S)$, and $t \in S_i$.

$$\mathrm{marginalN}(i, P, p, t) \;=\; \sum_{q \in \mathrm{Joint}(S)} \begin{cases} P_{p,q} & \text{if } q_i = t \\ 0 & \text{otherwise}\end{cases} \;=\; \sum_{\substack{q \in \mathrm{Joint}(S) \\ q_i = t}} P_{p,q}.$$

Degenerate cases. No stochasticity is required of $P$, so this can be any real number. If $\mathrm{Joint}(S)$ is empty (some $S_j$ empty) the value is $0$. If $N = 0$ the index $i \in \mathrm{Fin}\,0$ cannot be supplied, so the definition is vacuous in that case.

7. marginalDist

Assumptions: as in item 6. Inputs: an agent index $i$, a function $\mu : \mathrm{Joint}(S) \to \mathbb{R}$ (arbitrary — not assumed nonnegative or normalized), and $s \in S_i$.

$$\mathrm{marginalDist}(i, \mu, s) \;=\; \sum_{\substack{q \in \mathrm{Joint}(S) \\ q_i = s}} \mu_q .$$

Degenerate cases. May be negative or zero for arbitrary $\mu$; equals $0$ when $\mathrm{Joint}(S)$ is empty.

8. IsLocalTransitionN

Assumptions: $N$, $S$ implicit; $S_i$ finite with decidable equality. Inputs: an agent index $i \in \mathrm{Fin}\,N$; a matrix $P$ over $\mathrm{Joint}(S)$; a function $\mu : \mathrm{Joint}(S) \to \mathbb{R}$; a matrix $P^{(i)}$ over $S_i$. None of $P$, $\mu$, $P^{(i)}$ is assumed stochastic, nonnegative, or normalized.

The predicate holds iff for all $s, t \in S_i$,

$$\left(\sum_{\substack{q \in \mathrm{Joint}(S)\\ q_i = s}} \mu_q\right) \cdot P^{(i)}_{s,t} \;=\; \sum_{\substack{p \in \mathrm{Joint}(S)\\ p_i = s}} \mu_p \left( \sum_{\substack{q \in \mathrm{Joint}(S)\\ q_i = t}} P_{p,q} \right),$$

i.e. the $\mu$-marginal weight at $s$ times the candidate local entry equals the $\mu$-weighted marginal flow from the fibre $\{p : p_i = s\}$ into the fibre $\{q : q_i = t\}$. It is stated multiplicatively; no division occurs.

Degenerate cases. For any $s$ with vanishing marginal $\sum_{q_i = s}\mu_q = 0$, the left side is $0$ for every candidate value of $P^{(i)}_{s,\cdot}$, so the row $P^{(i)}_{s,\cdot}$ is completely unconstrained by the predicate at that $s$ (while the right side is then forced to be $0$, a condition on $P$ and $\mu$ alone that may be unsatisfiable, making the predicate hold for no $P^{(i)}$ at all). If $\mu \equiv 0$ the predicate reduces to requiring the right-hand side to vanish identically, again leaving $P^{(i)}$ arbitrary. If $S_i$ is empty the predicate is vacuously true. If $\mathrm{Joint}(S)$ is empty both sides are $0$ and the predicate is true for every $P^{(i)}$.

9. muAgentTVDistN

Assumptions: $N$, $S$ implicit; $S_i$ finite with decidable equality. Inputs: an agent index $i$; $\mu : \mathrm{Joint}(S) \to \mathbb{R}$ (arbitrary); $P$ a matrix over $\mathrm{Joint}(S)$ (arbitrary); $P^{(i)}$ a matrix over $S_i$ (arbitrary).

$$\mathrm{muAgentTVDistN}(i,\mu,P,P^{(i)}) \;=\; \sum_{p \in \mathrm{Joint}(S)} \mu_p \left( \tfrac12 \sum_{t \in S_i} \left| \sum_{\substack{q \in \mathrm{Joint}(S)\\ q_i = t}} P_{p,q} \;-\; P^{(i)}_{p_i,\,t} \right| \right).$$

That is, at each joint point $p$ one compares the marginal row of $P$ onto agent $i$'s coordinate with the row of $P^{(i)}$ indexed by $p_i$, takes half the $\ell^1$ discrepancy, and averages these with weights $\mu_p$ (a weighted sum, not a maximum).

Degenerate cases. With arbitrary $\mu$ the value can be negative. If $S_i$ or $\mathrm{Joint}(S)$ is empty the value is $0$.

10. entanglementWith

Assumptions: $N$, $S$ implicit; $S_i$ finite with decidable equality. Inputs: a completely arbitrary function $d$ taking two matrices over $\mathrm{Joint}(S)$ to a real number — it is not assumed symmetric, nonnegative, or to satisfy any metric axiom — and a matrix $P$ over $\mathrm{Joint}(S)$.

$$\mathrm{entanglementWith}(d, P) \;=\; \inf\, \bigl\{\, r \in \mathbb{R} \;\bigm|\; \exists\, Q \text{ a matrix over } \mathrm{Joint}(S),\ Q \text{ separable in the sense of item 3, and } r = d(P,Q) \,\bigr\},$$

the infimum of the values $d(P,Q)$ as $Q$ ranges over separable joint transitions, with $P$ in the first argument of $d$.

Degenerate cases. The infimum is the real-number $\inf$, which returns the junk value $0$ whenever the set is empty or unbounded below. Since $d$ is arbitrary, the set is in general not bounded below, so the value can be $0$ by convention rather than by any minimization. When $N = 0$ the only separable matrix is $[1]$ on the singleton joint space, so the value is $d(P,[1])$. When some $S_j$ is empty, $P$ and $Q$ are both the unique empty matrix and the value is $d(P,P)$.

11. entanglementN

Assumptions: $N$, $S$ implicit; $S_i$ finite with decidable equality. Inputs: an agent index $i \in \mathrm{Fin}\,N$; $\mu : \mathrm{Joint}(S) \to \mathbb{R}$ (arbitrary, not assumed a distribution); a matrix $P$ over $\mathrm{Joint}(S)$ (arbitrary).

$$\mathrm{entanglementN}(i,\mu,P) \;=\; \inf\Bigl\{\, r \in \mathbb{R} \;\Bigm|\; \exists\, P^{(i)} \text{ a matrix over } S_i \text{ with } P^{(i)}_{st}\ge 0 \text{ and } \sum_t P^{(i)}_{st}=1 \ \forall s,\ \text{ and } r = \mathrm{muAgentTVDistN}(i,\mu,P,P^{(i)}) \Bigr\},$$

with $\mathrm{muAgentTVDistN}$ as spelled out in item 9. Note the ranging object is required to be a genuine transition matrix, whereas $P$ and $\mu$ are unconstrained.

Degenerate cases. Again the real $\inf$ with the junk-value-$0$ convention on empty or unbounded-below sets. If $\mathrm{Joint}(S)$ is empty the set is $\{0\}$ and the value is $0$. If $S_i$ is empty, the unique matrix over $S_i$ is vacuously a transition matrix, so the infimum is over a single point. The definition takes an infimum over a set of reals rather than an indexed infimum over the subtype of transition matrices (unlike the imported two-agent entanglementA/entanglementB, which use the latter).

12. IsValueDecomposition

Assumptions: $N$, $S$ implicit; $S_i$ finite with decidable equality. Inputs: $Q : \mathrm{Joint}(S) \to \mathbb{R}$ and a family $Q^{(i)} : S_i \to \mathbb{R}$ — the local functions are given, not existentially quantified.

The predicate holds iff

$$Q(p) \;=\; \sum_{i \in \mathrm{Fin} N} Q^{(i)}(p_i) \qquad \text{for all } p \in \mathrm{Joint}(S).$$

Degenerate cases. If $N = 0$ the right-hand sum is empty, so the predicate says $Q \equiv 0$ on the singleton joint space. If $\mathrm{Joint}(S)$ is empty the predicate is vacuously true for all $Q$ and all $Q^{(i)}$.

13. IsProductTransition

Assumptions: $N$, $S$ implicit; $S_i$ finite with decidable equality. Inputs: a matrix $P$ over $\mathrm{Joint}(S)$ and a given family $P^{\ell,(i)}$ of matrices over $S_i$ (existentially quantified nowhere; and not assumed to be transition matrices).

The predicate holds iff $P$ equals the tensor product of item 2, i.e.

$$P_{p,q} \;=\; \prod_{i} P^{\ell,(i)}_{p_i,\,q_i} \qquad \text{for all } p,q \in \mathrm{Joint}(S).$$

Degenerate cases. With $N = 0$ this says $P_{\ast\ast} = 1$. With $\mathrm{Joint}(S)$ empty it is vacuously true. Since no stochasticity is required of $P^{\ell,(i)}$, this is exact equality of arbitrary real matrices with an entrywise product formula. Nothing in the definition mentions actions, action constraints, or coupling, despite the doc-comment.

14. JointZ

Assumptions: $N$ implicit; $S$ and $Z$ explicit; the family typeclass assumptions on $S$ (no assumption on $Z$ at this declaration).

An abbreviation for the product type

$$\mathrm{JointZ}(S, Z) \;=\; \Bigl(\prod_{i} S_i\Bigr) \times Z,$$

pairs consisting of a joint local configuration and one extra "global" coordinate in $Z$. It is a type abbreviation and asserts nothing.

15. marginalZ

Assumptions: $N$, $S$ implicit with $S_i$ finite and decidably equal; additionally $Z$ implicit with $Z$ finite and decidably equal. Inputs: an agent index $i \in \mathrm{Fin}\,N$; a matrix $P$ over $\mathrm{JointZ}(S,Z)$ (arbitrary); a point $p \in \mathrm{JointZ}(S,Z)$; and a target pair $t = (t_1, t_2) \in S_i \times Z$.

$$\mathrm{marginalZ}(i,P,p,t) \;=\; \sum_{\substack{q \in \mathrm{JointZ}(S,Z)\\ q^{\text{loc}}_i = t_1 \ \wedge\ q^{\text{glob}} = t_2}} P_{p,q},$$

i.e. the total mass that $P$ assigns from $p$ to all joint successors whose agent-$i$ local coordinate is $t_1$ and whose global coordinate is $t_2$, marginalizing over all other agents' coordinates.

Degenerate cases. Arbitrary sign and magnitude, since $P$ is unconstrained; equals $0$ if $Z$ or some $S_j$ is empty. This definition is not used by any other declaration in the file, and no shared-global-coordinate analogue of separability, local transition, or entanglement is defined.

16. IsDecomposableReward

Assumptions: $N$, $S$ implicit; $S_i$ finite with decidable equality. Input: $r : \mathrm{Joint}(S) \to \mathbb{R}$.

The predicate holds iff there exists a family of local functions $r^{(i)} : S_i \to \mathbb{R}$ such that

$$r(p) \;=\; \sum_{i \in \mathrm{Fin} N} r^{(i)}(p_i) \qquad \text{for all } p \in \mathrm{Joint}(S).$$

(The same shape as item 12, but with the local pieces existentially quantified rather than supplied.)

Degenerate cases. With $N = 0$ it says $r \equiv 0$ on the singleton joint space. With $\mathrm{Joint}(S)$ empty it is vacuously true for every $r$.

17. rewardEntanglement

Assumptions: $N$, $S$ implicit; $S_i$ finite with decidable equality. Inputs: $\mu : \mathrm{Joint}(S) \to \mathbb{R}$ (arbitrary — no nonnegativity, no normalization) and $r : \mathrm{Joint}(S) \to \mathbb{R}$.

$$\mathrm{rewardEntanglement}(\mu, r) \;=\; \inf\Bigl\{\, c \in \mathbb{R} \;\Bigm|\; \exists\, (r^{(i)} : S_i \to \mathbb{R})_{i},\ \ c = \sum_{p \in \mathrm{Joint}(S)} \mu_p \,\Bigl| r(p) - \sum_{i} r^{(i)}(p_i) \Bigr| \,\Bigr\},$$

using $\mathrm{muNorm}$ of item 4 applied to the residual $p \mapsto r(p) - \sum_i r^{(i)}(p_i)$. The local pieces $r^{(i)}$ range over all real-valued functions, with no boundedness or sign constraint.

Degenerate cases. The set is nonempty (take $r^{(i)} \equiv 0$), but with a $\mu$ having any negative value the set is in general unbounded below, in which case the real $\inf$ returns its junk value $0$; the same junk value $0$ is returned in the genuinely-zero cases, so the two are indistinguishable from the definition alone. If $\mathrm{Joint}(S)$ is empty the value is $0$. If $N = 0$ the residual is $r(\ast) - 0$ and the value is $\mu_\ast\,|r(\ast)|$.

18. transitionSpan

Assumptions: an arbitrary type $\iota$ assumed finite and decidably equal; this declaration does not mention $N$ or $S$.

$$\mathrm{transitionSpan}(\iota) \;=\; \operatorname{span}_{\mathbb{R}} \bigl\{\, P \in \mathbb{R}^{\iota \times \iota} \;\bigm|\; P_{ij} \ge 0 \ \forall i,j \ \text{ and } \ \textstyle\sum_j P_{ij} = 1 \ \forall i \,\bigr\},$$

the $\mathbb{R}$-linear span (as a submodule of the space of all real $\iota \times \iota$ matrices) of the set of transition matrices. Arbitrary real coefficients are allowed — no constraint that they sum to $1$, unlike the affine condition in item 3.

Degenerate cases. If $\iota$ is empty, the ambient matrix space is the zero module and the span is the whole (trivial) space. If $\iota$ is nonempty, the set spanned is nonempty. This declaration is not used by any other declaration in the file.