Finish the TODOs

Signed-off-by: zeramorphic <[email protected]>

blueprint/src/chapters/construction.tex

@@ -194,10 +194,10 @@ \section{Model data defined}
 \end{proof}
 \begin{definition}[new t-set]
   \label{def:NewTSet}
-  \uses{prop:AllPerm.smul_cloud_smul,prop:Path.rec}
+  \uses{prop:AllPerm.smul_cloud_smul}
   A \emph{new t-set} is an even code \( c \) such that there is an \( \alpha \)-support that supports \( c \) under the action of new allowable permutations, or a designated object called the empty set.
   New allowable permutations act on new t-sets in the same way that they act on codes, and map the empty set to itself.
-  We define the map \( U_\alpha \) from new t-sets to \( \StrSet_\alpha \) by cases from the top of the path in the obvious way (using \cref{prop:Path.rec} and the membership relation from \cref{prop:Code.ext}).
+  We define the map \( U_\alpha \) from new t-sets to \( \StrSet_\alpha \) by cases from the top of the path in the obvious way (using recursion on paths and the membership relation from \cref{prop:Code.ext}).
   It is easy to check that \( \rho(U_\alpha(x)) = U_\alpha(\rho(x)) \) by \cref{prop:AllPerm.smul_cloud_smul}.
 \end{definition}
 \begin{definition}[new model data]

blueprint/src/chapters/counting.tex

@@ -20,15 +20,27 @@ \section{Strong supports}
   If \( S \) is a strong \( \beta \)-support and \( \rho \) is \( \beta \)-allowable, then \( \rho(S) \) is strong.
 \end{proposition}
 \begin{proof}
-  TODO
+  Interference is stable under application of allowable permutations, and the required supports are also preserved under action of allowable permutations.
 \end{proof}
 \begin{proposition}
   \uses{def:Strong}
   \label{prop:exists_strong}
   For every support \( S \), there is a strong support \( T \succeq S \).
 \end{proposition}
 \begin{proof}
-  TODO
+  We define a relation \( R \) on pairs \( (A, N) \) where \( A : \beta \tpath \bot \) and \( N \) is a near-litter by the following constructor.
+  If \( I = (\gamma,\delta,\varepsilon,A) \) and \( t : \Tang_\delta \), then for any near-litter \( N_1 \) such that \( N_1^\circ = f_{\delta,\varepsilon}(t) \) and any path \( B : \delta \tpath \bot \) and near-litter \( N_2 \in \supp(t)_B^\NearLitter \), we define \( ((A_\delta)_B, N_2) \mathrel{R} ((A_\varepsilon)_\bot, N_1) \).
+  This is well-founded, because if \( (B, N_2) \mathrel{R} (A, N_1) \) then \( \iota(N_2) < \iota(N_1) \).
+  For any small set \( s \) of such pairs, the transitive closure of \( s \) under \( R \) is small.
+
+  Let \( S \) be a support, and let \( s \) be the transitive closure of the set of pairs \( (A, N) \) such that \( N \in \im S_A^\NearLitter \).
+  Generate a support \( T \) from \( S \) and \( s \) using the fact that every small set is the range of some enumeration.
+  This satisfies the second condition of being a strong support.
+
+  Now, for any base support \( T \), we define its \emph{interference support} to be a base support \( U \) consisting of just the atoms in the interference of all near-litters that appear in \( T \).
+  We may extend this definition to structural supports.
+
+  Finally, if \( U \) is the interference support of the \( T \) defined above, the support \( T + U \) is strong, and since \( S \succeq T \), we conclude \( S \preceq T + U \).
 \end{proof}
 
 \section{Coding functions}
@@ -148,9 +160,9 @@ \section{Specifications}
 \end{proof}
 \begin{proposition}
   \uses{def:StrSupport.spec}
-  \label{def:spec_smul}
+  \label{prop:spec_smul}
   Let \( \rho \) be \( \beta \)-allowable, and let \( S \) be a \( \beta \)-support.
