feat(SplitFold): add splitNth_eval_comp_pow evaluation lemma (#452)

* extract splitNth

* fix style guide violation

---------

Co-authored-by: Quang Dao <qvd@andrew.cmu.edu>

Author: klausnat

ArkLib/Data/Polynomial/SplitFold.lean

@@ -313,4 +313,19 @@ lemma foldNth_zero {s : ℕ} {α : 𝔽} : foldNth (2 ^ s) 0 α = 0 := by
       (0 : 𝔽[X]) := by rfl
   simp [this]
 
+omit [NoZeroDivisors 𝔽] in
+/--
+Lemma bridges the coefficient-level identity `splitNth_def` and
+evaluation-level reasoning about `splitNth` and `foldNth`.
+-/
+lemma splitNth_eval_comp_pow {n : ℕ} [NeZero n] (f : 𝔽[X]) (x : 𝔽) (i : Fin n) :
+    (eval₂ C (X ^ n) (splitNth f n i)).eval x = (splitNth f n i).eval (x ^ n) := by
+  rw [eval₂_eq_sum]
+  unfold Polynomial.eval
+  rw [Polynomial.eval₂_sum, eval₂_eq_sum]
+  congr
+  ext e a
+  rw [← eval]
+  simp
+
 end Polynomial

ArkLib/ProofSystem/Fri/RoundConsistency.lean

@@ -91,15 +91,6 @@ lemma generalised_round_consistency_completeness
     rw [splitNth_def n f]
   rw [Polynomial.eval_finset_sum]
   simp only [eval_mul, eval_C, eval_pow]
-  have eval_eval₂_pow_eq_eval_pow {s : 𝔽} (i) :
-      eval s (eval₂ C (X ^ n) (splitNth f n i)) = (splitNth f n i).eval (s ^ n) := by
-    rw [eval₂_eq_sum]
-    unfold Polynomial.eval
-    rw [Polynomial.eval₂_sum, eval₂_eq_sum]
-    congr
-    ext e a
-    rw [←eval]
-    simp
   conv =>
     left
     congr
@@ -110,7 +101,7 @@ lemma generalised_round_consistency_completeness
     congr
     · skip
     ext j
-    rw [eval_mul, eval_pow, eval_X, eval_eval₂_pow_eq_eval_pow]
+    rw [eval_mul, eval_pow, eval_X, splitNth_eval_comp_pow]
     rhs
     rw [mul_pow, h, one_mul]
   generalize heq : @Lagrange.interpolate 𝔽 inst1 (Fin _) _ _ _ _ = p'