protogalaxy post: add proof of Lemma 4.2

blogo-input/posts/protogalaxy.md

@@ -132,7 +132,7 @@ Our goal will be to prove that we have folded various instantiations of valid wi
 
 
 #### Lemma 4.2
-The following lemma is proven in the ProtoGalaxy paper, but for the current overview we will stick just to its results. The details can be found in the paper itself.
+The following lemma is from the ProtoGalaxy paper:
 
 > **Lemma 4.2:** Fix any polynomial $f(X) \in \mathbb{F}[X]$ and $a_0, \ldots, a_k \in \mathbb{F}$. There exists $Q(X) \in \mathbb{F}[X]$ such that
 >
@@ -140,6 +140,33 @@ The following lemma is proven in the ProtoGalaxy paper, but for the current over
 > 	f \left( \sum_{i=0}^k a_i L_i(X) \right) = \sum_{i=0}^k f(a_i) L_i(X) + Z(X) Q(X)
 > $$
 
+The way to check that the lemma is true for me was to implement it with code and check that it is satisfied. This is not a proper way, so luckily later [Héctor Masip](https://hecmas.github.io) showed me an actual proof of this lemma, which goes as follows:
+
+Recall from the [euclidean polynomial division](https://en.wikipedia.org/wiki/Polynomial_greatest_common_divisor#Euclidean_division):
+
+> For $f(X), g(X) \in \mathbb{F}[X]$ with $\deg f \geq \deg g$, $\exists$ unique polynomials $q(X), r(X) \in \mathbb{F}[X]$ such that $f(X) = g(X) q(X) + r(X)$, with $0 \leq \deg r < \deg g$.
+
+Thus,
+
+$$f(\sum_{i=0}^k a_i \cdot L_i(X)) = Q(X) \cdot Z(X) + r(X)$$
+
+with $0 \leq \deg r < \deg z = k+1$.
+
+So, when evaluating at $a_j, ~\forall j=0, \ldots, k$,
+
+$$f(\sum_{i=0}^k a_i \cdot L_i(a_j)) = f(a_j) = \underbrace{Q(a_j) \cdot Z(a_j)}_{0} + r(a_j)$$
+
+so $f(a_j)=r(a_j)$, therefore
+
+$$r(X) = \sum_{i=0}^k r(a_i) \cdot L_i(X) = \sum_{i=0}^k f(a_i) \cdot L_i(X)$$
+
+<div style="float:right;">
+
+$\square$
+
+</div>
+
+
 
 ## ProtoGalaxy protocol
 The main idea of this scheme, is to be able to fold $k+1$ instances that satisfy the relation, producing a single *folded instance* which still satisfies the relation.

public/protogalaxy.html

@@ -182,7 +182,7 @@ While, when we evaluate $L_2(X)$ at for example $\omega^1$, we will obtain a $0$
 
 <h4>Lemma 4.2</h4>
 
-<p>The following lemma is proven in the ProtoGalaxy paper, but for the current overview we will stick just to its results. The details can be found in the paper itself.</p>
+<p>The following lemma is from the ProtoGalaxy paper:</p>
 
 <blockquote>
 <p><strong>Lemma 4.2:</strong> Fix any polynomial <span class="math inline">\(f(X) \in \mathbb{F}[X]\)</span> and <span class="math inline">\(a_0, \ldots, a_k \in \mathbb{F}\)</span>. There exists <span class="math inline">\(Q(X) \in \mathbb{F}[X]\)</span> such that</p>
@@ -190,6 +190,26 @@ While, when we evaluate $L_2(X)$ at for example $\omega^1$, we will obtain a $0$
 	f \left( \sum_{i=0}^k a_i L_i(X) \right) = \sum_{i=0}^k f(a_i) L_i(X) + Z(X) Q(X)
 \]</span></p></blockquote>
 
+<p>The way to check that the lemma is true for me was to implement it with code and check that it is satisfied. This is not a proper way, so luckily later <a href="https://hecmas.github.io">Héctor Masip</a> showed me an actual proof of this lemma, which goes as follows:</p>
+
+<p>Recall from the <a href="https://en.wikipedia.org/wiki/Polynomial_greatest_common_divisor#Euclidean_division">euclidean polynomial division</a>:</p>
+
+<blockquote>
+<p>For <span class="math inline">\(f(X), g(X) \in \mathbb{F}[X]\)</span> with <span class="math inline">\(\deg f \geq \deg g\)</span>, <span class="math inline">\(\exists\)</span> unique polynomials <span class="math inline">\(q(X), r(X) \in \mathbb{F}[X]\)</span> such that <span class="math inline">\(f(X) = g(X) q(X) + r(X)\)</span>, with <span class="math inline">\(0 \leq \deg r &lt; \deg g\)</span>.</p>
+</blockquote>
+
+<p>Thus,</p>
+<p><span class="math display">\[f(\sum_{i=0}^k a_i \cdot L_i(X)) = Q(X) \cdot Z(X) + r(X)\]</span></p><p>with <span class="math inline">\(0 \leq \deg r &lt; \deg z = k+1\)</span>.</p>
+
+<p>So, when evaluating at <span class="math inline">\(a_j, ~\forall j=0, \ldots, k\)</span>,</p>
+<p><span class="math display">\[f(\sum_{i=0}^k a_i \cdot L_i(a_j)) = f(a_j) = \underbrace{Q(a_j) \cdot Z(a_j)}_{0} + r(a_j)\]</span></p><p>so <span class="math inline">\(f(a_j)=r(a_j)\)</span>, therefore</p>
+<p><span class="math display">\[r(X) = \sum_{i=0}^k r(a_i) \cdot L_i(X) = \sum_{i=0}^k f(a_i) \cdot L_i(X)\]</span></p>
+<div style="float:right;">
+
+$\square$
+
+</div>
+
 <h2>ProtoGalaxy protocol</h2>
 
 <p>The main idea of this scheme, is to be able to fold <span class="math inline">\(k+1\)</span> instances that satisfy the relation, producing a single <em>folded instance</em> which still satisfies the relation.</p>