-  Then \( \spec(\rho(S)) = \spec(S) \).\footnote{TODO: Consider removing this; I don't think it's used.}
+  Then \( \spec(\rho(S)) = \spec(S) \).
 \end{proposition}
 \begin{proof}
   \uses{prop:spec_eq_spec_iff}
@@ -182,7 +194,7 @@ \section{Specifications}
   \uses{def:BaseSupport}
   \label{def:conv_base}
   Let \( S \) and \( T \) be base supports.
-  We define the relations \( \conv_{S,T}^\Atom, \conv_{S,T}^\NearLitter \) by the constructors\footnote{TODO: We should abstract this out even further. This can be defined for any pair of relations with common domain.}
+  We define the relations \( \conv_{S,T}^\Atom, \conv_{S,T}^\NearLitter \) by the constructors\footnote{This should be abstracted out even further; this can be defined for any pair of relations with common domain.}
   \begin{align*}
     &(i, a_1) \in S^\Atom \to (i, a_2) \in T^\Atom \to (a_1, a_2) \in \conv_{S,T}^\Atom \\
     &(i, N_1) \in S^\NearLitter \to (i, N_2) \in T^\NearLitter \to (N_1, N_2) \in \conv_{S,T}^\NearLitter

blueprint/src/chapters/environment.tex

@@ -101,7 +101,14 @@ \section{The structural hierarchy}
 \begin{definition}[path]
   \label{def:Path}
   \uses{def:TypeIndex}
-  If \( \alpha, \beta \) are type indices, then a \emph{path} \( \alpha \tpath \beta \) is a nonempty finite subset of \( \lambda^\bot \) with maximal element \( \alpha \) and minimal element \( \beta \).\footnote{In previous versions, we used ordered lists (more precisely, a quiver structure) to represent paths. This had the effect that editing paths at the bottom was much easier than editing paths at the top. In this implementation, we are making the decision to put both types of edit on equal footing (and neither will definitionally reduce). TODO: It might be cleaner to still use a cons-list format but encapsulate it lots.}
+  If \( \alpha, \beta \) are type indices, then a \emph{path} \( \alpha \tpath \beta \) is given by the constructors
+  \begin{itemize}
+    \item \( \newoperator{nil} : \alpha \tpath \alpha \);
+    \item \( \newoperator{cons} : (\gamma < \beta) \to (\alpha \tpath \beta) \to (\alpha \tpath \gamma) \).
+  \end{itemize}
+  We define by recursion a \( \newoperator{snoc} \) operation on the top of paths.
+  We also prove the induction principle for \( \newoperator{nil} \) and \( \newoperator{snoc} \).
+
   A path \( \alpha \tpath \bot \) is called an \emph{\( \alpha \)-extended index}.
   We write \( \nil(\alpha) \) for the path \( \{ \alpha \} : \alpha \tpath \alpha \).
   If \( h \) is a proof of \( \beta < \alpha \), we write \( \single(h) \) for the path \( \{ \alpha, \beta \} : \alpha \tpath \beta \).
@@ -152,19 +159,6 @@ \section{The structural hierarchy}
   If \( A : \alpha \tpath \beta \) and \( B : \beta \tpath \gamma \), the derivative \( A_B \) is defined to be the union \( A \cup B : \alpha \tpath \gamma \), and the coderivative \( B^A \) is defined to be \( A_B \).
 \end{definition-no-bp}
 
