Modal-effect and encoding notation

notation	scope and role	forbidden transfer
notation	scope and role	forbidden transfer
$\mathcal{T},{\mathcal{R}}_{\mathrm{sc}},\mathcal{S}$	effect structure, scoped-row instance, set instance	not type universes or operational stores
$E,F,D$	effect contexts and finite extensions in Met	source rows and capability sets remain separately tagged
$D{\equiv }_{\mathcal{T}}{D}^{\prime }$, $E{⪯}_{\mathsf{e}}F$	effect-structure equivalence and its derived inclusion	neither relation is a source-row unifier or capability-set judgment
$A{\equiv }_{\mathsf{Met}}B$, $\mu {\equiv }_{\mathsf{Met}}\nu$	structural Met type and modality equivalence	distinct from the selected effect structure’s extension equivalence
$[E]$, $⟨D⟩$	absolute replacement and relative extension modalities	brackets do not denote evaluation contexts here
$\mu \circ \nu$	left-to-right modality composition: first $\mu$, then $\nu$	not ordinary right-to-left function composition
${◻}_{\mu }A$, ${\mathsf{mod}}_{\mu }V$	modal type and value introduction	$\mathsf{mod}$ does not suspend a computation
$x{:}_{{\mu }_F}A$, $\mathsf{lock}({\mu }_F)$	tagged variable and ordered context lock	the subscript is an ambient effect context, not a grade
$\mathrm{\Gamma }⊢M:A@E$	Met typing at effect context $E$	distinct from System $C$’s boxed type $T@C$
$\mathrm{\Gamma }{⊢}_{c}M:A!E$	System $F_{\epsilon }$ computation typing	not chapter 25’s inferred computation judgment
$\mathrm{\Gamma }{⊢}_{b}P:T\mid C$	System $C$ block typing with capability set	vertical bar is not semantic conditioning
$⟨⟨-⟩{⟩}_{\mathsf{r}}$, $⟨⟨-⟩{⟩}_{\mathsf{c}}$	row-source and capability-source translations to Met	neither glyph denotes an inverse or a source-to-source map
$\hat{f}$, $\tilde{f}$, ${\ell }_f$	effect variable, unlocked block term, and fresh local operation	the two target binders and the runtime label are not identified

Source subscripts are mandatory whenever one translation could be confused with the other. Within the Met card, $E{⪯}_{\mathsf{e}}F$ is derived subeffecting. Within System $C$, $C\subseteq C^{\prime }$ is set inclusion. Within System $F_{\epsilon }$, row equivalence preserves duplicates. These three relations are never silently interchanged.