3.3 Typed near-litters, singletons, and positions

Definition 3.13 typed near-litters

We define a function \( \operatorname {\mathsf{typed}}_\alpha \) from the type of near-litters to the type of new t-sets by mapping a near-litter \( N \) to the code \( (\bot , N) \). This code is even as all codes of the form \( (\bot , s) \) are even. This function is clearly injective, and satisfies

\[ \rho (\operatorname {\mathsf{typed}}_\alpha (N)) = \operatorname {\mathsf{typed}}_\alpha (\rho (\bot )(N)) \]

by definition.

Definition 3.14 singletons

We define a function \( \operatorname {\mathsf{singleton}}_\alpha \) for each lower type index \( \beta \) from \( \mathsf{TSet}_\beta \) to the type of new t-sets by \( x \mapsto (\beta , \{ x\} ) \). The given code is even as all singleton codes are even. This satisfies \( U_\alpha (\operatorname {\mathsf{singleton}}_\alpha (x))(\beta ) = \{ x \} \).

Proposition 3.15 position function

Using the model data from definition 3.12, if \( \# \mathsf{Tang}_\alpha \leq \# \mu \), then there is a position function on the type of \( \alpha \)-tangles, ¹ such that

if \( N \) is a near-litter and \( t \) is an \( \alpha \)-tangle such that \( \operatorname {\mathsf{set}}(t) = \operatorname {\mathsf{typed}}_\alpha (N) \), we have \( \iota (N) \leq \iota (t) \); and
if \( t \) is an \( \alpha \)-tangle and \( x \) is an atom or near-litter that occurs in the range of \( \operatorname {\mathsf{supp}}(t)_A \), then \( \iota (x) {\lt} \iota (t) \).

Proof ▶

We use proposition 2.18 to construct the position function, using denied set

\[ D(t) = \{ \iota (N) \mid \operatorname {\mathsf{set}}(t) = \operatorname {\mathsf{typed}}_\alpha (N) \} \cup \{ \iota (a) \mid a \in \operatorname {\mathsf{im}}\operatorname {\mathsf{supp}}(t)_A^{\mathcal A}\} \cup \{ \iota (N) \mid N \in \operatorname {\mathsf{im}}\operatorname {\mathsf{supp}}(t)_A^{\mathcal N}\} \]

The first set is a subsingleton and the second two sets are small, so the denied set has size less than \( \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu )) \) as required.