Proofs Theorems 2,3

Theorem 2: Acausal Commutative Square: The following diagram commutes for any belief function $Θ$ . Any infradistribution $D$ where $D = ⊤_{Π} ⋉ (λ π . u_{{π}}^{1} (D))$ also makes this diagram commute and induces a belief function.

Here's how the proof proceeds. In order to show that the full diagram commutes, we first select properties on the four corners such that for each morphism, if the source fulfills the relevant property, then the target fulfills the relevant property. Obviously, the property for the bottom-right corner must be "is a belief function". There are eight phases for this, some of which are quite easy, but the two most difficult are at the start, corresponding to the two morphisms on the bottom side, because we must exhaustively verify the belief function conditions and infradistribution conditions. As usual, lower-semicontinuity is the trickiest part to show. Then, since we have four sides of the square to show are isomorphisms, we have another eight phases where we verify going forward to a different corner and back is identity. Finally, there's an easy step where we rule out that going around in a loop produces a nontrivial automorphism, by showing that both paths from first-person static to third-person dynamic are equal.

First, let's define our properties.

The property for third-person static is $D = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D)))$ , and $D$ is an infradistribution.

The property for third-person dynamic is $ψ_{T} = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (ψ_{T})))$ , and $\to_{T} (π, a o h) = δ_{a, o, (π_{a o}, h)}$ , and $ψ_{T}$ is an infradistribution.

The property for first-person static is that $Θ$ is a belief function.

The property for first-person dynamic is $ψ_{F} = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (ψ_{F})))$ , and $\to_{F} ((π, a o h), a^{'}) = δ_{o, (π_{a o}, h)}$ when $a^{'} = a$ , and $⊥$ when $a^{'} \neq a$ , and $ψ_{F}$ is an infradistribution.

T2.1 Our first step is showing that all 8 morphisms induce the relevant property in the target if the source has the property.

T2.1.1 3-static to 1-static. Our definition is

$Θ (π) := p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D))$

and we must check the five conditions of a belief function for $Θ$ , assuming $D$ is an infradistribution on $P D$ and it has the property $D = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D)))$

T2.1.1.1 First, bounded Lipschitz constant. Our proof goal is

$\exists λ^{⊙} < \infty \forall π^{'}, U, U^{'} : | Θ (π) (U) - Θ (π) (U^{'}) | \leq λ^{⊙} d (U, U^{'})$

Let $λ^{⊙}$ be the Lipschitz constant of $D$ , which is finite because $D$ is an infradistribution. Then let $π^{'}, U, U^{'}$ be arbitrary (they must be bounded-continuous, though). We have

