Manuscript I@2 · I.tex · section · 85631fa7

Sharp contexts and transport

Context refinement and the Frauchiger–Renner example › Sharp contexts and transport · lines 2561–2577

For events $E, F$ in one context, write

Ψ ⊢_{C} E \Rightarrow F if C Pr (E ∖ F) = 0.

Chaining is sound within one context, because

E ∖ G \subseteq (E ∖ F) \cup (F ∖ G) .

Transport to a refining context uses the specified inverse-image map on labels, with the same event projectors. Shared verbal labels alone do not provide such a refinement.

Displayed formulas in this passage

unlabeled · line 2564
$Ψ ⊢_{C} E \Rightarrow F if C Pr (E ∖ F) = 0.$
unlabeled · line 2570
$E ∖ G \subseteq (E ∖ F) \cup (F ∖ G) .$

Nearby in this section

section: Sharp contexts and transport
lemma: Lemma: Common sharp refinement