Effect-capability and tunnelling notation

Chapter 32 owns the following notation within its three separate cards.

notation	scope and role	non-transfer condition
notation	scope and role	non-transfer condition
$\mathrm{\Gamma }$	value variables in System $\mathsf{Xi}$ and Effekt; term variables in tunnelling	the surrounding judgment fixes the context grammar
$\mathrm{\Delta }$	block variables in System $\mathsf{Xi}$ and Effekt; effect variables in tunnelling and Olaf	no equality between these contexts is implied
$\mathrm{\Xi }$	ordered allocation stack in System $\mathsf{Xi}$; label context in tunnelling; lifetime constants in Olaf	in ${\mathrm{\Xi }}_0,\ell :\tau ,{\mathrm{\Xi }}_{+}$, ${\mathrm{\Xi }}_0$ is the capability’s birth prefix and ${\mathrm{\Xi }}_{+}$ contains later delimiters
$P$	tunnelling handler-variable context	does not occur in System $\mathsf{Xi}$ or Effekt
$\mathrm{\Theta }$	abbreviation for a translated System-$\mathsf{Xi}$ block context; lifetime-variable context in the separate Olaf boundary	the surrounding card fixes which role is active
${\mathrm{\#}}_{\ell }\{s\}$	System-$\mathsf{Xi}$ runtime delimiter	introduced only by handler reduction
${\mathsf{cap}}_{\ell }\{(x,k)\Rightarrow s\}$	System-$\mathsf{Xi}$ runtime capability	second class and usable only under matching ${\mathrm{\#}}_{\ell }$
$\Uparrow h$	tunnelling request constructor	names a handler value, not merely an operation
${\Downarrow }_{[T{]}_{\overline{e}}}^{\ell }t$	tunnelling delimiter	distinct from System-$\mathsf{Xi}$’s ${\mathrm{\#}}_{\ell }$
$\ell ⇝̸K$	context $K$ does not bind label $\ell$	a syntactic side condition, not set nonmembership
$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }\vDash$ $t_1{⪯}_{\mathsf{log}}{t}_2:[T{]}_{\overline{e}}$	open logical-refinement judgment	$\vDash$ marks the judgment; ${⪯}_{\mathsf{log}}$ relates terms
$\mathsf{CapTy},\mathsf{CapEff}$ ${\mathsf{CapStmt}}_{\mathrm{\Sigma },\mathrm{\Delta }}$	named Effekt-to-System-$\mathsf{Xi}$ syntax translation	not semantic double brackets
$\mathcal{O},\mathcal{T},\mathcal{K},\mathcal{S}$ $\mathcal{V},\mathcal{H},\mathcal{U},\mathcal{W}$	tunnelling logical-relation components	indexed only by the displayed worlds and environments
$▹P$	step-indexed later modality in the tunnelling logical relation	lowers the numerical index; it does not extend the label context $\mathrm{\Xi }$

All context extensions in the tunnelling card bind fresh names. In particular, $\mathrm{\Xi },\ell :[T{]}_{\overline{e}}$ carries the side condition $\ell \notin \mathrm{dom}(\mathrm{\Xi })$; the separate condition $\ell \notin \mathrm{fl}(T,\overline{e})$ prevents that fresh label from escaping the delimiter’s result interface.

The glyphs $\Uparrow$ and $\Downarrow$ are owned by Chapter 32’s tunnelling syntax. Elsewhere in the book, raw arrows retain their usual order, reduction, or implication roles. The symbol ${⪯}_{\mathsf{log}}$ denotes logical refinement only when accompanied by the tunnelling or Olaf typing contexts. The symbol $⇝̸$ is a syntactic no-binding judgment.

The three effect carriers are deliberately distinct: Their union, substitution, and scope laws belong to their own cards. An Effekt set is not silently interpreted as a tunnelling effect sequence, and an Olaf lifetime effect is not a System-$\mathsf{Xi}$ runtime label.