-\begin{proposition}[induction along paths]
-  \label{prop:Path.rec}
-  \uses{def:Path}
-  Fix a type index \( \alpha \) and universe \( u \), and let
-  \[ C : \prod_{\beta : \lambda^\bot} (\alpha \tpath \beta) \to \Sort_u \]
-  Let
-  \[ n : C(\alpha, \nil(\alpha));\quad c : \prod_{\beta, \gamma : \lambda^\bot} \prod_{A : \alpha \tpath \beta} \prod_{h : \gamma < \beta} C(\beta, A) \to C(\beta, A_h) \]
-  Then there is a term
-  \[ x : \prod_{\beta : \lambda^\bot} \prod_{A : \alpha \tpath \beta} C(\beta, A) \]
-  such that
-  \[ x(\alpha, \nil(\alpha)) = n;\quad x(\gamma, A_h) = c(\beta, \gamma, A, h, x(\beta, A)) \]
-  The same holds for paths pointing in the reverse direction.
-\end{proposition}
 \begin{definition}[tree]
   \label{def:Tree}
   \uses{def:Path}
@@ -226,16 +220,20 @@ \section{The structural hierarchy}
 \begin{definition}[structural support]
   \label{def:StrSupport}
   \uses{def:BaseSupport,def:Tree}
