Foundations: finish \cyc definition/properties

manuscrit/20_foundations/20_code_analyzers.tex

@@ -394,7 +394,7 @@ referred to as its \emph{IPC} (its unit).
     For an integer number of kernel iterations $n$,
     $\sfrac{\Delta_n\text{ret}}{\card{\kerK}} = n$. While measurement
     errors may make $\Delta_{n}\text{ret}$ fluctuate slightly, this
-    fluctuation will be below a constant threshold:
+    fluctuation will be below a constant threshold.
     \[
         \abs{\dfrac{\Delta_n\text{ret}}{\card{\kerK}} - n}
         \leq E_\text{ret}
@@ -407,8 +407,20 @@ referred to as its \emph{IPC} (its unit).
     \]
     with $E_C$ a constant.
 
-    As such, for a given $n$,  \todo{}
-\end{proof}
+    As those errors are constant, while other quantities are linear, we thus
+    have
+
+    \[
+        \cycmes{\kerK}{n} = \dfrac{\Delta_n C}{\sfrac{\Delta_n
+        ret}{\card{\kerK}}} \limarrow{n}{\infty} \dfrac{C(\kerK^n)}{n}
+    \]
+
+    and, composing limits with the previous lemma, we thus obtain
+
+    \[
+        \cycmes{\kerK}{n} \limarrow{n}{\infty} \cyc{\kerK}
+    \]
+    \end{proof}
 
 Given this property, we will use $\cyc{\kerK}$ to refer to $\cycmes{\kerK}{n}$
 for large values of $n$ in this manuscript whenever it is clear that this value