$| Θ (π^{'}) (U) - Θ (π^{'}) (U^{'}) | = | p r_{(A \times O)^{ω} *} (u_{{π^{'}}}^{1} (D)) (U) - p r_{(A \times O)^{ω} *} (u_{{π^{'}}}^{1} (D)) (U^{'}) |$

and then unpack the projection to get

$= | u_{{π^{'}}}^{1} (D)) (λ π, h . U (h)) - u_{{π^{'}}}^{1} (D)) (λ π, h . U^{'} (h)) |$

and unpack the update to get

$= | D (λ π, h . 1_{π = π^{'}} U (h) + 1_{π \neq π^{'}}) - D (λ π, h . 1_{π = π^{'}} U^{'} (h) + 1_{π \neq π^{'}}) |$

and then by Lipschitzness for $D$ ,

$\leq λ^{⊙} {sup}_{π, h \sim π} | 1_{π = π^{'}} U (h) + 1_{π \neq π^{'}} - (1_{π = π^{'}} U^{'} (h) + 1_{π \neq π^{'}}) |$

Now, when $π \neq π^{'}$ , the two functions are equal, so we have

$= λ^{⊙} {sup}_{h \sim π^{'}} | U (h) - U^{'} (h) | \leq λ^{⊙} {sup}_{h} | U (h) - U^{'} (h) | = λ^{⊙} d (U, U^{'})$

We'll leave lower-semicontinuity for the end, it's hard.

T2.1.1.2 Now, normalization, ie ${inf}_{π} Θ (π) (1) = 1 \land {inf}_{π} Θ (π) (0) = 0$ To do this, we have

${inf}_{π} Θ (π) (1) = {inf}_{π} p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D)) (1)$

Then this can be rewritten as

$= ⊤_{Π} (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D)) (1))$

and then as a semidirect product.

$= (⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D))) (1)$

and then, from our defining property for $D$ , and normalization for $D$ since it's an infradistribution, we have

$= D (1) = 1$

The same proof works for 0 as well.

T2.1.1.3 Now, sensible supports. Pick a $π^{'}, U, U^{'}$ where $U$ and $U^{'}$ are identical on histories compatible with $π^{'}$ . We want to show

$Θ (π^{'}) (U) = Θ (π^{'}) (U^{'})$

To start,

$Θ (π^{'}) (U) = p r_{(A \times O)^{ω} *} (u_{{π^{'}}}^{1} (D)) (U)$

and undoing the projection and update, we have

$= D (λ π, h . 1_{π = π^{'}} U (h) + 1_{π \neq π^{'}})$

Remember that actually, $D$ is supported over $P D$ , ie, the subset of $Π \times (A \times O)^{ω}$ where the destiny is compatible with the policy, so when $π = π^{'}$ , $h \sim π = π^{'}$ and so $U$ and $U^{'}$ behave identically. Making this substitution in, we have

$= D (λ π, h . 1_{π = π^{'}} U^{'} (h) + 1_{π \neq π^{'}})$

which then packs up as $Θ (π^{'}) (U^{'})$ and we're done.

T2.1.1.4 Now for agreement on max value. For the $[0, 1]$ type signature on inframeasures, we want to show

$\forall π^{'}, π^{''} : Θ (π^{'}) (1) = Θ (π^{''}) (1)$

Let $π^{'}, π^{''}$ be arbitrary. We have

$Θ (π^{'}) (1) = p r_{(A \times O)^{ω} *} (u_{{π^{'}}}^{1} (D)) (1)$

and then the projection and update unpack to

$D (λ π, h . 1_{π = π^{'}} 1 + 1_{π \neq π^{'}}) = D (1) = D (λ π, h . 1_{π = π^{''}} 1 + 1_{π \neq π^{''}})$

and then, working in reverse from there, we get $= Θ (π^{''}) (1)$ and we're done. For the $R$ type signature, we want to show

$\forall π^{'}, π^{''} : Θ (π^{'}) (\infty) = Θ (π^{''}) (\infty)$

Let $π^{'}, π^{''}$ be arbitrary. We have

$Θ (π^{'}) (\infty) = p r_{(A \times O)^{ω} *} (u_{{π^{'}}}^{\infty} (D)) (\infty)$

which then unpacks as

$D (λ π, h . 1_{π = π^{'}} \infty + 1_{π \neq π^{'}} \infty) = D (\infty) = D (λ π, h . 1_{π = π^{''}} \infty + 1_{π \neq π^{''}} \infty)$

and then, working in reverse, we get $= Θ (π^{''}) (\infty)$ and we're done.

T2.1.1.5 Time to revisit lower-semicontinuity. We want to show that

${liminf}_{n \to \infty} Θ (π_{n}) (U) \geq Θ (π_{\infty}) (U)$

This is going to take some rather intricate work with Propositions 2 and 3, and Theorem 1 from Inframesures and Domain Theory. Namely, the supremum of continuous functions is lower-semicontinuous, any lower-semicontinuous lower-bounded function has an ascending sequence of lower-bounded continuous functions which limits to it pointwise, and for any ascending sequence which limits to a lower-semicontinuous function pointwise, you can shuffle the limit outside of an inframeasure. Fix some continuous bounded $U$ , either in $[0, 1]$ or in $R$ , and sequence of policies $π_{n}$ which converge to $π_{\infty}$ .

Our first task is to establish that the subset of $P D$ where $π = π_{n}$ or $π_{n + 1}$ or $π_{n + 2}$ ... or $π_{\infty}$ is closed. This can be viewed as the following subset of $Π \times (A \times O)^{ω}$ :

$({π_{n}}_{n \geq m} \times (A \times O)^{ω}) \cap {π, h | h \sim π}$

$(A \times O)^{ω}$ is compact, and ${π_{n}}_{n \geq m}$ is compact as well, since it limits to a point and the limit point is included. So that product is a compact set, and must be closed. The latter set is $P D$ itself. And so, since this set is the intersection of a closed set with $P D$ , it's closed in $P D$ with the subspace topology.

Now, define the functions $u_{\geq m} : P D \to R ⊔ {\infty}$ as follows. If $(π, h)$ has $π = π_{m}$ or $π_{m + 1}$ or $π_{m + 2}$ or... or $π_{\infty}$ , then return $U (h)$ . Otherwise, return 1 (or $\infty$ for the other type signature).

$u_{\infty}$ is the function where, if $π = π_{\infty}$ , return $U (h)$ , otherwise return 1 (or $\infty$ ).

Our first task is to show that all the $u_{\geq m}$ , and $u_{\infty}$ are lower-semicontinuous. This is pretty easy to do. They are 1 (or $\infty$ ) outside of a closed set, and less than that inside the closed set.

Lower-semicontinuity happens because we have one of three cases holding. In the first case, the limit point is outside of the closed set (in the complement open set). Then, at some finite stage and forever afterwards, the sequence is outside closed set of interest, and the sequence becomes just a constant value of 1 (or $\infty$ ), and so liminf equals the value of the limit.

In the second case, the limit point is inside the closed set, and there's a subsequence of policy-tagged destinies which remains within the closed set of interest. The liminf of the original sequence of policy-tagged destinies evaluated by $u_{\geq m}$ equals the liminf of the subsequence which stays in the "safe" closed set, because all other points in the sequence get maximal value according to $u_{\geq m}$ (because they're outside the closed set), so they're irrelevant for evaluating the liminf. Then, inside the closed set, $u_{\geq m}$ acts like $U$ , which is continuous, so the liminf of $u_{\geq m}$ inside the closed set equals the limit of $U$ inside the closed set, which equals $u_{\geq m}$ applied to the limit point (in the closed set)

In the third case, the limit point is inside the closed set, but there's no subsequence of policy-tagged destinies which remains within the closed set of interest. So, after some finite stage, the value of $u_{\geq m}$ is 1 or infinity, so the liminf is high and the value of the limit point is low, and again we get lower-semicontinuity.

Finally, we need to show that $u_{\geq m}$ is an ascending sequence of functions which has $u_{\infty}$ as the pointwise limit. The "ascending sequence" part is easy, because as m increases, $u_{\geq m}$ maps a smaller and smaller set (fewer policies) to the value $U$ reports, and more points to 1 (or infinity).

If $π, h$ has $π = π_{\infty}$ , then regardless of n, $u_{\geq n} (π, h) = U (h) = u_{\infty} (π, h)$ , so that works out. If $π, h$ has $π \neq π_{\infty}$ , then the sequence $π_{n}$ can't hit $π$ infinitely often, otherwise $π = π_{\infty}$ , so after some finite n, $π, h$ drops out of the closed set associated with $u_{\geq n}$ , and we have ${lim}_{n \to \infty} (u_{\geq n} (π, h)) = 1 = u_{\infty} (π, h)$ .

Just one more piece of setup. For each $u_{\geq m}$ , since it's lower-semicontinuous, we can apply our Proposition 3 from the domain theory post to construct an ascending sequence of bounded continuous functions $f_{m, n}$ where ${lim}_{n \to \infty} f_{m, n} = u_{\geq m}$ pointwise.

NOW we can begin showing lower-semicontinuity of $Θ$ .

${liminf}_{n \to \infty} Θ (π_{n}) (U) = {liminf}_{n \to \infty} p r_{(A \times O)^{ω} *} (u_{{π_{n}}}^{1} (D)) (U)$

by how $Θ$ was defined. And then we unpack the projection and update to get

$= {liminf}_{n \to \infty} D (λ π, h . 1_{π = π_{n}} U (h) + 1_{π \neq π_{n}})$

First, we observe that the function inside $D$ is greater than $u_{\geq n}$ , because $u_{\geq n}$ copies $U (h)$ when $π = π_{n}$ or $π_{n + 1}$ or $π_{n + 2}$ ... and is maximal otherwise, while the interior function just copies $U (h)$ when $π = π_{n}$ and is maximal otherwise. So, by monotonicity, we can go

$\geq {liminf}_{n \to \infty} D (u_{\geq n})$

And then, we can use monotonicity again to get

$\geq {liminf}_{n \to \infty} D ({sup}_{m \leq n} f_{m, n})$

Wait, what's this? Well, if $m \leq n$ , then $f_{m, n} \leq u_{\geq m} \leq u_{\geq n}$ , because $f_{m, n}$ was constructed to be an ascending sequence of functions (in n) limiting to $u_{\geq m}$ . And $u_{\geq m}$ is an ascending sequence of functions (in m), so it's below $u_{\geq n}$ . Thus, the function ${sup}_{m \leq n} f_{m, n}$ lies below $u_{\geq n}$ , we just applied monotonicity.

Our next claim is that ${sup}_{m \leq n} f_{m, n}$ is an ascending sequence of continuous functions which limits pointwise to $u_{\infty}$ . Here's how to show it. The functions are continuous because they're all the supremum of finitely many continuous functions $f_{m, n}$ . They ascend because

${sup}_{m \leq n + 1} f_{m, n + 1} \geq {sup}_{m \leq n} f_{m, n + 1} \geq {sup}_{m \leq n} f_{m, n}$

The first inequality was from considering one less function in the sup. the second inequality is because, for all m, $f_{m, n}$ is an ascending sequence of functions in n.

For showing that the sequence ${sup}_{m \leq n} f_{m, n}$ limits (in n) pointwise to $u_{\infty}$ , we fix an arbitrary $m^{*}$ and do

${lim}_{n \to \infty} {max}_{m \leq n} f_{m, n} (π, h) \geq {lim}_{n \to \infty} f_{m^{*}, n} (π, h) = u_{\geq m^{*}} (π, h)$

The inequality is because eventually n goes past the fixed number $m^{*}$ , and then we're selecting a single function out of the supremum of functions. The equality is because $f_{m^{*}, n}$ limits pointwise in $n$ to $u_{\geq m^{*}}$ . Now, with this, we can go:

$u_{\infty} (π, h) = {lim}_{n \to \infty} u_{\geq n} (π, h) = {lim}_{n \to \infty} {max}_{m \leq n} u_{\geq m} (π, h)$

$\geq {lim}_{n \to \infty} {max}_{m \leq n} f_{m, n} (π, h) \geq {sup}_{m^{*}} u_{\geq m^{*}} (π, h) = u_{\infty} (π, h)$

Let's break that down. The first equality was because we showed that $u_{\infty}$ is the pointwise limit of the $u_{\geq n}$ . The second equality is because $u_{\geq m}$ makes an ascending sequence of functions, so the supremum of the functions would just be $u_{\geq n}$ itself. The first inequality is because $f_{m, n} \leq u_{\geq m}$ , it's one of the approximating continuous functions. The second inequality was the thing we showed earlier, about how the limit exceeds $u_{\geq m^{*}} (π, h)$ regardless of $m^{*}$ . Finally, we use again that $u_{\infty}$ is the pointwise limit of the $u_{\geq m^{*}}$ .

We just showed a quantity is greater than or equal to itself, so all these inequalities must be equalities, and we have

$u_{\infty} (π, h) = {lim}_{n \to \infty} {max}_{m \leq n} f_{m, n} (π, h)$

So, the ascending sequence of continuous functions ${sup}_{m \leq n} f_{m, n}$ limits pointwise to $u_{\infty}$ . Now that we have that, let's recap what we've got so far.We have

${liminf}_{n \to \infty} Θ (π_{n}) (U) \geq {liminf}_{n \to \infty} D ({sup}_{m \leq n} f_{m, n})$

Since ${sup}_{m \leq n} f_{m, n}$ is an ascending sequence of continuous functions in $n$ , then by monotonicity of $D$ , that sequence must be increasing, so we have

$= {lim}_{n \to \infty} D ({sup}_{m \leq n} f_{m, n})$

and then, we can apply the monotone convergence theorem for infradistributions, that a sequence of continuous functions ascending pointwise to a lower-semicontinuous function has the limit of the infradistribution expectations equaling the expectation of the lower-semicontinuous supremum, so we have

$= D (u_{\infty}) = D (λ π, h . 1_{π = π_{\infty}} U (h) + 1_{π \neq π_{\infty}})$

and then we pack this back up as an update and projection

$= p r_{(A \times O)^{ω} *} (u_{{π_{\infty}}}^{1} (D)) (U)$

and back up to get

$= Θ (π_{\infty}) (U)$

and lower-semicontinuity of $Θ$ has been shown. So translating over an infradistribution makes a belief function.

T2.1.2 1-static to 3-static.

$D := ⊤_{Π} ⋉ Θ$

Now, we'll show the five infradistribution conditions on $D$ , along with the sixth condition on $D$ that it equals $⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D)))$ .

First, to show it's even well-defined, we have

$D (f) = (⊤_{Π} ⋉ Θ) (f) = ⊤_{Π} (λ π . Θ (π) (λ h . f (π, h)))$

That inner function is lower-semicontinuous in $π$ , because, starting with

${liminf}_{n \to \infty} Θ (π_{n}) (λ h . f (π_{n}, h))$

then we have that, because $f$ is continuous and $Π \times (A \times O)^{ω}$ is compact, $f$ is uniformly continuous. So, as n increases, the function $λ h . f (π_{n}, h)$ uniformly limits to $λ h . f (π_{\infty}, h)$ . Since all the $Θ (π_{n})$ have a uniform upper bound on the Lipschitz constant (from $Θ$ being a belief function) they converge to agreeing that $λ h . f (π_{n}, h)$ has similar value as $λ h . f (π_{\infty}, h)$ , so we get

$= {liminf}_{n \to \infty} Θ (π_{n}) (λ h . f (π_{\infty}, h))$

and then, by lower-semicontinuity for $Θ$ ,

$\geq Θ (π_{\infty}) (λ h . f (π_{\infty}, h))$

So, since the inner function is lower-semicontinuous, it can be evaluated.

T2.1.2.1 Now for the condition that

$D = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D)))$

We start with $D (f)$ and unpack the definition of $D$ , to get

$= (⊤_{Π} ⋉ Θ) (f)$

And unpack the definition of semidirect product and what $⊤_{Π}$ means, to get

$= {inf}_{π} Θ (π) (λ h . f (π, h))$

$= {inf}_{π} {inf}_{π^{'}} Θ (π^{'}) (λ h . 1_{π^{'} = π} f (π, h) + 1_{π^{'} \neq π})$

This step happens because, if $π^{'} \neq π$ , then $Θ (π^{'})$ will be assessing the value of the constant-1 function (or constant-infinity function), and will return a maximal value (by condition 5 on belief functions, that they all agree on the value of 1 (or $\infty$ )). So the only way to minimize that line via a choice of $π^{'}$ is to make it equal to $π$ , as that means that we're evaluating $Θ (π) (λ h . f (π, h))$ instead, which may be less than the maximal value.

Now we pack up what $⊤_{Π}$ means, and the semidirect product, to get

$= {inf}_{π} (⊤_{Π} ⋉ Θ) (λ π^{'}, h . 1_{π^{'} = π} f (π, h) + 1_{π^{'} \neq π})$

Pack up the definition of $D$ to get

$= {inf}_{π} D (λ π^{'}, h . 1_{π^{'} = π} f (π, h) + 1_{π^{'} \neq π})$

Pack up the definition of "1-update on $π$ " to get

$= {inf}_{π} u_{{π}}^{1} (D) (λ π^{'}, h . f (π, h))$

Pack up how projection mappings work, to get:

$= {inf}_{π} p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D)) (λ h . f (π, h))$

Pack up what $⊤_{Π}$ means and the semidirect product to get

$= (⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D)))) (f)$

So we have

$D = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D)))$

as desired, since $f$ was arbitrary.

T2.1.2.2 Now to verify the infradistribution conditions on $D$ . First, monotonicity. Let $f^{'} \geq f$

$D (f^{'}) = (⊤_{Π} ⋉ Θ) (f^{'})$

And unpack the definition of semidirect product and what $⊤_{Π}$ means, to get

$= {inf}_{π} Θ (π) (λ h . f^{'} (π, h))$

Then, by monotonicity for all the $Θ (π)$ , we have

$\geq {inf}_{π} Θ (π) (λ h . f (π, h))$

which packs back up in reverse as $D (f)$ .

T2.1.2.3 Now for concavity. Start with $D (p f + (1 - p) f^{'})$ and unpack in the usual way to get

$= {inf}_{π} Θ (π) (λ h . p f (π, h) + (1 - p) f^{'} (π, h))$

Then, by concavity for the $Θ (π)$ , as they're inframeasures, we have

$\geq {inf}_{π} (p Θ (π) (λ h . f (π, h)) + (1 - p) Θ (π) (λ h . f^{'} (π, h)))$

and distribute the inf

$\geq {inf}_{π} (p Θ (π) (λ h . f (π, h))) + {inf}_{π} ((1 - p) Θ (π) (λ h . f^{'} (π, h)))$

Pulling the constants out, we have

$= p {inf}_{π} (Θ (π) (λ h . f (π, h))) + (1 - p) {inf}_{π} (Θ (π) (λ h . f^{'} (π, h)))$

and packing back up in the usual way, we have

$= p D (f) + (1 - p) D (f^{'})$

Concavity is shown.

T2.1.2.4 For Lipschitzness, we start with $| D (f) - D (f^{'}) |$ and then partially unpack in the usual way to get

$= | ⊤_{Π} (λ π . Θ (π) (λ h . f (π, h))) - ⊤_{Π} (λ π . Θ (π) (λ h . f^{'} (π, h))) |$

And, since $⊤_{Π}$ is a sharp infradistribution, it has a Lipschitz constant of 1, so we have

$\leq {sup}_{π} | Θ (π) (λ h . f (π, h)) - Θ (π) (λ h . f^{'} (π, h)) |$

Since all the $Θ (π)$ have a uniform bound on their Lipschitz constants (one of the belief function conditions), we then have

$\leq {sup}_{π} λ^{⊙} {sup}_{h} | f (π, h) - f^{'} (π, h) |$

which rearranges as

$= λ^{⊙} {sup}_{π, h} | f (π, h) - f^{'} (π, h) | = λ^{⊙} d (f, f^{'})$

and we're done, we got a Lipschitz constant.

T2.1.2.5 The CAS property for $D$ is trival because $P D$ is a closed subset of $Π \times (A \times O)^{ω}$ which is a compact space, and so you can just take all of $P D$ as a compact support.

T2.1.2.6 That just leaves normalization. We have

$D (1) = {inf}_{π} Θ (π) (1) = 1$

$D (0) = {inf}_{π} Θ (π) (0) = 0$

by unpacking $D$ and applying normalization for a belief function.

So now, $D$ is an infradistribution.

T2.1.3 For 3-static to 3-dynamic, we have

$\to_{T} (π, a o h) := δ_{a, o, π_{a o}, h}$ (which fulfills one of the 3-dynamic conditions), and $ψ_{T} := D$

Since $D$ is an infradistribution, $ψ_{T}$ is too, and for the condition on $ψ_{T}$ , we have:

$ψ_{T} = D = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D))) = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (ψ_{T})))$

and we're done, since $D$ had the relevant condition.

T2.1.4 For 3-dynamic to 3-static, we have

$D := p r_{Π \times (A \times O)^{ω} *} (ψ_{T} ⋉ \to_{T : \infty})$

First, we must show that the niceness conditions are fulfilled for the infinite semidirect product to be defined at all. $\to_{T}$ maps $π, a o h$ to $a, o, (π_{a o}, h)$ . This is clearly a continuous mapping, so in particular, it's lower-semicontinuous. Dirac-delta distributions are 1-Lipschitz when interpreted as inframeasures (all probability distributions have that property, actually). The compact-shared-CAS condition is redundant because $A \times O \times P D$ is already a compact space. And all probability distributions (dirac-delta distributions are probability distributions) map constants to the same constant, so we get the increase-in-constants property and the 1 maps to 1 property. So we can indeed take the infinite semidirect product of the $\to_{T}$ .

Now, we'll show that unrolling like this just produces $ψ_{T}$ exactly. We'll use $s_{0}$ for the initial state (pair of policy and destiny, also written as $(π, h)_{0}$ ), and $a o s_{1 : \infty}$ for the successive unrolled history of states, actions, and observations. First, by unpacking $D$ 's definition,

$D (f) = p r_{Π \times (A \times O)^{ω} *} (ψ_{T} ⋉ \to_{T : \infty}) (f)$

Then we unpack the projection and semidirect product

$= ψ_{T} (λ (π, h)_{0} . \to_{T : \infty} ((π, h)_{0}) (λ a o s_{1 : \infty} . f (π, a o_{1 : \infty})))$

And pack things up into a projection

$= ψ_{T} (λ (π, h)_{0} . p r_{(A \times O)^{ω} *} (\to_{T : \infty} ((π, h)_{0})) (λ a o_{1 : \infty} . f (π, a o_{1 : \infty})))$

And then we can observe that unrolling the initial state forever via "advance the destiny 1 step, popping actions and observations off, and advance the policy", when you project down to just the actions and observations (not the intermediate states), yields just the point distribution on that destiny, so we get:

$= ψ_{T} (λ (π, h)_{0} . δ_{h} (λ h^{'} . f (π, h^{'})))$

And then substitute the value of that dirac-delta in to get

$= ψ_{T} (λ π, h . f (π, h)) = ψ_{T} (f)$

So, our $D = ψ_{T}$ . Now we can go

$D = ψ_{T} = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (ψ_{T}))) = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D)))$

and we're done, showing $D$ had the relevant condition from $ψ_{T}$ having it. Since $ψ_{T}$ is an infradistribution, $D$ is too.

T2.1.5 For 3-dynamic to 1-dynamic, we have

$\to_{F} (π, h, a) := p r_{O \times P D *} (u_{{a}}^{1} (\to_{T} (π, h)))$

For the action $π ()$ (which is compatible with the start of the history), we have

$\to_{F} (π, π () o h, π ()) (f)$

Applying our definition, we have

$= p r_{O \times P D *} (u_{{π ()}}^{1} (\to_{T} (π, π () o h))) (f)$

Unpacking the projection, we have (where $s$ is a state)

$= u_{{π ()}}^{1} (\to_{T} (π, π () o h)) (λ a, o, s . f (o, s))$

Unpacking the update, we have

$= \to_{T} (π, π () o h) (λ a, o, s . 1_{a = π ()} f (o, s) + 1_{a \neq π ()})$

And then we consider that $\to_{T} (π, π () o h)$ is just the dirac-delta distribution on $(π (), o, (π_{π () o}, h))$ , so we have

$= δ_{π (), o, (π_{π () o}, h)} (λ a, o, s . 1_{a = π ()} f (o, s) + 1_{a \neq π ()})$

Substitute the values in, and we have

$= f (o, (π_{π () o}, h))$

and then pack up the dirac-delta and we get

$= δ_{o, (π_{π () o}, h)} (f)$

So, $\to_{F} (π, π () o h, π ())$ is just the dirac-delta distribution on $o$ and the pair of $h$ and the policy advanced one step, as it should be. For $a^{'}$ that aren't $π ()$ as it should be, we have

$\to_{F} (π, π () o h, a^{'}) (f)$

Applying our definition, we have

$= p r_{O \times P D *} (u_{{a^{'}}}^{1} (\to_{T} (π, π () o h))) (f)$

Unpacking the projection, we have (where $s$ is a state)

$= u_{{a^{'}}}^{1} (\to_{T} (π, π () o h)) (λ a, o, s . f (o, s))$

Unpacking the update, we have

$= \to_{T} (π, π () o h) (λ a, o, s . 1_{a = a^{'}} f (o, s) + 1_{a \neq a^{'}})$

And then we consider that $\to_{T} (π, π () o h)$ is just the dirac-delta distribution on $(π (), o, (π_{π () o}, h))$ , so we have

$= δ_{π (), o, (π_{π () o}, h)} (λ a, o, s . 1_{a = a^{'}} f (o, s) + 1_{a \neq a^{'}})$

Substitute the values in, and remembering that $a^{'}$ and $π ()$ are assumed to be different, and we have (regardless of $f$ )

$= 1$

Or infinity for the other type signature. Therefore,

$\to_{F} (π, π () o h, a^{'}) = ⊥$

So our transition kernel works out. For the other conditions on $ψ_{F}$ , just observe that $ψ_{F} := ψ_{T}$ , and use the extreme similarity of their defining conditions.

T2.1.6 For 1-dynamic to 3-dynamic, we have $ψ_{T} := ψ_{F}$ so we can use our defining property of $ψ_{F}$ again, clearly show that $ψ_{T}$ has the relevant defining properties, so that just leaves cleaning up the defining property for the $\to_{T}$ infrakernel. We remember that

$\to_{T} (π, h) := ⊤_{A} ⋉ (λ a . \to_{F} (π, h, a))$

Therefore, we have:

$\to_{T} (π, π () o h) (f) = (⊤_{A} ⋉ (λ a . \to_{F} (π, π () o h, a))) (f)$

This occurs because the history must be compatible with the policy. Then, we can unpack as:

$= ⊤_{A} (λ a . \to_{F} (π, π () o h, a) (λ o, s . f (a, o, s)))$

We unpack our $⊤_{A}$ , getting

$= {inf}_{a} (\to_{F} (π, π () o h, a) (λ o, s . f (a, o, s)))$

Then, we observe that for any $a \neq π ()$ , $\to_{F} (π, π () o h, a) = ⊥$ . So, $a$ must be $π ()$ , and we have

$= \to_{F} (π, π () o h, π ()) (λ o, s . f (π (), o, s))$

Now, $\to_{F} (π, π () o h, π ())$ is the dirac-delta distribution on $(o, (h, π_{π () o}))$ , so making that substitution in, we have

$= δ_{o, (h, π_{π () o})} (λ o, s . f (π (), o, s))$

$= f (π (), o, (h, π_{π () o})) = δ_{π (), o, (h, π_{π () o})} (f)$

And this holds for all $f$ , so we get our desired result that

$\to_{T} (π, π () o h) = δ_{π (), o, (h, π_{π () o})}$

T2.1.7 For 1-static to 1-dynamic, we just have

$ψ_{F} := ⊤_{Π} ⋉ Θ$

$\to_{F} (π, a o h, a) := δ_{o, (π_{a o}, h)}$

$\to_{F} (π, a o h, a^{'}) := ⊥$

So this automatically makes the infrakernel have the desired properties. For showing the relevant properties of $ψ_{F}$ , we just copy the proof at the start of getting the properties for $D$ from $Θ$ being a belief function, since $D$ and $ψ_{F}$ are both defined in the same way.

T2.1.8 For 1-dynamic to 1-static, we have

$Θ (π^{'}) := p r_{(A \times O)^{ω} *} ((u_{{π^{'}}}^{1} (ψ_{F})) ⋉ \to_{F : \infty}^{π^{'}})$

We'll work on getting that latter quantity into a better form, but first we have to verify that
$\to_{F : \infty}^{π}$ is even well-defined at all, w need the $\to_{F : n}^{π}$ to fulfill the niceness conditions. They're defined as

$\to_{F : n}^{π} (s_{0}, a o s_{1 : n}) := δ_{π (a o_{1 : n})} ⋉ (λ a . \to_{F} (s_{n}, a))$

For lower-semicontinuity, $\to_{F}$ is lower-semicontinuous, because it returns $⊥$ on every action but one (this is a clopen set), and for the action that pairs up with the initial state, the policy-tagged history just has the history and policy advanced, which is continuous. $\to_{F : n}^{π}$ behaves similarly, continuous variation in input leads to continuous variation in output, because eventually the behavior of the policy settles down to a fixed action as the history of actions and observations stabilizes amongst one of the finitely many options.

For making inframeasures, $\to_{F : n}^{π}$ always returns a dirac-delta distribution or $⊥$ , so we're good there. Similarly, for 1-Lipschitzness, both $⊥$ and dirac-delta distributions are 1-Lipschitz. For compact-shared CAS, as the target space is $A \times O \times P D$ , it's compact and you don't need to worry about that. Finally, both dirac-delta distributions and $⊥$ map constants to either the same constant or higher, and in the $[0, 1]$ type signature, both $⊥$ and dirac-delta distributions map 1 to 1. So all niceness conditions are fulfilled.

Let's work on unpacking the value

$p r_{(A \times O)^{ω} *} ((u_{{π^{'}}}^{1} (ψ_{F})) ⋉ \to_{F : \infty}^{π}) (U)$

unpacking the projection and semidirect product, we get

$= u_{{π^{'}}}^{1} (ψ_{F}) (λ π, h . \to_{F : \infty}^{π^{'}} (π, h) (λ a o s_{1 : \infty} . U (a o_{1 : \infty})))$

And unpacking the update, we have

$= ψ_{F} (λ π, h . 1_{π = π^{'}} \to_{F : \infty}^{π^{'}} (π, h) (λ a o s_{1 : \infty} . U (a o_{1 : \infty})) + 1_{π \neq π^{'}})$

We can make a substitution which changes nothing (in the scope of the indicator function where $π = π^{'}$ ), that

$= ψ_{F} (λ π, h . 1_{π = π^{'}} \to_{F : \infty}^{π^{'}} (π^{'}, h) (λ a o s_{1 : \infty} . U (a o_{1 : \infty})) + 1_{π \neq π^{'}})$

and then we can write this as a projection in the inside

$= ψ_{F} (λ π, h . 1_{π = π^{'}} p r_{(A \times O)^{ω} *} (\to_{F : \infty}^{π^{'}} (π^{'}, h)) (λ a o_{1 : \infty} . U (a o_{1 : \infty})) + 1_{π \neq π^{'}})$

And then we can realize that when we unroll $\to_{F : \infty}^{π^{'}} (π^{'}, h)$ , it just always deterministically unrolls the history, along with the policy, since for $π^{'}, h$ to be an input state, $π^{'}$ must be compatible with $h$ , so picking actions from $π^{'}$ means there's never any action mismatches. Projecting this down to the actions and observations just makes the history $h$ exactly. So we have

$= ψ_{F} (λ π, h . 1_{π = π^{'}} δ_{h} (λ a o_{1 : \infty} . U (a o_{1 : \infty})) + 1_{π \neq π^{'}})$

Substituting the dirac-delta value in, we have

$= ψ_{F} (λ π, h . 1_{π = π^{'}} U (h) + 1_{π \neq π^{'}})$

And we pack the update and projection back up to get

$= p r_{(A \times O)^{ω} *} (u_{{π^{'}}}^{1} (ψ_{F})) (U)$

Since $U$ was arbitrary, we have

$p r_{(A \times O)^{ω} *} ((u_{{π^{'}}}^{1} (ψ_{F})) ⋉ \to_{F : \infty}^{π}) = p r_{(A \times O)^{ω} *} (u_{{π^{'}}}^{1} (ψ_{F}))$

And so, an alternate way to define $Θ (π^{'})$ is as

$= p r_{(A \times O)^{ω} *} (u_{{π^{'}}}^{1} (ψ_{F}))$

We can run through the same proof that $Θ$ is indeed a belief function, back from the 3-static to 1-static case, because $ψ_{F}$ fulfills all the same properties that $D$ did.

Alright, now we have, for all four corners, a condition that's basically "came from an acausal belief function" that is preserved under morphisms. Now we need to show that all 8 back-and-forth directions are identity.

T2.2.1 For 1-static to 3-static back to 1-static, we want to show

$Θ (π^{'}) = p r_{(A \times O)^{ω} *} (u_{{π^{'}}}^{1} (⊤_{Π} ⋉ Θ))$

This is (we assume the hard version first)

$p r_{(A \times O)^{ω} *} (u_{{π^{'}}}^{1} (⊤_{Π} ⋉ Θ)) (U)$

Then unpack the projection and update

$= (⊤_{Π} ⋉ Θ) (λ π, h . 1_{π = π^{'}} U (h) + 1_{π \neq π^{'}})$

Then unpack the semidirect product and $⊤_{Π}$ to get

$= {inf}_{π} Θ (π) (λ h . 1_{π = π^{'}} U (h) + 1_{π \neq π^{'}})$

Then realize that the minimizer is picking $π^{'}$ exactly, otherwise you'd just get maximal value and all the $Θ (π)$ agree on what a maximal input maps to.

$= Θ (π^{'}) (λ h . U (h)) = Θ (π^{'}) (U)$

And we're done.

T.2.2.2 For 3-static to 1-static to 3-static being identity, we want to show

$D = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (D)))$

This is just exactly the condition we're assuming on $D$ , so we trivially fulfill this (the nontrivial part was shoved into showing that going belief-function to infradistribution over policy-tagged states produced this property).

T2.2.3 For 3-static to 3-dynamic back to 3-static, we need to show that

$D = p r_{Π \times (A \times O)^{ω} *} (D ⋉ \to_{T : \infty})$

For this, we abbreviate states beyond the first one as $s$ , so $(h, π)_{0}$ is the initial state, and $a o s_{1 : \infty}$ is an element of $(A \times O \times P D)^{ω}$ . Taking the complicated part, it's

$p r_{Π \times (A \times O)^{ω} *} (D ⋉ \to_{T : \infty}) (f)$

$= (D ⋉ \to_{T : \infty}) (λ (π, h)_{0}, a o s_{1 : \infty} . f (π, a o_{1 : \infty}))$

And then we unpack the semidirect product a bit, to get

$= D (λ (π, h)_{0} . \to_{T : \infty} ((π, h)_{0}) (λ a o s_{1 : \infty} . f (π, a o_{1 : \infty})))$

And then we can write this as a projection, to get

$= D (λ (π, h)_{0} . p r_{(A \times O)^{ω} *} (\to_{T : \infty} ((π, h)_{0})) (λ a o_{1 : \infty} . f (π, a o_{1 : \infty})))$

Now, we observe that because $\to_{T}$ , when repeatedly unrolled, is just emitting the actions and observations from the starting destiny/history, this projection is just the point distribution on the action-observation sequence that is h.

$= D (λ (π, h)_{0} . δ_{h} (λ a o_{1 : \infty} . f (π, a o_{1 : \infty})))$

Then we evaluate the expectation, yielding

$= D (λ π, h . f (π, h)) = D (f)$

And we're done.

T2.2.4 For going 3-dynamic to 3-static to 3-dynamic, we need that

$ψ_{T} = p r_{Π \times (A \times O)^{ω} *} (ψ_{T} ⋉ \to_{T : \infty})$

To show this, just reuse the exact same proof from above, just with $ψ_{T}$ instead of $D$ . Also, $\to_{F} (π, h)$ works out.

At this point, we've established isomorphism for two sides of the square. We've just got two more sides left to address, then showing that going around the square results in identity instead of a nontrivial automorphism.

T2.2.5,6 For translating back and forth between 3-dynamic and 1-dynamic, we observe that both translations keep the initial infradistribution over policy-tagged destinies the same, and our 3-dynamic to 1-dynamic, and 1-dynamic to 3-dynamic proofs verified that the $\to_{F}$ and $\to_{T}$ behave as they should when they go back and forth, so we don't need to worry about this.

T2.2.7 Next is 1-dynamic to 1-static to 1-dynamic. The infrakernel is guaranteed to have the right form, we just need to show that $ψ_{F}$ is unchanged. So, we must show

$ψ_{F} = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} ((u_{{π}}^{1} (ψ_{F})) ⋉ \to_{F : \infty}^{π}))$

But, since our condition on 1-dynamic (that we showed is a property of applying the morphism to go from any belief function to first-person dynamic) was

$ψ_{F} = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (ψ_{F})))$

The only thing we need to show is that, regardless of $π$ ,

$p r_{(A \times O)^{ω} *} ((u_{{π}}^{1} (ψ_{F})) ⋉ \to_{F : \infty}^{π}) = p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (ψ_{F}))$

For if we could show that, then we could go:

$⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} ((u_{{π}}^{1} (ψ_{F})) ⋉ \to_{F : \infty}^{π})) = ⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (ψ_{F}))) = ψ_{F}$

and we'd be done. So, we'll show that

$p r_{(A \times O)^{ω} *} ((u_{{π}}^{1} (ψ_{F})) ⋉ \to_{F : \infty}^{π}) = p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (ψ_{F}))$

instead, as that's all we need. Again, we'll massage the more complicated side until we get it into the simple form for the other side.

$p r_{(A \times O)^{ω} *} ((u_{{π}}^{1} (ψ_{F})) ⋉ \to_{F : \infty}^{π}) (U)$

We undo the projection, and abbreviate states as $s_{0}$ , and action-observation-state sequences as $a o s_{1 : \infty}$ , to yield

$= ((u_{{π}}^{1} (ψ_{F})) ⋉ \to_{F : \infty}^{π}) (λ s_{0}, a o s_{1 : \infty} U (a o_{1 : \infty}))$

Then we reexpress the semidirect product, to yield

$= u_{{π}}^{1} (ψ_{F}) (λ s_{0} . \to_{F : \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U (a o_{1 : \infty})))$

We unpack the initial state a fuzz to yield

$= u_{{π}}^{1} (ψ_{F}) (λ π^{'}, h . \to_{F : \infty}^{π} (π^{'}, h) (λ a o s_{1 : \infty} . U (a o_{1 : \infty})))$

We apply the update to yield

$= ψ_{F} (λ π^{'}, h . 1_{π^{'} = π} \cdot (\to_{F : \infty}^{π} (π^{'}, h) (λ a o s_{1 : \infty} . U (a o_{1 : \infty}))) + 1_{π^{'} \neq π})$

Then, we realize that if $π^{'} = π$ , we can swap $π^{'}$ out for $π$ in the relevant function associated with it.

$= ψ_{F} (λ π^{'}, h . 1_{π^{'} = π} \cdot (\to_{F : \infty}^{π^{'}} (π^{'}, h) (λ a o s_{1 : \infty} . U (a o_{1 : \infty}))) + 1_{π^{'} \neq π})$

Now, we can partially pack this up as a projection, to get

$= ψ_{F} (λ π^{'}, h . 1_{π^{'} = π} \cdot (p r_{(A \times O)^{ω} *} (\to_{F : \infty}^{π^{'}} (π, h)) (U)) + 1_{π^{'} \neq π})$

At this point, we can realize something interesting. $p r_{(A \times O)^{ω} *} (\to_{F : \infty}^{π^{'}} (π^{'}, h))$ is "start with an initial policy of $π^{'}$ and h compatible with $π^{'}$ , then repeatedly feed in actions as if they were created by $π^{'}$ forever, and forget about the states, leaving just the action-observation sequence". Now, since the action (being produced by $π^{'}$ ) always lines up with what the $π^{'}$ encoded in the state would do, this process never hits the $⊥$ infradistribution, it keeps going on and on and advancing the history with no issue. In particular, the history unrolls to completion, and the resulting action-observation sequence you get would just be the original destiny packed up in the state. So, this infradistribution is just $δ_{h}$ . Making this substitution in, we get

$= ψ_{F} (λ π^{'}, h . 1_{π^{'} = π} \cdot δ_{h} (U) + 1_{π^{'} \neq π})$

$= ψ_{F} (λ π^{'}, h . 1_{π^{'} = π} U (h) + 1_{π^{'} \neq π})$

Now we pack up the update again, to get

$= u_{{π}}^{1} (ψ_{F}) (λ π^{'}, h . U (h))$

And then realize that this is a projection, to get

$= p r_{(A \times O)^{ω} *} (u_{{π}}^{1} (ψ_{F})) (U)$

And we're done, we showed our desired result to establish that going first-person dynamic to static back to dynamic is identity.

T2.2.8 Time for the last leg of the square, that going first-person static to first-person dynamic and first-person static is identity. We want to show that, regardless of $π^{'}$ ,

$Θ (π^{'}) = p r_{(A \times O)^{ω} *} ((u_{{π^{'}}}^{1} (⊤_{Π} ⋉ Θ)) ⋉ \to_{F : \infty}^{π^{'}})$

Again, like usual, we'll take the complicated thing and repeatedly rewrite it to reach the simpler thing, for an arbitrary function.

$p r_{(A \times O)^{ω} *} ((u_{{π^{'}}}^{1} (⊤_{Π} ⋉ Θ)) ⋉ \to_{F : \infty}^{π^{'}}) (U)$

Using $s$ for states, we can rewrite the projection, to get

$= ((u_{{π^{'}}}^{1} (⊤_{Π} ⋉ Θ)) ⋉ \to_{F : \infty}^{π^{'}}) (λ s_{0}, a o s_{1 : \infty} . U (a o_{1 : \infty}))$

Then we rewrite the semidirect product, and unpack the initial state into a policy $π$ and destiny h compatible with $π$ , to get

= $u_{{π^{'}}}^{1} (⊤_{Π} ⋉ Θ) (λ π, h . \to_{F : \infty}^{π^{'}} (π, h) (λ a o s_{1 : \infty} . U (a o_{1 : \infty})))$

We can then rewrite the interior as a projection to get

$= u_{{π^{'}}}^{1} (⊤_{Π} ⋉ Θ) (λ π, h . p r_{(A \times O)^{ω} *} (\to_{F : \infty}^{π^{'}} (π, h)) (U))$

Now, it's time to rewrite the update. It rewrites as:

$= (⊤_{Π} ⋉ Θ) (λ π, h . 1_{π = π^{'}} p r_{(A \times O)^{ω} *} (\to_{F : \infty}^{π^{'}} (π, h)) (U) + 1_{π \neq π^{'}})$

Now, since $π = π^{'}$ inside the scope of the indicator function, we can rewrite as

$= (⊤_{Π} ⋉ Θ) (λ π, h . 1_{π = π^{'}} p r_{(A \times O)^{ω} *} (\to_{F : \infty}^{π^{'}} (π^{'}, h)) (U) + 1_{π \neq π^{'}})$

And use our usual argument from before that $p r_{(A \times O)^{ω} *} (\to_{F : \infty}^{π^{'}} (π^{'}, h))$ is just the dirac-delta distribution on h, to get

$= (⊤_{Π} ⋉ Θ) (λ π, h . 1_{π = π^{'}} U (h) + 1_{π \neq π^{'}})$

Now, we can unpack the semidirect product as well as what $⊤_{Π}$ means, to get:

$= {inf}_{π} Θ (π) (λ h . 1_{π = π^{'}} U (h) + 1_{π \neq π^{'}})$

Now, if $π \neq π^{'}$ , then that inner function turns into 1 (or infinity) which is assigned maximum value by all $Θ (π)$ , so it's minimized when $π = π^{'}$ , so we get:

$= Θ (π^{'}) (λ h . U (h)) = Θ (π^{'}) (U)$

And we're done with the last "doing this path is identity" result. All that remains in our proof is just showing that taking both paths from one corner to another corner makes the same result, to show that going around in a loop is identity, ruling out nontrivial automorphisms.

T2.3 The easiest pair of corners for this is going from first-person static to third-person dynamic in both ways. Obviously, the transition kernel would be the same no matter which path you took, which just leaves verifying that the starting infradistribution is the same. Down one path, we have

$D := ⊤_{Π} ⋉ Θ, ψ_{T} := D$

Down the other path, we have

$ψ_{F} := ⊤_{Π} ⋉ Θ, ψ_{T} := ψ_{F}$

Obviously, both these paths produce the same result when you try to define $ψ_{T}$ in both ways from $Θ$ . And we're done!

Theorem 3: Pseudocausal Commutative Square: The following diagram commutes for any choice of pseudocausal belief function $Θ$ . Any choice of infradistribution $D$ where $D = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (D)))$ also makes this diagram commute.

Again, the work we need to put in is getting conditions in the four corners that are "came from a pseudocausal belief function", then, for phase 1, verifying that all 8 morphisms preserve the relevant property in the target if the source had it, then for phase 2, verifying that all 8 ways of going from a corner to 1 away and back result in identity to get 4 isomorphisms, then finally showing that starting in one corner and going to the other corner by two different paths make the same result, to rule out nontrivial automorphisms.

The property for third-person static is $D = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (D)))$

The property for third-person dynamic is $ψ_{T} = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (ψ_{T})))$ and $\to_{T} (a o h) = δ_{a, o, h}$

The property for first-person static is pseudocausality, $\forall π^{'}, π, U : u_{\sim π^{'}}^{1} (Θ (π)) (U) \geq Θ (π^{'})$

The property for first-person dynamic is $ψ_{F} = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (ψ_{F})))$ and $\to_{F} (a o h, a^{'}) = δ_{o, h}$ when $a^{'} = a$ , and $⊥$ when $a^{'} \neq a$ .

Time to show preservation of these properties by all the morphisms, as well as that the translations make a belief function/infradistribution.

Our first step is showing that all 8 morphisms induce the relevant property in the target if the source has the property.

T3.1.1 3-static to 1-static. Our definition is

$Θ (π) := u_{\sim π}^{1} (D)$

and we must check the five conditions of a belief function, as well as pseudocausality.

T3.1.1.1 Checking the five conditions of a belief function proceeds in almost exactly the same way as checking the five conditions of a belief function in the "Acausal Commutative Square" theorem. We leave it as an exercise to the reader, and will just elaborate on the only nontrivial new argument needed.

The only nontrivial modification is in our proof of lower-semicontinuity. In order for it to work, we need that for any m, the subset of $(A \times O)^{ω}$ where $h \sim π_{m}$ or $h \sim π_{m + 1}$ or $π_{m + 2}$ ... or $π_{\infty}$ is closed.

We can rephrase the set ${h | \exists n \geq m : h \sim π_{n}}$ as the projection down to the $(A \times O)^{ω}$ coordinate of the set

$({π_{n}}_{n \geq m} \times (A \times O)^{ω}) \cap {π, h | h \sim π}$

$(A \times O)^{ω}$ is compact, and ${π_{n}}_{n \geq m}$ is compact as well, since it limits to a point and the limit point is included. So that product is a compact set. The set ${π, h | h \sim π}$ is closed. So $({π_{n}}_{n \geq m} \times (A \times O)^{ω}) \cap {π, h | h \sim π}$ is the intersection of a compact and a closed set, and so is compact. And projections of compact sets are compact, and compactness implies closure. So, the set of histories ${h | \exists n \geq m : h \sim π_{n}}$ is closed regardless of m, even if $m = \infty$ .

The rest of the proof works out with no issue, so translating over an infradistribution makes a belief function.

T3.1.1.2 We still have to check pseudocausality however. Our translation is

$Θ (π) := u_{\sim π}^{1} (D)$

and we want to show

$\forall π^{'}, π, U : u_{\sim π^{'}}^{1} (Θ (π)) (U) \geq Θ (π^{'}) (U)$

Reexpressing this desired statement in terms of $D$ , we have

$\forall π^{'}, π, U : u_{\sim π^{'}}^{1} (u_{\sim π}^{1} (D)) (U) \geq u_{\sim π^{'}}^{1} (D) (U)$

Let $π^{'}$ and $π$ be arbitrary. Then the left side is

$u_{\sim π^{'}}^{1} (u_{\sim π}^{1} (D)) (U)$

We unpack the update

$= u_{\sim π}^{1} (D) (λ h . 1_{h \sim π^{'}} U (h) + 1_{h ≁ π^{'}})$

And unpack the update again, to get

$= D (λ h . 1_{h \sim π} \cdot (1_{h \sim π^{'}} f (h) + 1_{h ≁ π^{'}}) + 1_{h ≁ π})$

Looking at this, the function is $U$ when h is compatible with both $π^{'}$ and $π$ , and 1 otherwise. This is a greater function than $U$ when h is compatible with just $π^{'}$ , and 1 otherwise, so by monotonicity for infradistributions, we can get:

$\geq D (λ h . 1_{h \sim π^{'}} U (h) + 1_{h ≁ π^{'}})$

and pack up the update to get

$= u_{\sim π^{'}}^{1} (D) (U)$

And we're done, we get pseudocausality.

T3.1.2 1-static to 3-static. Our translation is

$D := p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ)$

We'll show the infradistribution conditions on $D$ . First, to show it's even well-defined, we have

$D (U) = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ) (U) = ⊤_{Π} (λ π . Θ (π) (λ h . U (h)))$

That inner function is lower-semicontinuous in $π$ , because $Θ$ was assumed to have that property in its first argument. Since the inner function is lower-semicontinuous, it can be evaluated.

Now for the condition that

$D = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (D)))$

We start with $D (U)$ and unpack the definition of $D$ , to get

$= p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ) (U)$

And then undo the projection and semidirect product and what $⊤_{Π}$ means, to get

$= {inf}_{π} Θ (π) (λ h . U (h))$

And then, by pseudocausality for $Θ$ (for all $π^{'}$ , $u_{\sim π}^{1} (Θ (π^{'})) (U) \geq Θ (π) (U)$ and also $u_{\sim π}^{1} (Θ (π)) (U) = Θ (π) (U)$ because $Θ (π)$ is supported entirely on histories compatible with $π$ ), we can swap $Θ (π) (λ h . U (h))$ out for

$= {inf}_{π} {inf}_{π^{'}} u_{\sim π}^{1} (Θ (π^{'})) (λ h . U (h))$

And then unpack the update, to get

$= {inf}_{π} {inf}_{π^{'}} Θ (π^{'}) (λ h . 1_{h \sim π} U (h) + 1_{h ≁ π})$

Now we pack up what $⊤_{Π}$ means, and the semidirect product, to get

$= {inf}_{π} (⊤_{Π} ⋉ Θ) (λ π^{'}, h . 1_{h \sim π} U (h) + 1_{h ≁ π})$

Write this as a projection

$= {inf}_{π} p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ) (λ h . 1_{h \sim π} U (h) + 1_{h ≁ π})$

Pack up the definition of $D$ to get

$= {inf}_{π} D (λ h . 1_{h \sim π} U (h) + 1_{h ≁ π})$

Pack up the definition of "1-update on $π$ " to get

$= {inf}_{π} u_{\sim π}^{1} (D) (λ h . U (h))$

Pack up what $⊤_{Π}$ means and the semidirect product and the projection to get

$= p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (D))) (U)$

So we have

$D = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (D)))$

as desired, since $U$ was arbitrary.

Now to verify the infradistribution conditions on $D$ . This proof is pretty much identical to the proof in the "Acausal Commutative Square" theorem, interested readers can fill it in.

T3.1.3 For 3-static to 3-dynamic, we have $\to_{T} (a o h) := δ_{a, o, h}$ (which fulfills one of the 3-dynamic conditions), and $ψ_{T} := D$

Since $D$ is an infradistribution, $ψ_{T}$ is too, and for the condition on $ψ_{T}$ , we have:

$ψ_{T} = D = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (D))) = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (ψ_{T})))$

and we're done, since $D$ had the relevant condition.

T3.1.4 For 3-dynamic to 3-static, we have

$D := p r_{(A \times O)^{ω} *} (ψ_{T} ⋉ \to_{T : \infty})$

First, we must show that the niceness conditions are fulfilled for the infinite semidirect product to be defined. $\to_{T}$ maps $a o h$ to $a, o, h$ . This is clearly a continuous mapping, so in particular, it's lower-semicontinuous. Dirac-delta distributions are 1-Lipschitz when interpreted as inframeasures (all probability distributions have that property, actually). The compact-shared-CAS condition is redundant because $A \times O \times (A \times O)^{ω}$ is already a compact space. And all probability distributions (dirac-delta distributions are probability distributions) map constants to the same constant, so we get the increase-in-constants property and the 1 maps to 1 property. So we can indeed take the infinite semidirect product of the $\to_{T}$ .

Now, we'll show that unrolling like this just produces $ψ_{T}$ exactly. We'll use $h_{0}$ for the initial destiny state, and $a o h_{1 : \infty}$ for the successive unrolled history of states, actions, and observations. First, by unpacking $D$ 's definition,

$D (U) = p r_{(A \times O)^{ω} *} (ψ_{T} ⋉ \to_{T : \infty}) (U)$

Then we unpack the projection and semidirect product

$= ψ_{T} (λ h_{0} . \to_{T : \infty} (h_{0}) (λ a o h_{1 : \infty} . U (a o_{1 : \infty})))$

And pack things up into a projection

$= ψ_{T} (λ h_{0} . p r_{(A \times O)^{ω} *} (\to_{T : \infty} (h_{0})) (λ a o_{1 : \infty} . U (a o_{1 : \infty})))$

And then we can observe that unrolling the initial destiny forever via "advance the destiny 1 step, popping actions and observations off", when you project down to just the actions and observations, yields just the point distribution on that destiny, so we get:

$= ψ_{T} (λ h . δ_{h} (λ a o_{1 : \infty} . U (a o_{1 : \infty})))$

And then substitute the value of that dirac-delta in to get

$= ψ_{T} (λ h . U (h)) = ψ_{T} (U)$

So, our $D = ψ_{T}$ . Now we can go

$D = ψ_{T} = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (ψ_{T}))) = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (D)))$

and we're done, showing $D$ had the relevant condition from $ψ_{T}$ having it. Since $ψ_{T}$ is an infradistribution, $D$ is too.

T3.1.5 For 3-dynamic to 1-dynamic, we have

$\to_{F} (h, a^{'}) := p r_{O \times (A \times O)^{ω} *} (u_{{a^{'}}}^{1} (\to_{T} (h)))$

Let's write $h$ as $a o h$ (unpacking the destiny a bit). Now, for the action $a$ (which is compatible with the start of the history), we have

$\to_{F} (a o h, a) (f)$

Applying our definition, we have

$= p r_{O \times (A \times O)^{ω} *} (u_{{a}}^{1} (\to_{T} (a o h))) (f)$

Unpacking the projection, we have

$= u_{{a}}^{1} (\to_{T} (a o h)) (λ a^{'}, o^{'}, h^{'} . f (o^{'}, h^{'}))$

Unpacking the update, we have

$= \to_{T} (a o h) (λ a^{'}, o^{'}, h^{'} . 1_{a^{'} = a} f (o^{'}, h^{'}) + 1_{a^{'} \neq a})$

And then we consider that $\to_{T} (a o h)$ is just the dirac-delta distribution on $(a, o, h)$ , so we have

$= δ_{a, o, h} (λ a^{'}, o^{'}, h^{'} . 1_{a^{'} = a} f (o^{'}, h^{'}) + 1_{a^{'} \neq a})$

Substitute the values in, and we have

$= f (o, h) = δ_{o, h} (f)$

So, $\to_{F} (a, a o h)$ is just the dirac-delta distribution on $o$ and $h$ , as it should be.

For $a^{'}$ that aren't $a$ as it should be, we have

$\to_{F} (a o h, a^{'}) (f)$

Applying our definition, we have

$= p r_{O \times (A \times O)^{ω} *} (u_{{a^{'}}}^{1} (\to_{T} (a o h))) (f)$

Unpacking the projection, we have

$= u_{{a^{'}}}^{1} (\to_{T} (a o h)) (λ a^{''}, o^{'}, h^{'} . f (o^{'}, h^{'}))$

Unpacking the update, we have

$= \to_{T} (a o h) (λ a^{''}, o^{'}, h^{'} . 1_{a^{''} = a^{'}} f (o^{'}, h^{'}) + 1_{a^{''} \neq a^{'}})$

And then we consider that $\to_{T} (a o h)$ is just the dirac-delta distribution on $(a, o, h)$ , so we have

$= δ_{a, o, h} (λ a^{''}, o^{'}, h^{'} . 1_{a^{''} = a^{'}} f (o^{'}, h^{'}) + 1_{a^{''} \neq a^{'}})$

and because $a^{'} \neq a$ , substituting the dirac-delta in produces 1 (or infinity), ie, $⊥ (f)$ . Therefore,

$\to_{F} (a o h, a^{'}) = ⊥$

So our transition kernel works out. For the other conditions, just observe that $ψ_{F} := ψ_{T}$ , and use the extreme similarity of their defining conditions.

T3.1.6 For 1-dynamic to 3-dynamic, we have $ψ_{T} := ψ_{F}$ so we can use our defining property to again, clearly show that the resulting 3-dynamic starting infradistribution has the relevant property, so that just leaves cleaning up the defining property for the $\to_{T}$ infrakernel. We remember that

$\to_{T} (h) := ⊤_{A} ⋉ (λ a . \to_{F} (h, a))$

Therefore, we have:

$\to_{T} (a o h) (f) = (⊤_{A} ⋉ (λ a^{'} . \to_{F} (a o h, a^{'}))) (f)$

Then, we can unpack the semidirect product as:

$= ⊤_{A} (λ a^{'} . \to_{F} (a o h, a^{'}) (λ o^{'}, h^{'} . f (a^{'}, o^{'}, h^{'})))$

We unpack our $⊤_{A}$ , getting

$= {inf}_{a^{'}} (\to_{F} (a o h, a^{'}) (λ o^{'}, h^{'} . f (a^{'}, o, s)))$

Then, we observe that for any $a^{'} \neq a$ , $\to_{F} (a o h, a^{'}) = ⊥$ . So, $a^{'}$ must be $a$ , and we have

$= \to_{F} (a o h, a) (λ o^{'}, h^{'} . f (a, o^{'}, h^{'}))$

Now, $\to_{F} (a o h, a)$ is the dirac-delta distribution on $(o, h)$ , so making that substitution in, we have

$= δ_{o, h} (λ o^{'}, h^{'} . f (a, o^{'}, h^{'})) = f (a, o, h) = δ_{a, o, h} (f)$

And this holds for all $f$ , so we get our desired result that

$\to_{T} (a o h) = δ_{a, o, h}$

T3.1.7: For 1-static to 1-dynamic, we just have

$ψ_{F} := p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ)$

$\to_{F} (a o h, a) := δ_{o, h}$

$\to_{F} (a o h, a^{'}) := ⊥$

So this automatically makes the infrakernel have the desired properties. For showing the relevant property of $ψ_{F}$ , we just copy the proof at the start of getting the properties for $D$ from $Θ$ being a belief function, since $D$ and $ψ_{F}$ are both defined in the same way.

T3.1.8 For 1-dynamic to 1-static, we have

$Θ (π^{'}) := p r_{(A \times O)^{ω} *} (ψ_{F} ⋉ \to_{F : \infty}^{π^{'}})$

We'll work on getting that latter quantity into a better form, but first we have to verify that
$\to_{F : \infty}^{π}$ has the $\to_{F : n}^{π}$ fulfilling the niceness conditions. It's defined as

$\to_{F : n}^{π} (h_{0}, a o h_{1 : n}) := δ_{π (a o_{1 : n})} ⋉ (λ a . \to_{F} (h_{n}, a))$

For lower-semicontinuity, $\to_{F}$ is lower-semicontinuous, because it returns $⊥$ on every action but one (this is a clopen set), and for the action that pairs up with the initial destiny, it just advances the destiny, which is continuous. $\to_{F : n}^{π}$ behaves similarly, continuous variation in input leads to continuous variation in output, because eventually the behavior of the policy settles down to a fixed action as the history of actions and observations stabilizes amongst one of the finitely many options.

For making inframeasures, $\to_{F : n}^{π}$ always returns a dirac-delta distribution or $⊥$ , so we're good there. Similarly, for 1-Lipschitzness, both $⊥$ and dirac-delta distributions are 1-Lipschitz. For compact-shared CAS, as the target space is $A \times O \times (A \times O)^{ω}$ , it's compact and you don't need to worry about that. Finally, both dirac-delta distributions and $⊥$ map constants to either the same constant or higher, and in the $[0, 1]$ type sinature, both $⊥$ and dirac-delta distributions map 1 to 1. So all niceness conditions are fulfilled.

Let's work on unpacking the value

$p r_{(A \times O)^{ω} *} (ψ_{F} ⋉ \to_{F : \infty}^{π}) (U)$

unpacking the projection and semidirect product, we get

$= ψ_{F} (λ h_{0} . \to_{F : \infty}^{π} (h) (λ a o h_{1 : \infty} . U (a o_{1 : \infty})))$

And then we can write this as a projection in the inside

$= ψ_{F} (λ h_{0} . p r_{(A \times O)^{ω} *} (\to_{F : \infty}^{π} (h)) (λ a o_{1 : \infty} . U (a o_{1 : \infty})))$

One of two things can happen. In the first case, h is compatible with $π$ , so playing $π$ against it never hits $⊥$ , and it unrolls to completion, and projecting down just yields the dirac-delta distribution on h itself. In the second case, h is incompatible with $π$ , so eventually we hit $⊥$ , which maps everything to maximal value (either 1 or infinity). Thus, we can write this as an indicator function

$= ψ_{F} (λ h . 1_{h \sim π} δ_{h} (λ a o_{1 : \infty} . U (a o_{1 : \infty})) + 1_{h ≁ π^{'}})$

Substituting the dirac-delta value in, we have

$= ψ_{F} (λ h . 1_{h \sim π} U (h) + 1_{h ≁ π})$

And we pack the update back up to get

$= u_{\sim π}^{1} (ψ_{F}) (U)$

Since $U$ was arbitrary, we have

$p r_{(A \times O)^{ω} *} (ψ_{F} ⋉ \to_{F : \infty}^{π}) = u_{\sim π^{'}}^{1} (ψ_{F})$

And so, an alternate way to define $Θ (π)$ is as

$= u_{\sim π}^{1} (ψ_{F})$

We can then run through the same proof that $Θ$ is indeed a belief function, back from the 3-static to 1-static case, because $ψ_{F}$ fulfills all the same properties that $D$ did.

Alright, now we have, for all four corners, a condition that's basically "came from a pseudocausal belief function" that is preserved under morphisms. Now we need to show that all 8 back-and-forth directions are identity.

T3.2.1 For 1-static to 3-static back to 1-static, we want to show

$Θ (π^{'}) = u_{\sim π^{'}}^{1} (p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ))$

This is (we assume the hard version first)

$u_{\sim π^{'}}^{1} (p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ)) (U)$

Then unpack the update

$= p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ) (λ h . 1_{h \sim π^{'}} U (h) + 1_{h ≁ π^{'}})$

And the projection

$= (⊤_{Π} ⋉ Θ) (λ π, h . 1_{h \sim π^{'}} U (h) + 1_{h ≁ π^{'}})$

Then unpack the semidirect product and $⊤_{Π}$ to get

$= {inf}_{π} Θ (π) (λ h . 1_{h \sim π^{'}} U (h) + 1_{h ≁ π^{'}})$

then rewrite this as an update

$= {inf}_{π} u_{\sim π^{'}}^{1} (Θ (π)) (λ h . U (h))$

And then we can apply pseudocausality of \BF to get that the minimizer must pick $π^{'}$ exactly because $u_{\sim π^{'}}^{1} (Θ (π)) (U) \geq Θ (π^{'}) (U) = u_{\sim π^{'}}^{1} (Θ (π^{'})) (U)$ and so we get

$= Θ (π^{'}) (U)$

and we're done.

T3.2.2 For 3-static to 1-static to 3-static, we must show

$D = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (D)))$

Well, the property for a third-person static $D$ is exactly that.

T3.2.3 For 3-static to 3-dynamic to 3-static, we want that

$D = p r_{(A \times O)^{ω} *} (D ⋉ \to_{T : \infty})$

Taking the complicated part, it's

$p r_{(A \times O)^{ω} *} (D ⋉ \to_{T : \infty}) (U)$

We unpack the projection

$= (D ⋉ \to_{T : \infty}) (λ h_{0}, a o h_{1 : \infty} . U (a o_{: \infty}))$

And then we unpack the semidirect product a bit, to get

$= D (λ h_{0} . \to_{T : \infty} (h_{0}) (λ a o h_{1 : \infty} . U (a o_{1 : \infty})))$

And then we can write this as a projection, to get

$= D (λ h_{0} . p r_{(A \times O)^{ω} *} (\to_{T : \infty} (h_{0})) (λ a o_{1 : \infty} . U (a o_{1 : \infty})))$

Now, we observe that because $\to_{T}$ , when repeatedly unrolled, is just emitting the actions and observations from the starting destiny, this projection is just the point distribution on the action-observation sequence that is $h_{0}$ .

$= D (λ h_{0} . δ_{h_{0}} (λ a o_{1 : \infty} . U (a o_{1 : \infty})))$

Then we evaluate the expectation, yielding

$= D (λ h . U (h)) = D (U)$

And we're done.

T3.2.4 For going 3-dynamic to 3-static to 3-dynamic, we need that

$ψ_{T} = p r_{(A \times O)^{ω} *} (ψ_{T} ⋉ \to_{T : \infty})$

To show this, just reuse the exact same proof from above, just with $ψ_{T}$ instead of $D$ . Also, $\to_{F} (h)$ works out as it should.

T3.2.5,6 For translating back and forth between 3-dynamic and 1-dynamic, we observe that both translations keep the initial infradistribution over destinies the same, and our 3-dynamic to 1-dynamic, and 1-dynamic to 3-dynamic proofs verified that the $\to_{F}$ and $\to_{T}$ behave as they should when they go back and forth, so we don't need to worry about this.

T3.2.7 Next is 1-dynamic to 1-static to 1-dynamic. The infrakernel is guaranteed to have the right form, we just need to show that $ψ_{F}$ is unchanged. So, we must show

$ψ_{F} = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (ψ_{F} ⋉ \to_{F : \infty}^{π})))$

But, since our condition on 1-dynamic (that we showed is a property of applying the morphism to go from any belief function to first-person dynamic) was

$ψ_{F} = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (ψ_{F})))$

The only thing we need to show is that, regardless of $π$ ,

$u_{\sim π}^{1} (ψ_{F}) = p r_{(A \times O)^{ω} *} (ψ_{F} ⋉ \to_{F : \infty}^{π})$

For if we could show that, then we could go:

$p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . p r_{(A \times O)^{ω} *} (ψ_{F} ⋉ \to_{F : \infty}^{π}))) = p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ (λ π . u_{\sim π}^{1} (ψ_{F}))) = ψ_{F}$

and we'd be done. However, from the 1-dynamic to 1-static proof of property preservation, we already showed that

$p r_{(A \times O)^{ω} *} (ψ_{F} ⋉ \to_{F : \infty}^{π}) (U) = u_{\sim π}^{1} (ψ_{F}) (U)$

back then, so we're just done.

T3.2.8 Time for the last leg of the square, that going first-person static to dynamic and back to static is identity. We want to show that, regardless of $π^{'}$ ,

$Θ (π^{'}) = p r_{(A \times O)^{ω} *} ((p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ)) ⋉ \to_{F : \infty}^{π^{'}})$

To do this, we use the result from the 1-dynamic to 1-static proof of property preservation, that

$p r_{(A \times O)^{ω} *} (ψ_{F} ⋉ \to_{F : \infty}^{π}) = u_{\sim π}^{1} (ψ_{F})$

Applying this fact with $ψ_{F}$ as an abbreviation for $p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ)$ , we can rewrite our proof goal equivalently with this fact as

$Θ (π^{'}) = p r_{(A \times O)^{ω} *} (u_{\sim π^{'}}^{1} (p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ)))$

But we showed this exact result when we showed that 1-static to 3-static to 1-static was identity, so we're done.

T3.3 The easiest pair of corners for this is going from first-person static to third-person dynamic in both ways. Obviously, the transition kernel would be the same no matter which path you took, which just leaves verifying that the starting infradistribution is the same. Down one path, we have

$D := p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ), ψ_{T} := D$

Down the other path, we have

$ψ_{F} := p r_{(A \times O)^{ω} *} (⊤_{Π} ⋉ Θ), ψ_{T} := ψ_{F}$

Obviously, both these paths produce the same result when you try to define $ψ_{T}$ in both ways from $Θ$ . And we're done!

LESSWRONG
LW

LESSWRONG
LW

5

Proofs Theorems 2,3

5

Ω 3

5

Ω 3