-  A \emph{\( \beta \)-structural support} (or just \emph{\( \beta \)-support}) is a \( \beta \)-tree of base supports.
+  A \emph{\( \beta \)-structural support} (or just \emph{\( \beta \)-support}) is a pair \( S = (S^\Atom, S^\NearLitter) \) where \( S^\Atom \) is an enumeration of \( (\beta \tpath \bot) \times \Atom \) and \( S^\NearLitter \) is an enumeration of \( (\beta \tpath \bot) \times \NearLitter \).
   The type of \( \beta \)-supports is written \( \StrSupp_\beta \).
   There are precisely \( \#\mu \) structural supports for any type index \( \beta \).
-  Following \cref{def:Tree}, structural supports have derivatives, structural permutations act on structural supports, and there is a group action of \( \beta \)-permutations on \( \beta \)-supports.
-  If \( S \) is a \( \beta \)-support and \( A : \alpha \tpath \beta \), the coderivative \( S^A \) is the \( \alpha \)-support given by
-  \[ (S^A)_B = \begin{cases}
-    S_C & \text{if } B = A_C \text{ for some } C \\
-    \varnothing & \text{otherwise}
-  \end{cases} \]
-  Thus \( (S^A)_A = S \).
+
+  For a path \( A : \beta \tpath \bot \), we write \( S_A \) for the base support \( T \) given by
+  \[ T^\Atom = \{ (i, a) \mid (i, (A, a)) \in S^\Atom \};\quad T^\NearLitter = \{ (i, N) \mid (i, (A, N)) \in S^\NearLitter \} \]
+  More generally, for a path \( A : \beta \tpath \gamma \), we write \( S_A \) for the \( \gamma \)-support \( T \) given by
+  \[ T^\Atom = \{ (i, (B, a)) \mid (i, (A_B, a)) \in S^\Atom \};\quad T^\NearLitter = \{ (i, (B, N)) \mid (i, (A_B, N)) \in S^\NearLitter \} \]
+  For a path \( A : \alpha \tpath \beta \), we write \( S^A \) for the \( \alpha \)-support \( T \) given by
+  \[ T^\Atom = \{ (i, (A_B, a)) \mid (i, (B, a)) \in S^\Atom \};\quad T^\NearLitter = \{ (i, (A_B, N)) \mid (i, (B, N)) \in S^\NearLitter \} \]
+  Clearly, \( (S^A)_A = S \).
+
+  \( \beta \)-structural permutations act on pairs \( (A, x) \) by \( \pi(A, x) = (A, \pi_A(x)) \), where \( x \) is either an atom or a near-litter.
+  Hence, structural permutations act on structural supports.
 
   Let \( \tau \) be a type, and let \( G \) be a \( \texttt{StrPermClass}_\beta \)-group that acts on \( \tau \).
   We say that \( S \) \emph{supports} \( x : \tau \) under the action of \( G \) if whenever \( \pi : G \) fixes \( S \), it also fixes \( x \), and moreover, if \( \beta = \bot \) then \( S_A^\NearLitter \) is empty for any \( A : \bot \tpath \bot \) (and of course there is exactly one such path).
@@ -368,13 +366,13 @@ \section{Hypotheses of the recursion}
 \end{definition}
 \begin{definition}[coherent data]
   \label{def:CoherentData}
-  \uses{def:TypedNearLitter,prop:Path.rec,def:InflexiblePath}
+  \uses{def:TypedNearLitter,def:InflexiblePath}
   Let \( \alpha \) be a proper type index.
   Suppose that we have model data for all type indices \( \beta \leq \alpha \), position functions for \( \Tang_\beta \) for all \( \beta < \alpha \), and typed near-litters for all \( \beta < \alpha \).
   We say that the model data is \emph{coherent} below level \( \alpha \) if the following hold.
   \begin{itemize}
     \item For \( \gamma < \beta \leq \alpha \), there is a map \( \AllPerm_\beta \to \AllPerm_\gamma \) that commutes with the coercions from \( \AllPerm_{(-)} \) to \( \StrPerm_{(-)} \).
-    We can use this map to define arbitrary derivatives of allowable permutations by \cref{prop:Path.rec}.
+    We can use this map to define arbitrary derivatives of allowable permutations by recursion on paths.
     \item If \( (x, S) \) is a \( \beta \)-tangle for \( \beta < \alpha \), and \( y \) is an atom or near-litter that occurs in the range of \( S_A \), then \( \iota(y) < \iota(x, S) \).
     \item Let \( \beta \leq \alpha \), and let \( \gamma, \delta < \beta \) be distinct with \( \delta \) proper.
     Let \( t : \Tang_\gamma \) and \( \rho : \AllPerm_\beta \).

blueprint/src/chapters/induction.tex

@@ -70,7 +70,7 @@ \section{Building the tower}
   For a proper type index \( \alpha \), the \emph{main motive} at \( \alpha \) is the type \( \Motive_\alpha \) consisting of model data at \( \alpha \), a position function for \( \Tang_\alpha \), and typed near-litters at \( \alpha \), such that if \( (x, S) \) is an \( \alpha \)-tangle and \( y \) is an atom or near-litter that occurs in the range of \( S_A \), then \( \iota(y) < \iota(x, S) \).
 \end{definition}
 \begin{definition}
-  \uses{def:MainMotive,def:TypedNearLitter,prop:Path.rec,def:InflexiblePath}
+  \uses{def:MainMotive,def:TypedNearLitter,def:InflexiblePath}
   \label{def:MainHypothesis}
   We define the \emph{main hypothesis}
   \[ \Hypothesis : \prod_{\alpha : \lambda} \Motive_\alpha \to \left( \prod_{\beta < \alpha} \Motive_\beta \right) \to \Type_{u+1} \]

blueprint/src/chapters/model.tex

@@ -45,17 +45,27 @@ \section{Raising strong supports}
   Follows directly from \cref{prop:Strong.smul,prop:raiseStrong}.
 \end{proof}
 \begin{proposition}
-  \uses{prop:exists_strong,def:StrSupport.spec}
-  \label{prop:raiseRaise_spec}
-  Let \( S \) be a strong \( \alpha \)-support and let \( T \) be a \( \gamma \)-support.
-  Let \( U \) be the strong support generated by \( T^\beta \), and let \( V \) be the support whose image is precisely those atoms in the interference of \( S_\beta \) and \( U \).
-  Let \( \rho \) be a \( \beta \)-allowable permutation that fixes \( S_\beta \).
-  Then \( S + (U + V)^\alpha \) and \( S + (\rho(U + V))^\alpha \) have the same specification.
+  \label{prop:combineStrong}
+  Let \( S \) be a strong \( \alpha \)-support.
+  Let \( U \) be a strong \( \beta \)-support with the property that if \( A \) is a path such that \( \im U_A^\NearLitter \) is nonempty, then \( A \) has length at least 2.
+  Then for every \( \beta \)-allowable \( \rho \) that fixes \( S_\beta \), we have \( \spec(S + U^\alpha) = \spec(S + (\rho(U))^\alpha) \).
 \end{proposition}
 \begin{proof}
-  \uses{prop:spec_eq_spec_iff,prop:raiseStrong}
-  We appeal to \cref{prop:spec_eq_spec_iff}.
-  TODO
+  Appeal to \cref{prop:spec_eq_spec_iff}.
+  First, note that \( (i, a) \in (S + (\rho(U))^\alpha)_A^\Atom \) if and only if \( (i, a) \in S \) or \( A = B^\alpha \) and \( (i, a) \in \rho(U)_B^\Atom \).
+  Thus,
+  \begin{align*}
+    (i, a_1) \in (S + U^\alpha)_A^\Atom &\to \exists a_2,\, (i, a_2) \in (S + (\rho(U))^\alpha)_A^\Atom \\
+    &\quad\wedge [(\exists B,\, A = B^\alpha \wedge \rho_B(a_1) = a_2) \vee ((\forall B,\, A \neq B^\alpha) \wedge a_1 = a_2)]
+  \end{align*}
+  and the same holds for the other direction\footnote{We can prove the other direction easily from this by substituting \( \rho(U) \) and \( \rho^{-1} \).} and for near-litters.
+
+  The coimage condition is clear.
+  Suppose that \( (i, a_1) \in (S + U^\alpha)_A^\Atom \) and \( (i, a_2) \in (S + (\rho(U))^\alpha)_A^\Atom \).
+  Then by coinjectivity we can apply the above result, giving that either there is \( B \) such that \( A = B^\alpha \) and \( \rho_B(a_1) = a_2 \), or there is no such \( B \), and \( a_1 = a_2 \).
+  In either case, the result is easy to show.
+
+  The result for litters follows from the fact that the condition on \( U \) implies that proofs of inflexiblity of litters in \( U \) correspond bijectively to proofs of inflexibility of litters in \( U^\alpha \).
 \end{proof}
 \begin{proposition}
   \uses{def:Strong}
@@ -66,8 +76,9 @@ \section{Raising strong supports}
   \[ \rho'(S) = S;\quad (\rho'_\beta)_\gamma(T) = \rho_\gamma(T) \]
 \end{proposition}
 \begin{proof}
