proofs.tex

\newpage
\usepackage[english]{babel}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{corollary}{Corollary}[theorem]
\newtheorem{lemma}[theorem]{Lemma}

\section{MDL Proofs}
\label{sec:proofs}

\subsection{Proof of Correctness}

\paragraph{Theorem 1.} \textit{\protocol provides \mdl.}
\\
\\

% No real time edges %
\begin{lemma}
\label{lemma:pred_epoch_order}
    Given operations $e_1$ and $e_2$, $e_1 <_p e_2 \implies \epsilon_1 < \epsilon_2$
\end{lemma}

\begin{lemma}
\label{lemma:shard_epoch_order}
    Given operations $e_1$ and $e_2$, $e_1 <_x e_2 \implies \epsilon_1 \leq \epsilon_2$
\end{lemma}

% 1 real time edge %
\begin{lemma}
    Given operations $e_1$ and $e_2$, $e_1 \rightarrow_\alpha e_2 <_p e_3 \implies e_1 \rightarrow_\alpha e_3$
\end{lemma}

\begin{lemma}
    the minimum cycle with one real time edge must be size $m \geq 3$
\end{lemma}

\begin{lemma}
    Given operations $e_1, e_2, e_3, e_4$, $e_1 <_p e_2 \rightarrow_\alpha e_3 <_x e_4 \land shard(e_1) = shard(e_4) \implies \epsilon_1 < \epsilon_4$
\end{lemma}

\begin{lemma}
    Given operations $e_1, e_2, e_3, e_4, e_5$, $e_1 <_p e_2 <_{x_1} e_3 \rightarrow_\alpha e_4 <_{x_2} e_5 \land shard(e_1) = shard(e_5) \implies \epsilon_1 < \epsilon_5$
\end{lemma}