From 2f6706752d8428a23028d3d49a23fca3c4872a56 Mon Sep 17 00:00:00 2001 From: arnaucube Date: Tue, 21 Nov 2023 17:35:21 +0100 Subject: [PATCH] protogalaxy post: add proof of Lemma 4.2 --- blogo-input/posts/protogalaxy.md | 29 ++++++++++++++++++++++++++++- public/protogalaxy.html | 22 +++++++++++++++++++++- 2 files changed, 49 insertions(+), 2 deletions(-) diff --git a/blogo-input/posts/protogalaxy.md b/blogo-input/posts/protogalaxy.md index d02b5d1..1c009bb 100644 --- a/blogo-input/posts/protogalaxy.md +++ b/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)$$ + +
+ +$\square$ + +
+ + ## 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. diff --git a/public/protogalaxy.html b/public/protogalaxy.html index 19edad8..2c1fac9 100644 --- a/public/protogalaxy.html +++ b/public/protogalaxy.html @@ -182,7 +182,7 @@ While, when we evaluate $L_2(X)$ at for example $\omega^1$, we will obtain a $0$

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

@@ -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) \]

+

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 showed me an actual proof of this lemma, which goes as follows:

+ +

Recall from the euclidean polynomial 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)\]

+
+ +$\square$ + +
+

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.