-  \uses{prop:exists_allowable_of_spec_eq_spec,prop:raiseRaise_strong,prop:raiseRaise_spec}
-  Apply \cref{prop:exists_allowable_of_spec_eq_spec,prop:raiseRaise_strong,prop:raiseRaise_spec}.
+  \uses{prop:exists_allowable_of_spec_eq_spec,prop:raiseRaise_strong,prop:raiseStrong_length,prop:combineStrong}
+  Let \( U \) be the strong support generated by \( T^\beta \), and let \( V \) be the support whose image is precisely those atoms in the interference of \( S_\beta \) and \( U \).
+  Then apply \cref{prop:exists_allowable_of_spec_eq_spec,prop:raiseRaise_strong,prop:raiseStrong_length,prop:combineStrong}.
 \end{proof}
 
 \section{Tangled type theory}

blueprint/src/chapters/model_theory.tex

@@ -104,4 +104,4 @@ \section{Ambiguity}
   Let \( L \) be an \( \mathbb N \)-language.
   A \emph{type raising morphism} is a map of languages \( L \xrightarrow{\newoperator{succ}} L \), where \( \newoperator{succ} : \mathbb N \to \mathbb N \) is the successor function.
 \end{definition}
-TODO
+The remainder of this chapter is left unfinished until we finish the main part of the project.

blueprint/src/content.tex

@@ -30,10 +30,6 @@ \chapter{Model theory and verifying \texorpdfstring{\( \Con(\NF) \)}{Con(NF)}}
 \label{c:model_theory}
 \input{chapters/model_theory.tex}
 
-\chapter{Conclusion}
-\label{c:conclusion}
-\input{chapters/conclusion.tex}
-
 \appendix
 \chapter{Auxiliary results}
 \label{c:auxiliary}