- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
The typical atom graph of \( \psi \) is the relation \( \psi ^{T{\mathcal A}} \) given by the following constructor. If \( (L_1, L_2) \in \psi ^{\mathcal L}\), then
for some \( i : \kappa \), where for any near-litter \( N \), \( h_N \) is an equivalence \( \kappa \simeq N \) chosen in advance.
The atom graph of \( \psi \) is the relation \( \psi ^{\mathcal A}= \psi ^{E{\mathcal A}} \sqcup \psi ^{T{\mathcal A}} \): the join of the exceptional and typical atom graphs.
A base action is a pair \( \xi = (\xi ^{\mathcal A}, \xi ^{\mathcal N}) \) such that \( \xi ^{\mathcal A}\) and \( \xi ^{\mathcal N}\) are relations of atoms and near-litters respectively (definition A.1), such that
\( \xi ^{\mathcal A}\) and \( \xi ^{\mathcal N}\) are defined on small sets;
\( \xi ^{\mathcal A}\) is one-to-one;
if \( (a_1, a_2) \in \xi ^{\mathcal A}\) and \( (N_1, N_2) \in \xi ^{\mathcal N}\), then \( a_1 \in N_1 \) if and only if \( a_2 \in N_2 \);
if \( (N_1, N_3), (N_2, N_4) \in \xi ^{\mathcal N}\), then \( N_1^\circ = N_2^\circ \) if and only if \( N_3^\circ = N_4^\circ \);
for each \( (N_1, N_3), (N_2, N_4) \in \xi ^{\mathcal N}\),
\[ \operatorname {\mathsf{interf}}(N_1, N_2) \subseteq \operatorname {\mathsf{coim}}\xi ^{\mathcal A};\quad \operatorname {\mathsf{interf}}(N_3, N_4) \subseteq \operatorname {\mathsf{im}}\xi ^{\mathcal A} \]
Note that these conditions imply that \( \xi ^{\mathcal N}\) is one-to-one. We define the one-to-one relation \( \xi ^{\mathcal L}\) by the constructor
The partial order on base actions is defined by \( \xi \leq \zeta \) if and only if \( \xi ^{\mathcal A}\leq \zeta ^{\mathcal A}\) and \( \xi ^{\mathcal N}= \zeta ^{\mathcal N}\). 1 The inverse of \( \xi \) is \( ((\xi ^{\mathcal A})^{-1}, (\xi ^{\mathcal N})^{-1}) \). They act on base supports in the natural way.
A base action \( \xi \) is nice if whenever \( (N_1, N_2) \in \xi ^{\mathcal N}\),
A base approximation is a pair \( \psi = (\psi ^{E{\mathcal A}}, \psi ^{\mathcal L}) \) such that \( \psi ^{E{\mathcal A}} \) and \( \psi ^{\mathcal L}\) are permutative relations of atoms and litters respectively (definition A.1), and for each litter \( L \), the set
is small. The relation \( \psi ^{E{\mathcal A}} \) is called the exceptional atom graph, and \( \psi ^{\mathcal L}\) is called the litter graph. We make the following definitions.
The inverse of a base approximation is \( \psi ^{-1} = ((\psi ^{E{\mathcal A}})^{-1}, (\psi ^{\mathcal L})^{-1}) \).
If \( \psi \) and \( \chi \) are base approximations where \( \operatorname {\mathsf{coim}}\psi ^{E{\mathcal A}} = \operatorname {\mathsf{coim}}\chi ^{E{\mathcal A}} \) and \( \operatorname {\mathsf{coim}}\psi ^{\mathcal L}= \operatorname {\mathsf{coim}}\chi ^{\mathcal L}\), then their composition \( \psi \circ \chi \) is the base approximation \( (\psi ^{E{\mathcal A}} \circ \chi ^{E{\mathcal A}}, \psi ^{\mathcal L}\circ \chi ^{\mathcal L}) \).
The \( \psi \)-sublitter of a litter \( L \), written \( L_\psi \), is the near-litter \( (L, \operatorname {\mathsf{LS}}(L) \setminus \operatorname {\mathsf{coim}}\psi ^{E{\mathcal A}}) \).
Let \( A : \beta \rightsquigarrow \bot \). An \( A \)-flexible approximation of a base action \( \xi \) is a base approximation \( \psi \) such that
\( \xi ^{\mathcal A}\leq \psi ^{E{\mathcal A}} \);
if \( L \in \operatorname {\mathsf{coim}}\psi ^{\mathcal L}\), then \( L \) is \( A \)-flexible;
if \( (N_1, N_2) \in \xi ^{\mathcal N}\) and \( N_1^\circ \) is \( A \)-flexible, then \( (N_1^\circ , N_2^\circ ) \in \psi ^{\mathcal L}\);
if \( (N_1, N_2) \in \xi ^{\mathcal N}\), then \( N_1 \mathrel {\triangle }\operatorname {\mathsf{LS}}(N_1^\circ ) \subseteq \operatorname {\mathsf{coim}}\psi ^{\mathcal A}\) and \( N_2 \mathrel {\triangle }\operatorname {\mathsf{LS}}(N_2^\circ ) \subseteq \operatorname {\mathsf{coim}}\psi ^{\mathcal A}\);
if \( (N_1, N_2) \in \xi ^{\mathcal N}\), then for each atom \( a_2 \),
\[ a_2 \in N_2 \leftrightarrow (\exists a_1 \in N_1,\, (a_1, a_2) \in \psi ^{E{\mathcal A}}) \vee (a_2 \notin \operatorname {\mathsf{coim}}\psi ^{E{\mathcal A}} \wedge a_2^\circ = N_2^\circ ) \]
A flexible approximation of a \( \beta \)-action \( \xi \) is a \( \beta \)-approximation \( \psi \) such that for each \( A : \beta \rightsquigarrow \bot \), the base approximation \( \psi _A \) is an \( A \)-flexible approximation of \( \xi _A \). Flexible approximations are coherent.
Let \( A \) be a \( \beta \)-extended type index. A litter \( L \) is \( A \)-inflexible if there is an inflexible \( \beta \)-path \( I \) such that \( A = ((A_I)_{\varepsilon _I})_\bot \) and \( L = f_{\delta _I, \varepsilon _I}(t) \) for some \( t : \mathsf{Tang}_{\delta _I} \). The coderivative operation works in the obvious way. A litter can be \( A \)-inflexible in at most one way. 1
We say that a \( L \) is \( A \)-flexible if it is not \( A \)-inflexible. 2 If \( L \) is \( B_A \)-flexible, then \( L \) is \( A \)-flexible.
The near-litter graph of \( \psi \) is the relation \( \psi ^{\mathcal N}\) given by setting \( (N_1, N_2) \in \psi ^{\mathcal N}\) if and only if \( (N_1^\circ , N_2^\circ ) \in \psi ^{\mathcal L}\), \( N_1 \) and \( N_2 \) are subsets of \( \operatorname {\mathsf{coim}}\psi ^{\mathcal A}\), and the image of \( \psi ^{\mathcal A}\) on \( N_1 \) is \( N_2 \) (or equivalently, by proposition A.2, the coimage of \( \psi ^{\mathcal A}\) on \( N_2 \) is \( N_1 \)).
Base approximations act on base supports in the following way. If \( S^{\mathcal A}= (i, f) \), then \( \psi (S)^{\mathcal A}= (i, f') \) where
The same definition is used for near-litters.
For a type index \( \beta \), a \( \beta \)-action is a \( \beta \)-tree of base actions. We define an action of \( \beta \)-actions \( \xi \) on \( \beta \)-supports \( S \) by \( (\xi (S))_A = \xi _A(S_A) \).
A \( \beta \)-action \( \xi \) is coherent at \( (A, L_1, L_2) \) if:
If \( L_1 \) is \( A \)-inflexible with inflexible \( \beta \)-path \( I = (\gamma , \delta , \varepsilon , B) \) and tangle \( t : \mathsf{Tang}_\delta \), then there is some \( \delta \)-allowable permutation \( \rho \) such that
\[ (\xi _B)_\delta (\operatorname {\mathsf{supp}}(t)) = \rho (\operatorname {\mathsf{supp}}(t)) \]and
\[ L_2 = f_{\delta ,\varepsilon }(\rho (t)) \](and hence again every \( \delta \)-allowable \( \rho \) satisfying the hypothesis also satisfies the conclusion).
If \( L_1 \) is \( A \)-flexible, then \( L_2 \) is \( A \)-flexible.
We say that \( \xi \) is coherent if whenever \( (L_1, L_2) \in \xi _A^{\mathcal L}\), \( \xi \) is coherent at \( (A, L_1, L_2) \).
For a type index \( \beta \), a \( \beta \)-approximation is a \( \beta \)-tree of base approximations. We define the partial order on \( \beta \)-approximations branchwise. We define an action of \( \beta \)-approximations \( \psi \) on \( \beta \)-supports \( S \) by \( (\psi (S))_A = \psi _A(S_A) \).
We say that a \( \beta \)-approximation \( \psi \) approximates a \( \beta \)-allowable permutation \( \rho \) if \( \psi _A^{\mathcal L}\leq \rho _A^{\mathcal L}\) and \( \psi _A^{\mathcal A}\leq \rho _A^{\mathcal A}\) for each path \( A : \beta \rightsquigarrow \bot \). If \( \psi \) approximates \( \rho \) then \( \psi ^n \) approximates \( \rho ^n \) for each \( n : \mathbb Z \). 1 A \( \beta \)-approximation \( \psi \) exactly approximates a \( \beta \)-allowable permutation \( \rho \) if \( \psi \) approximates \( \rho \), and in addition, if \( a \) is an atom and \( A : \beta \rightsquigarrow \bot \), then \( a \notin \operatorname {\mathsf{coim}}\psi _A^{\mathcal A}\) implies \( \rho (a)^\circ = \rho (a^\circ ) \) and \( \rho ^{-1}(a)^\circ = \rho ^{-1}(a^\circ ) \).
A \( \beta \)-approximation \( \psi \) is coherent at \( (A, L_1, L_2) \) if:
If \( L_1 \) is \( A \)-inflexible with inflexible \( \beta \)-path \( I = (\gamma , \delta , \varepsilon , B) \) and tangle \( t : \mathsf{Tang}_\delta \), then there is some \( \delta \)-allowable permutation \( \rho \) such that
\[ (\psi _B)_\delta (\operatorname {\mathsf{supp}}(t)) = \rho (\operatorname {\mathsf{supp}}(t)) \]and
\[ L_2 = f_{\delta ,\varepsilon }(\rho (t)) \](and hence all \( \delta \)-allowable permutations \( \rho \) such that \( (\psi _B)_\delta (\operatorname {\mathsf{supp}}(t)) = \rho (\operatorname {\mathsf{supp}}(t)) \) satisfy \( L_2 = f_{\delta ,\varepsilon }(\rho (t)) \)).
If \( L_1 \) is \( A \)-flexible, then \( L_2 \) is \( A \)-flexible.
We say that \( \psi \) is coherent if whenever \( (L_1, L_2) \in \psi _A^{\mathcal L}\), \( \psi \) is coherent at \( (A, L_1, L_2) \).
Let \( \psi \) be a base approximation, and let \( L : \mathbb N \to {\mathcal L}\) be a function such that
for all integers \( m, n, k : \mathbb Z \). Suppose that for all \( n \), \( L(n) \notin \operatorname {\mathsf{coim}}\psi ^{\mathcal L}\). Then there is an extension \( \chi \geq \psi \) such that \( \chi ^{\mathcal L}(L(n)) = L(n+1) \) and \( \operatorname {\mathsf{coim}}\chi ^{\mathcal L}= \operatorname {\mathsf{coim}}\psi ^{\mathcal L}\cup \operatorname {\mathsf{ran}}L \).
If \( \psi , \chi \) have equal exceptional atom and litter coimages, then \( (\psi \circ \chi )^{T{\mathcal A}} = \psi ^{T{\mathcal A}} \circ \chi ^{T{\mathcal A}} \).
\( (\psi ^{-1})^{\mathcal N}= (\psi ^{\mathcal N})^{-1} \), and \( \psi ^{\mathcal N}\) is permutative.
Let \( \psi \) be a coherent \( \beta \)-approximation, and let \( L \) be \( A \)-inflexible with path \( (\gamma , \delta , \varepsilon , B) \) and tangle \( t : \mathsf{Tang}_\delta \). Suppose that \( (\psi _B)_\delta \) is defined on all of \( \operatorname {\mathsf{supp}}(t) \). 2 Suppose that freedom of action holds at level \( \delta \). Then there is a coherent extension \( \chi \geq \psi \) with \( L \in \operatorname {\mathsf{coim}}\chi _A^{\mathcal L}\).
Suppose that \( \psi \) is an approximation and \( L : \mathbb Z \to {\mathcal L}\) is a function satisfying the hypotheses of proposition 4.11. Let \( \chi \) be the extension produced by the structural version of this result. 3 If \( \psi \) is coherent, and is additionally coherent at \( (L(n), L(n+1)) \) for each integer \( n \), then \( \chi \) is coherent.
If \( \psi \) and \( \chi \) are coherent and have equal coimages along all paths, then \( \psi \circ \chi \) is coherent.
If \( \psi \) is a coherent \( \beta \)-approximation and \( A \) is a path \( \beta \rightsquigarrow \beta ' \), then \( \psi _A \) is a coherent \( \beta ' \)-approximation.