Given $B_{sl_{i}}$ at slot $sl_i$, there $\exists! B_{sl_f}$ s.t.
$$ sl_f =\argmin_{sl \in \mathbb{Z} ,\space sl>sl_i}{\forall B_{sl_j},sl_j \le sl},\space \textbf{forkchoice}(B_{sl_j}, B_{sl})=B_{sl}
$$
That is, what is the earliest block after $sl_i$ in which selecting any other block before that block and applying the fork choice rule, will result in the selection of that block.
$s=3k/f$ such that
$$ s >> Empirical\space Finality $$
Given zone update $Z$ and block tree $T$. Zone finality is only defined IFF $Z$ is eventually finalized by cryptarchia.
let $\mathbb{B}_Z=\{B\in T | Z\in B\}$
let $sl_i = \argmin_i B_{sl_i} \in \mathbb{B}_Z$
let $sl_f = \argmax_f B_{sl_f} \in \mathbb{B}_Z$