diff --git a/ArkLib.lean b/ArkLib.lean index e82af39234..1f31d1d9d6 100644 --- a/ArkLib.lean +++ b/ArkLib.lean @@ -77,6 +77,7 @@ import ArkLib.Data.CodingTheory.ProximityGap.DG25.Basic import ArkLib.Data.CodingTheory.ProximityGap.DG25.MainResults import ArkLib.Data.CodingTheory.ProximityGap.DG25.ReedSolomon import ArkLib.Data.CodingTheory.ProximityGap.Folding +import ArkLib.Data.CodingTheory.ProximityGap.Folding.Multilinear import ArkLib.Data.CodingTheory.ProximityGap.MCAGenerator import ArkLib.Data.CodingTheory.ProximityGap.ProximityGenerators import ArkLib.Data.CodingTheory.ReedSolomon @@ -142,6 +143,7 @@ import ArkLib.Data.Matrix.Sparse import ArkLib.Data.Matrix.Vandermonde import ArkLib.Data.Misc.Basic import ArkLib.Data.MvPolynomial.Degrees +import ArkLib.Data.MvPolynomial.EvenAndOdd import ArkLib.Data.MvPolynomial.Interpolation import ArkLib.Data.MvPolynomial.LinearMvExtension import ArkLib.Data.MvPolynomial.Multilinear diff --git a/ArkLib/Data/CodingTheory/ProximityGap/Folding.lean b/ArkLib/Data/CodingTheory/ProximityGap/Folding.lean index 97b1d8b3cb..5e866219ec 100644 --- a/ArkLib/Data/CodingTheory/ProximityGap/Folding.lean +++ b/ArkLib/Data/CodingTheory/ProximityGap/Folding.lean @@ -262,6 +262,34 @@ theorem foldWord_k_1 [NeZero n] {i : Fin (2 ^ (n - 1))} {α : F} : ((f i + f i') / 2) + α * ((f i - f i') / (2 * x)) := by simp [foldWord, foldValue_k_1] +/-- An explicit formula for `foldWord` when `k = 1` that + does not use Lagrange interpolation. Function-level version. -/ +theorem foldWord_k_1' [NeZero n] {α : F} : + foldWord domain f 1 α = fun i ↦ + let x : domain := CosetFftDomain.twoNthRoot (i := 1) + ⟨domain.subdomain 1 i, by simp⟩ + let i := domain.log x + let i' := domain.log ⟨-x.1, by obtain ⟨x, hx⟩ := x; simpa using hx⟩ + ((f i + f i') / 2) + α * ((f i - f i') / (2 * x)) := by aesop (add simp [foldWord_k_1]) + +/-- The version of a folding where + k steps are achieved via iterated application + of k=1 folding. -/ +noncomputable def iteratedFoldWord (domain : SmoothCosetFftDomain n F) + (f : Word F (Fin (2 ^ n))) (k : ℕ) (α : Fin k → F) : + Word F (Fin (2 ^ (n - k))) := + match k with + | 0 => f + | Nat.succ k => + let prev := iteratedFoldWord domain f k (fun i ↦ α ⟨i.val, by omega⟩) + let foldedPrev := + foldWord (domain.subdomain k) prev 1 (α ⟨k, by omega⟩) + fun i ↦ foldedPrev ⟨i.val, by aesop (add safe cases Fin)⟩ + +@[simp] +lemma iteratedFoldWord_zero {α : Fin 0 → F} : + iteratedFoldWord domain f 0 α = f := rfl + omit [DecidableEq F] in /-- TODO: this will go once this https://github.com/Verified-zkEVM/CompPoly/pull/203 is merged. -/ @@ -417,6 +445,49 @@ theorem foldWord_mem_code_of_mem_code {d : ℕ} rw [ReedSolomon.toPolynomial_eval_at_domain] simp [evalOnPoints] +private lemma div_two_pow_div_two (d k : ℕ) : + d / 2 ^ k / 2 ^ 1 = d / 2 ^ (k + 1) := by + rw [pow_one, Nat.div_div_eq_div_mul, ←pow_succ] + +/-- Perfect completeness of iterated folding: if a word belongs to an RS-code + then its `iteratedFoldWord` belongs to a folded RS-code. +-/ +theorem iteratedFoldWord_mem_code_of_mem_code {d : ℕ} + {α : Fin k → F} + (hk : k ≤ n) + (hk_d_dvd : 2 ^ k ∣ d) + {f : Word F (Fin (2 ^ n))} + (hf : f ∈ ReedSolomon.code (domain : Fin (2 ^ n) ↪ F) d) : + iteratedFoldWord domain f k α ∈ + ReedSolomon.code (domain.subdomain k : Fin (2 ^ (n - k)) ↪ F) (d / (2 ^ k)) := by + induction k with + | zero => simp [hf] + | succ k ih => + have hdvd_k : 2 ^ k ∣ d := dvd_trans (pow_dvd_pow 2 (Nat.le_succ k)) hk_d_dvd + have hprev := ih (α := fun i ↦ α ⟨i.val, by omega⟩) (by omega) hdvd_k + have hk1 : (1 : ℕ) ≤ n - k := by omega + have hdvd1 : (2 : ℕ) ^ 1 ∣ d / 2 ^ k := by + obtain ⟨c, rfl⟩ := hk_d_dvd + refine ⟨c, ?_⟩ + rw [pow_succ, mul_assoc, Nat.mul_div_cancel_left _ (by positivity), pow_one] + have hfold := foldWord_mem_code_of_mem_code (domain := domain.subdomain k) (k := 1) + (α := α ⟨k, by omega⟩) hk1 hdvd1 hprev + rw [ReedSolomon.mem_code_iff_exists_polynomial] at hfold + obtain ⟨p, hpdeg, hpeval⟩ := hfold + rw [div_two_pow_div_two] at hpdeg + have hunfold : iteratedFoldWord domain f (k + 1) α = + fun i : Fin (2 ^ (n - (k + 1))) ↦ + foldWord (domain.subdomain k) + (iteratedFoldWord domain f k (fun j ↦ α ⟨j.val, by omega⟩)) 1 + (α ⟨k, by omega⟩) ⟨i.val, by rw [Nat.sub_sub]; exact i.isLt⟩ := rfl + rw [hunfold, ReedSolomon.mem_code_iff_exists_polynomial] + refine ⟨p, hpdeg, ?_⟩ + funext i + have hb := subdomain_one_comp (ω := domain) hk ⟨i.val, by rw [Nat.sub_sub]; exact i.isLt⟩ i rfl + simp only [hpeval, ReedSolomon.evalOnPoints, Function.Embedding.coeFn_mk, LinearMap.coe_mk, + AddHom.coe_mk] + rw [hb] + private noncomputable def foldWordAuxCoeff (domain : SmoothCosetFftDomain n F) (f : Word F (Fin (2 ^ n))) (k : ℕ) (i : Fin k) (x : F) : F := (foldWordAux domain f k x).coeff i diff --git a/ArkLib/Data/CodingTheory/ProximityGap/Folding/Multilinear.lean b/ArkLib/Data/CodingTheory/ProximityGap/Folding/Multilinear.lean new file mode 100644 index 0000000000..5aa90ab011 --- /dev/null +++ b/ArkLib/Data/CodingTheory/ProximityGap/Folding/Multilinear.lean @@ -0,0 +1,182 @@ +/- +Copyright (c) 2024-2026 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ilia Vlasov, Aristotle (Harmonic) +-/ + +import Mathlib.Algebra.Polynomial.Roots +import Mathlib.LinearAlgebra.Lagrange + +import ArkLib.Data.CodingTheory.ProximityGap.Basic +import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Curves +import ArkLib.Data.CodingTheory.ProximityGap.Folding +import ArkLib.Data.Domain.CosetFftDomain.Subdomain +import ArkLib.Data.Domain.CosetFftDomain.Log +import ArkLib.Data.MvPolynomial.EvenAndOdd +import CompPoly.Data.MvPolynomial.Notation + +/-! This module provides an equivalent statement + of folding completeness of RS-codes in terms of multilinear polynomials + as can be found in [ACFY24]. + +## References + + * [Arnon, G., Chiesa, A., Fenzi, G., and Yogev, E., *WHIR: Reed–Solomon Proximity Testing + with Super-Fast Verification*][ACFY24] +-/ + +namespace ProximityGap + +open NNReal Finset Function +open scoped ProbabilityTheory +open scoped BigOperators LinearCode +open Code Affine ReedSolomon +open Domain +open CosetFftDomain CosetFftDomainClass +open MvPolynomial LinearMvExtension + +variable {F : Type} [Field F] [DecidableEq F] +variable {n : ℕ} +variable {domain : SmoothCosetFftDomain n F} {f : Word F (Fin (2 ^ n))} +variable {k : ℕ} {x : F} + +/-- One step of lemma 4.15 from [ACFY24]. -/ +lemma foldWord_eq_evalOnPoints_powAlgHom [NeZero n] {α : F} + {g : F⦃≤ 1⦄[X (Fin n)]} + (hf : f = evalOnPoints domain (powAlgHom g.1)) : + foldWord domain f 1 α = + evalOnPoints + (domain.subdomain 1) + (powAlgHom (g.1.aeval (fun i ↦ + if h : i = 0 then C α else MvPolynomial.X (⟨i.val - 1, by omega⟩ : Fin (n - 1))))) := by + have hchar := CosetFftDomainClass.domain_implies_char_ne_2 domain + have h2ne0 : (2 : F) ≠ 0 := fun contra ↦ hchar <| + ringChar.of_eq (CharP.ringChar_of_prime_eq_zero Nat.prime_two contra) + subst hf + conv_lhs => + rw [powAlgHom_eq_even_add_odd_powAlgHom hchar] + rw [even_and_odd_eval hchar, foldWord_k_1'] + ext u + extract_lets x j j' + have : x.val ≠ 0 := fun contra ↦ by + have := x.2 + simp_all + aesop + (add safe (by field_simp)) + (add simp + [evalOnPoints, + subdomain_sqFoldMapGen_eq_pow_domain, + evalOnPoints_sq_eq_evalOnPoints_subdomain]) + (add unsafe + [(by ring_nf), + (by rw [add_comm, mul_comm]), + sqFoldMapGen_eq_sqFoldMapGen_of_pow_apply_eq_pow_apply]) + +private noncomputable def substFun (m : ℕ) (β : Fin m → F) (i : Fin n) : + MvPolynomial (Fin (n - m)) F := + if h : i.val < m then MvPolynomial.C (β ⟨i.val, h⟩) + else MvPolynomial.X ⟨i.val - m, by omega⟩ + +omit [DecidableEq F] in +private lemma aeval_substFun_comp {k : ℕ} [NeZero (n - k)] (γ : Fin (k + 1) → F) + (g0 : MvPolynomial (Fin n) F) : + (MvPolynomial.aeval (substFun k (fun j ↦ γ ⟨j.val, by omega⟩)) g0).aeval + (fun i : Fin (n - k) ↦ if h : i = 0 then MvPolynomial.C (γ ⟨k, by omega⟩) + else MvPolynomial.X (⟨i.val - 1, by omega⟩ : Fin (n - k - 1))) + = MvPolynomial.aeval (substFun (k + 1) γ) g0 := by + rw [MvPolynomial.comp_aeval_apply] + refine congrArg (fun φ ↦ MvPolynomial.aeval φ g0) ?_ + funext i + unfold substFun + by_cases h1 : i.val < k + · rw [dif_pos h1, dif_pos (show i.val < k + 1 by omega)] + simp + · rw [dif_neg h1] + by_cases h2 : i.val = k + <;> aesop (add safe (by grind)) + +private lemma aeval_split_mem {n : ℕ} [NeZero n] {R : Type} [Field R] + (hchar : ¬CharP R 2) + (p : R⦃≤ 1⦄[X (Fin n)]) (α : R) : + p.1.aeval + (fun i ↦ if h : i = 0 then C α else (MvPolynomial.X ⟨i.val - 1, by omega⟩ : R[X (Fin (n - 1))])) + ∈ restrictDegree (Fin (n - 1)) R 1 := by + rw [even_and_odd_eval hchar] + exact Submodule.add_mem _ (even_pred p).2 + (by rw [MvPolynomial.C_mul']; exact Submodule.smul_mem _ _ (odd_pred p).2) + +omit [DecidableEq F] in +private lemma aeval_substFun_mem [NeZero n] {gg : F⦃≤ 1⦄[X (Fin n)]} + {domain : SmoothCosetFftDomain n F} : + ∀ (m : ℕ), m ≤ n → ∀ (β : Fin m → F), + MvPolynomial.aeval (substFun m β) gg.1 ∈ MvPolynomial.restrictDegree (Fin (n - m)) F 1 := by + intro m + induction m with + | zero => + intro hm β + have : (substFun (n := n) 0 β) = MvPolynomial.X := by aesop + aesop + | succ m ih => + intro hm β + haveI : NeZero (n - m) := ⟨by omega⟩ + have hchar : ¬CharP F 2 := CosetFftDomainClass.domain_implies_char_ne_2 domain + have hq : MvPolynomial.aeval (substFun m (fun j ↦ β ⟨j.val, by omega⟩)) gg.1 ∈ + MvPolynomial.restrictDegree (Fin (n - m)) F 1 := ih (by omega) _ + have hmem : + (MvPolynomial.aeval (substFun m (fun j ↦ β ⟨j.val, by omega⟩)) gg.1).aeval + (fun i : Fin (n - m) ↦ if h : i = 0 then MvPolynomial.C (β ⟨m, by omega⟩) + else MvPolynomial.X (⟨i.val - 1, by omega⟩ : Fin (n - m - 1))) + ∈ MvPolynomial.restrictDegree (Fin (n - m - 1)) F 1 := + aeval_split_mem hchar ⟨_, hq⟩ (β ⟨m, by omega⟩) + rw [←aeval_substFun_comp (k := m) β gg.1] + exact hmem + +/-- Lemma 4.15 from [ACFY24]. Provides a way to + compute the corresponding multilinear extension + for the interated folding of codewords. -/ +theorem iteratedFoldWord_eq_evalOnPoints_powAlgHom [NeZero n] {α : Fin k → F} + {g : F⦃≤ 1⦄[X (Fin n)]} + (hk : k ≤ n) + (hf : f = evalOnPoints domain (powAlgHom g.1)) : + iteratedFoldWord domain f k α = + evalOnPoints + (domain.subdomain k) + (powAlgHom (g.1.aeval (fun i ↦ + if h : i.val < k then C (α ⟨i.val, h⟩) else MvPolynomial.X + (⟨i.val - k, by omega⟩ : Fin (n - k))))) := by + suffices H : ∀ (k : ℕ), k ≤ n → ∀ (α : Fin k → F), + iteratedFoldWord domain f k α + = evalOnPoints (domain.subdomain k) (powAlgHom (g.1.aeval (substFun k α))) by + exact H k hk α + intro k + induction k with + | zero => + intro _ α + have : (substFun (n := n) 0 α) = MvPolynomial.X := by aesop + aesop + | succ k ih => + intro hk α + haveI : NeZero (n - k) := ⟨by omega⟩ + have hprev : iteratedFoldWord domain f k (fun j ↦ α ⟨j.val, by omega⟩) + = evalOnPoints (domain.subdomain k) + (powAlgHom (g.1.aeval (substFun k (fun j ↦ α ⟨j.val, by omega⟩)))) := + ih (by omega) _ + have hmem := aeval_substFun_mem (domain := domain) (gg := g) k (by omega) + (fun j ↦ α ⟨j.val, by omega⟩) + have hfold := foldWord_eq_evalOnPoints_powAlgHom + (domain := domain.subdomain k) + (f := iteratedFoldWord domain f k (fun j ↦ α ⟨j.val, by omega⟩)) + (α := α ⟨k, by omega⟩) + (g := ⟨g.1.aeval (substFun k (fun j ↦ α ⟨j.val, by omega⟩)), hmem⟩) + hprev + funext i + have hi2 : i.val < 2 ^ (n - k - 1) := by grind + change foldWord (domain.subdomain k) + (iteratedFoldWord domain f k (fun j ↦ α ⟨j.val, by omega⟩)) 1 (α ⟨k, by omega⟩) + ⟨i.val, hi2⟩ = _ + rw [hfold] + simp only [evalOnPoints, Function.Embedding.coeFn_mk, LinearMap.coe_mk, AddHom.coe_mk] + rw [aeval_substFun_comp (k := k) (γ := α) g.1, + subdomain_one_comp (ω := domain) (by omega) ⟨i.val, hi2⟩ i rfl] + +end ProximityGap diff --git a/ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean b/ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean index 4ab226a928..9aea8e0182 100644 --- a/ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean +++ b/ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean @@ -18,6 +18,7 @@ import Mathlib.Tactic.Field import ArkLib.Data.Domain.CosetFftDomain.Ops import ArkLib.Data.Domain.FftDomain.Ops +import ArkLib.Data.CodingTheory.ReedSolomon /-! # Subdomains of smooth coset FFT domains @@ -450,6 +451,234 @@ lemma square_roots_explicit [DecidableEq F] {i : ℕ} (hi : i < n) {y : F} · have hy_mem : y ∈ subdomain ω i := sq_root_mem_subdomain hi hx hy simp_all [Finset.subset_iff] +/-- The generalized modular reduction map from `Fin (2^n)` to `Fin (2^(n-i))`, +sending `u` to `u % 2^(n-i)`. Can be used to compute indices of powers of subdomain memebers. -/ +def sqFoldMapGen {i : ℕ} (u : Fin (2 ^ n)) : Fin (2 ^ (n - i)) := + ⟨u.val % 2 ^ (n - i), Nat.mod_lt _ (Nat.two_pow_pos _)⟩ + +/-- `ReedSolomon.evalOnPoints` related on the domain and a subdomain. -/ +lemma evalOnPoints_pow_of_two_eq_evalOnPoints_subdomain + [NeZero n] {p : Polynomial F} {i : ℕ} : + ReedSolomon.evalOnPoints (ω : Fin (2 ^ n) ↪ F) (p.comp (Polynomial.X ^ (2 ^ i))) = + (ReedSolomon.evalOnPoints (subdomain ω i : Fin (2 ^ (n - i)) ↪ F) p) ∘ + sqFoldMapGen := by + ext u + simp only [ReedSolomon.evalOnPoints, Function.Embedding.coeFn_mk, LinearMap.coe_mk, + AddHom.coe_mk, Polynomial.eval_comp, Polynomial.eval_pow, Polynomial.eval_X, subdomain, inv_pow, + Function.comp_apply] + congr 1 + -- By definition of exponentiation in the field F, we can rewrite the right-hand side. + have h_exp : + ω u ^ (2 ^ i) = + (ω 0) ^ (2 ^ i - 1) * + ω (CosetFftDomainClass.subdomain_embed + i (Fin.mk + (u.val % 2 ^ (n - i)) + (Nat.mod_lt _ (Nat.two_pow_pos _)))) := by + have h_exp : + ∀ i : ℕ, ∀ u : Fin (2 ^ n), + ω u ^ 2 ^ i = ω 0 ^ (2 ^ i - 1) * + ω (Fin.mk + (2 ^ i * u.val % 2 ^ n) + (Nat.mod_lt _ (Nat.two_pow_pos _))) := by + intro i u + induction i generalizing u with + | zero => + simp_all only [pow_zero, pow_one, tsub_self, one_mul] + norm_num [Nat.mod_eq_of_lt] + | succ i ih => + simp_all only [pow_succ, pow_mul, pow_zero, one_mul] + have h_exp : + ω (Fin.mk + (2 ^ i * u.val % 2 ^ n) + (Nat.mod_lt _ (Nat.two_pow_pos _))) ^ 2 = + ω 0 * + ω (Fin.mk + (2 ^ (i + 1) * u.val % 2 ^ n) + (Nat.mod_lt _ (Nat.two_pow_pos _))) := by + have h_exp : ∀ u v : Fin (2 ^ n), ω u * ω v = ω 0 * ω (u + v) := by + intro u v + have := ‹CosetFftDomainClass D (Fin (2 ^ n)) F›.map_add ω u v + simp_all [mul_comm, mul_left_comm] + convert h_exp _ _ using 2 + · ring_nf + rw [sq] + · congr 1 + norm_num [Fin.add_def, Nat.mod_eq_of_lt] + ring_nf + convert congr_arg (· * (ω 0 ^ (2 ^ i - 1)) ^ 2) h_exp using 1 + <;> ring_nf + rw [show 2 ^ i * 2 - 1 = (2 ^ i - 1) * 2 + 1 by zify; norm_num; ring] + ring_nf + by_cases hi : i ≥ n + · simp_all only [ge_iff_le, CosetFftDomainClass.subdomain_embed, ↓reduceDIte, + mul_eq_mul_left_iff, pow_eq_zero_iff', ne_zero, ne_eq, false_and, or_false] + norm_num [Nat.mod_eq_zero_of_dvd (dvd_mul_of_dvd_left (pow_dvd_pow _ hi) _)] + · convert h_exp i u using 3 + simp only [CosetFftDomainClass.subdomain_embed, ge_iff_le] + split_ifs + · simp_all + · simp_all only [ge_iff_le, not_false_eq_true, Fin.mk.injEq] + rw [←Nat.mul_mod_mul_left, + ←pow_add, + Nat.add_sub_of_le (le_of_not_ge ‹¬n ≤ i›)] + convert h_exp using 1 + convert congr_arg + (fun x : Fˣ => x.val) + (show + ({ val := ω 0 ^ 2 ^ i, inv := (ω 0 ^ 2 ^ i) ⁻¹, val_inv := _, inv_val := _ } : Fˣ) * + ({ val := (ω 0) ⁻¹ * + ω (CosetFftDomainClass.subdomain_embed i ⟨u.val % 2 ^ (n - i), + Nat.mod_lt _ (Nat.two_pow_pos _)⟩), + inv := ω 0 * + (ω (CosetFftDomainClass.subdomain_embed i + ⟨u.val % 2 ^ (n - i), Nat.mod_lt _ (Nat.two_pow_pos _)⟩)) ⁻¹, + val_inv := _, + inv_val := _} : Fˣ) = + { val := ω 0 ^ (2 ^ i - 1) * + ω (CosetFftDomainClass.subdomain_embed i ⟨u.val % 2 ^ (n - i), + Nat.mod_lt _ (Nat.two_pow_pos _) ⟩), + inv := _, + val_inv := _, + inv_val := _} from ?_) using 1 + · exact (ω 0 ^ (2 ^ i - 1) * + ω (CosetFftDomainClass.subdomain_embed i ⟨u.val % 2 ^ ( n - i ), + Nat.mod_lt _ (Nat.two_pow_pos _)⟩))⁻¹ + all_goals norm_num [Units.ext_iff] + · field_simp + · field_simp + · cases k : 2 ^ i <;> simp_all [pow_succ, mul_assoc] + +/-- A particularly useful special case of `evalOnPoints_pow_of_two_eq_evalOnPoints_subdomain` + when `i = 1`. -/ +lemma evalOnPoints_sq_eq_evalOnPoints_subdomain [NeZero n] {p : Polynomial F} : + ReedSolomon.evalOnPoints (ω : Fin (2 ^ n) ↪ F) (p.comp (Polynomial.X ^ 2)) = + (ReedSolomon.evalOnPoints (subdomain ω 1 : Fin (2 ^ (n - 1)) ↪ F) p) ∘ + sqFoldMapGen := by + rw [show Polynomial.X ^ 2 = Polynomial.X ^ (2 ^ 1) by rfl, + evalOnPoints_pow_of_two_eq_evalOnPoints_subdomain] + +/-- Powers of domain values in terms of subdomain values. -/ +lemma subdomain_sqFoldMapGen_eq_pow_domain [NeZero n] {i : ℕ} {j : Fin (2 ^ n)} : + subdomain ω i (sqFoldMapGen j) = ω j ^ 2 ^ i := by + have := @evalOnPoints_pow_of_two_eq_evalOnPoints_subdomain + specialize @this F _ n D _ _ ω _ (Polynomial.X) i + simp_all [funext_iff, ReedSolomon.evalOnPoints] + +/-- `sqFoldMapGen j` equals `sqFoldMapGen j'` + if `ω j ^ 2 ^ j` equals `ω j ^ 2 ^ j'`. -/ +lemma sqFoldMapGen_eq_sqFoldMapGen_of_pow_apply_eq_pow_apply + [NeZero n] {i : ℕ} {j j' : Fin (2 ^ n)} + (h : ω j ^ 2 ^ i = ω j' ^ 2 ^ i) : + sqFoldMapGen (i := i) j = sqFoldMapGen j' := by + contrapose! h with h_contra + have h_key_id : + ∀ i u, ω u ^ 2 ^ i = + ω 0 ^ (2 ^ i - 1) * + ω (Fin.mk (2 ^ i * u.val % 2 ^ n) (Nat.mod_lt _ (Nat.two_pow_pos _))) := by + intro i u + induction i generalizing u with + | zero => + simp_all only [ne_eq, pow_zero, pow_one, tsub_self, one_mul] + norm_num [Nat.mod_eq_of_lt] + | succ i ih => + simp_all only [ne_eq, pow_succ, pow_mul, pow_zero, one_mul] + have h_sq : + ∀ u : Fin (2 ^ n), ω u ^ 2 = + ω 0 * ω (Fin.mk (2 * u.val % 2 ^ n) (Nat.mod_lt _ (Nat.two_pow_pos _))) := by + intro u + have := ‹CosetFftDomainClass D (Fin ( 2 ^ n )) F›.map_add ω u u + simp_all only [mul_assoc, sq] + simp_all only [Fin.add_def, two_mul, ne_eq, ne_zero, not_false_eq_true, + mul_inv_cancel_left₀] + convert congr_arg (· ^ 2) (ih u) using 1 <;> ring_nf + · convert congr_arg (· ^ 2) (ih u) |> Eq.symm using 1 + · ring_nf + · norm_num [pow_mul] + · rw [h_sq] + ring_nf + rw [show (2 ^ i * 2 - 1 : ℕ) = (2 ^ i - 1) * 2 + 1 + by zify; norm_num; ring] + ring_nf + norm_num [mul_assoc, Nat.mul_mod_mul_right] + have h_cancel : + ω (Fin.mk + (2 ^ i * j.val % 2 ^ n) + (Nat.mod_lt _ (Nat.two_pow_pos _))) ≠ + ω (Fin.mk + (2 ^ i * j'.val % 2 ^ n) + (Nat.mod_lt _ (Nat.two_pow_pos _))) := by + intro h_eq + have := (‹CosetFftDomainClass D (Fin (2 ^ n)) F›.injective ω) h_eq + simp_all only [ne_eq, Fin.ext_iff] + -- Since $2^i * j \equiv 2^i * j' \pmod{2^n}$, + -- we can divide both sides by $2^i$ (which is valid since $2^i$ is coprime to $2^n$). + have h_div : j.val % 2 ^ (n - i) = j'.val % 2 ^ (n - i) := by + by_cases hi : i ≤ n; + · have h_div : 2 ^ i * (j.val - j'.val) ≡ 0 [ZMOD 2 ^ n] := by + exact Int.modEq_zero_iff_dvd.mpr + ⟨2 ^ i * j / 2 ^ n - 2 ^ i * j' / 2 ^ n, + by linarith + [Int.emod_add_mul_ediv (2 ^ i * j) (2 ^ n), + Int.emod_add_mul_ediv (2 ^ i * j') (2 ^ n)]⟩ + have h_div : (j.val - j'.val : ℤ) ≡ 0 [ZMOD 2 ^ (n - i)] := by + rw [Int.modEq_zero_iff_dvd] at * + exact Exists.elim h_div fun k hk ↦ + ⟨k, by + rw [show ( 2 ^ n : ℤ ) = 2 ^ i * 2 ^ (n - i) by + rw [←pow_add, Nat.add_sub_of_le hi]] at hk; + nlinarith [pow_pos (zero_lt_two' ℤ) i]⟩ + exact Nat.ModEq.symm + (Nat.modEq_of_dvd <| by simpa [←Int.natCast_dvd_natCast] using h_div.symm.dvd) + · grind + exact h_contra h_div + simp_all [mul_comm] + +private lemma subdomain_embed_comp {k : ℕ} (hk : k + 1 ≤ n) + (a : Fin (2 ^ (n - k - 1))) + (i : Fin (2 ^ (n - (k + 1)))) (hai : (a : ℕ) = (i : ℕ)) : + CosetFftDomainClass.subdomain_embed (n := n) k + (CosetFftDomainClass.subdomain_embed (n := n - k) 1 a) = + CosetFftDomainClass.subdomain_embed (n := n) (k + 1) i := by + ext + by_cases hk1 : k + 1 = n + · have hnk : n - k = 1 := by omega + simp only [CosetFftDomainClass.subdomain_embed, hnk, ge_iff_le, + show ¬n ≤ k by omega, show n ≤ k + 1 by omega, le_refl, + ↓reduceDIte, Fin.val_zero, mul_zero] + · have hk1' : k + 1 < n := by omega + simp only [CosetFftDomainClass.subdomain_embed, ge_iff_le, + show ¬n ≤ k by omega, show ¬n ≤ k + 1 by omega, show ¬n - k ≤ 1 by omega, + ↓reduceDIte, Fin.val_mk, pow_one] + rw [hai, pow_succ] + ring + +private lemma subdomain_eval (ω : D) (j : ℕ) + (b : Fin (2 ^ (n - j))) : + (subdomain ω j) b = + ω 0 ^ 2 ^ j * ((ω 0)⁻¹ * ω (CosetFftDomainClass.subdomain_embed j b)) := rfl + +/-- Composing the `k`th subdomain with one more folding step gives the `(k+1)`th subdomain + (pointwise, under the index identification `n - k - 1 = n - (k + 1)`). -/ +lemma subdomain_one_comp + {k : ℕ} (hk : k + 1 ≤ n) + (a : Fin (2 ^ (n - k - 1))) (i : Fin (2 ^ (n - (k + 1)))) (hai : (a : ℕ) = (i : ℕ)) : + subdomain (subdomain ω k) 1 a = subdomain ω (k + 1) i := by + have hw0 : (subdomain ω k) 0 = ω 0 ^ 2 ^ k := by + rw [subdomain_eval ω k 0, CosetFftDomainClass.subdomain_embed_zero, + inv_mul_cancel₀ (CosetFftDomainClass.ne_zero ω 0), mul_one] + have hwe : (subdomain ω k) (CosetFftDomainClass.subdomain_embed 1 a) + = ω 0 ^ 2 ^ k + * ((ω 0)⁻¹ * ω (CosetFftDomainClass.subdomain_embed (k + 1) i)) := by + rw [subdomain_eval ω k (CosetFftDomainClass.subdomain_embed 1 a), + subdomain_embed_comp hk a i hai] + rw [subdomain_eval (subdomain ω k) 1 a, hw0, hwe, subdomain_eval ω (k + 1) i] + have hg0 : ω 0 ≠ 0 := CosetFftDomainClass.ne_zero ω 0 + have hgk : ω 0 ^ 2 ^ k ≠ 0 := pow_ne_zero _ hg0 + rw [show (ω 0 ^ 2 ^ k) ^ 2 ^ 1 = ω 0 ^ 2 ^ (k + 1) from by + rw [←pow_mul, pow_one, ←pow_succ]] + field_simp + end CosetFftDomainClass namespace CosetFftDomain @@ -460,6 +689,22 @@ variable [DecidableEq F] abbrev subdomain {n : ℕ} (ω : SmoothCosetFftDomain n F) (i : ℕ) : SmoothCosetFftDomain (n - i) F := CosetFftDomainClass.subdomain ω i +omit [DecidableEq F] in +/-- The zeroth subdomain of a `SmoothCosetFftDomain` + is itself on the nose. -/ +@[simp] +lemma subdomain_zero_eq_self {n : ℕ} {ω : SmoothCosetFftDomain n F} : + ω.subdomain 0 = ω := by + aesop + (add simp + [subdomain, + CosetFftDomainClass.subdomain, + CosetFftDomainClass.mkSubgroupUnit, + CosetFftDomainClass.subdomain_embed]) + (add safe cases Fin) + (add safe (by grind)) + (add unsafe (by rw [eval_coset_fft_domain_eq_eval_generator_mul_domain])) + /-- Search through a smooth coset FFT domain for an element whose `2 ^ i`th power is `x`, using `fuel` as the remaining search bound. -/ def twoNthRootAux (n i : ℕ) (ω : SmoothCosetFftDomain n F) (x : F) (fuel : ℕ) : ω := diff --git a/ArkLib/Data/MvPolynomial/EvenAndOdd.lean b/ArkLib/Data/MvPolynomial/EvenAndOdd.lean new file mode 100644 index 0000000000..13b262e637 --- /dev/null +++ b/ArkLib/Data/MvPolynomial/EvenAndOdd.lean @@ -0,0 +1,376 @@ +/- +Copyright (c) 2024-2026 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: František Silváši, Ilia Vlasov, Aristotle (Harmonic) +-/ + +import Mathlib.Algebra.MvPolynomial.Monad +import Mathlib.Tactic.IntervalCases +import Mathlib.Algebra.CharP.Basic + +import CompPoly.Data.MvPolynomial.Notation +import ArkLib.Data.MvPolynomial.LinearMvExtension + +namespace MvPolynomial + +open BigOperators Fintype Finset + +variable {R : Type} [Field R] +variable {n : ℕ} [NeZero n] +variable {p : MvPolynomial (Fin n) R} + +private noncomputable def substPlus (p : MvPolynomial (Fin n) R) : + MvPolynomial (Fin n) R := + p.aeval (fun i ↦ if i = 0 then 1 else (MvPolynomial.X i : MvPolynomial (Fin n) R)) + +private noncomputable def substMinus (p : MvPolynomial (Fin n) R) : + MvPolynomial (Fin n) R := + p.aeval (fun i ↦ if i = 0 then -1 else MvPolynomial.X i) + +private lemma substPlus_mem_restrictDegree + (hp : p ∈ restrictDegree (Fin n) R 1) : + substPlus p ∈ restrictDegree (Fin n) R 1 := by + have h_support : ∀ m ∈ p.support, ∀ i, m i ≤ 1 := by + rwa [mem_restrictDegree] at hp + unfold substPlus + have h_monomial : ∀ m ∈ p.support, + (MvPolynomial.monomial m (p.coeff m)).aeval + (fun i ↦ if i = 0 then 1 else (MvPolynomial.X i : MvPolynomial (Fin n) R)) ∈ + restrictDegree (Fin n) R 1 := by + intro m hm + have h_monomial : + (MvPolynomial.monomial m (p.coeff m)).aeval (fun i ↦ + if i = 0 then 1 else (MvPolynomial.X i : MvPolynomial (Fin n) R)) = + MvPolynomial.monomial (m.erase 0) (p.coeff m) := by + simp [MvPolynomial.monomial_eq, Finset.prod_ite, Finset.filter_ne', Finsupp.erase] + rw [mem_restrictDegree] + intro s hs i + by_cases hi : i = 0 <;> aesop + rw [MvPolynomial.as_sum p] + convert Submodule.sum_mem _ h_monomial using 1 + rw [map_sum] + +private lemma substMinus_mem_restrictDegree + (hp : p ∈ restrictDegree (Fin n) R 1) : + substMinus p ∈ restrictDegree (Fin n) R 1 := by + have := substPlus_mem_restrictDegree hp + unfold substPlus substMinus at * + have h_subst : + ∀ i : Fin n, + (MvPolynomial.degreeOf i + (MvPolynomial.bind₁ (fun i ↦ if i = 0 then -1 else X i) p)) ≤ 1 := by + intro i + have h_subst : ∀ m ∈ p.support, + (MvPolynomial.degreeOf i + (MvPolynomial.bind₁ + (fun i ↦ if i = 0 then -1 else X i) (MvPolynomial.monomial m (p.coeff m)))) ≤ 1 := by + intro m hm + have h_deg : ∀ i, m i ≤ 1 := by aesop + simp_all only [aeval_eq_bind₁, mem_support_iff, ne_eq, bind₁_monomial, ite_pow, + ge_iff_le] + apply le_trans (MvPolynomial.degreeOf_mul_le _ _ _) _ + simp_all only [degreeOf_C, zero_add] + apply le_trans (MvPolynomial.degreeOf_prod_le _ _ _) _ + rw [Finset.sum_eq_add_sum_diff_singleton i _ (by aesop)] + rw [Finset.sum_equiv + (t := m.support \ {i}) + (Equiv.refl _) + (by simp) + (g := fun x ↦ 0) + (fun j hj ↦ by + split_ifs with hjeq0 + · have : m 0 = 1 := by grind + aesop + · have : i ≠ j := by aesop + exact Nat.eq_zero_of_le_zero <| + le_trans (MvPolynomial.degreeOf_pow_le _ _ _) <| by + simp [MvPolynomial.degreeOf_X, this])] + split_ifs + · by_cases hm0 : m 0 = 0 + · aesop + · have : m 0 = 1 := by grind + aesop + · simp only [sum_const_zero, add_zero] + apply le_trans (MvPolynomial.degreeOf_pow_le _ _ _) + simp [MvPolynomial.degreeOf, h_deg] + rw [MvPolynomial.as_sum p, map_sum] + exact le_trans + (MvPolynomial.degreeOf_sum_le _ _ _) + (Finset.sup_le fun m hm => h_subst m hm) + aesop + (add simp [MvPolynomial.degreeOf_eq_sup, mem_restrictDegree, mem_support_iff]) + +omit [NeZero n] in +private lemma mul_C_mem_restrictDegree + (hp : p ∈ restrictDegree (Fin n) R 1) + (c : R) : p * C c ∈ restrictDegree (Fin n) R 1 := by + convert Submodule.smul_mem _ c hp using 1 + rw [mul_comm, MvPolynomial.C_mul'] + +private lemma even_mem (p : R⦃≤ 1⦄[X (Fin n)]) : + (substPlus p.1 + substMinus p.1) * C (2⁻¹) ∈ restrictDegree (Fin n) R 1 := + mul_C_mem_restrictDegree ((restrictDegree (Fin n) R 1).add_mem + (substPlus_mem_restrictDegree p.2) (substMinus_mem_restrictDegree p.2)) _ + +private lemma odd_mem (p : R⦃≤ 1⦄[X (Fin n)]) : + (substPlus p.1 - substMinus p.1) * C (2⁻¹) ∈ restrictDegree (Fin n) R 1 := + mul_C_mem_restrictDegree ((restrictDegree (Fin n) R 1).sub_mem + (substPlus_mem_restrictDegree p.2) (substMinus_mem_restrictDegree p.2)) _ + +noncomputable def even (p : R⦃≤ 1⦄[X (Fin n)]) : + R⦃≤ 1⦄[X (Fin n)] := + ⟨(substPlus p.1 + substMinus p.1) * C (2⁻¹), even_mem p⟩ + +noncomputable def odd (p : R⦃≤ 1⦄[X (Fin n)]) : + R⦃≤ 1⦄[X (Fin n)] := + ⟨(substPlus p.1 - substMinus p.1) * C (2⁻¹), odd_mem p⟩ + +private lemma formula_for_monomial + (h2ne0 : (2 : R) ≠ 0) + (m : Fin n →₀ ℕ) (c : R) (hm : ∀ i, m i ≤ 1) : + (substPlus (monomial m c) + substMinus (monomial m c)) * C (2⁻¹) + + X 0 * ((substPlus (monomial m c) - substMinus (monomial m c)) * C (2⁻¹)) = monomial m c := by + by_cases h0 : m 0 = 0 + · have h_subst : + substPlus (MvPolynomial.monomial m c) = + MvPolynomial.monomial m c ∧ + substMinus (MvPolynomial.monomial m c) = MvPolynomial.monomial m c := by + simp [substPlus, substMinus, MvPolynomial.bind₁_monomial] + simp [MvPolynomial.monomial_eq, Finset.prod_ite, Finset.filter_ne', Finset.filter_eq', h0] + simp only [h_subst, sub_self, zero_mul, mul_zero, add_zero] + rw [←two_smul R, smul_mul_assoc, ←MvPolynomial.C_mul'] + ring_nf + rw [mul_right_comm, ←MvPolynomial.C_mul, mul_inv_cancel₀ h2ne0, MvPolynomial.C_1, one_mul] + · have h_monomial : monomial m c = C c * X 0 * ∏ i ∈ m.support \ {0}, X i ^ (m i) := by + rw [MvPolynomial.monomial_eq] + simp only [Finsupp.prod, prod_X_pow_eq_monomial, mul_assoc, mul_eq_mul_left_iff, map_eq_zero] + have hsup : 0 ∈ m.support := by simp [h0] + have : (X 0 : R[X (Fin n)]) = X 0 ^ (m 0) := by simp [show m 0 = 1 by grind] + rw [this, + ←Finset.prod_eq_mul_prod_diff_singleton (s := m.support) 0 + (f := fun i ↦ X i ^ m i) (by aesop)] + aesop + aesop + (add simp [ + substPlus, substMinus, + Finset.prod_ite, Finset.filter_ne', Finset.filter_eq', + mul_assoc, inv_mul_cancel₀]) + (add unsafe [(by ring_nf), (by erw [←map_mul])]) + +private lemma formula_generic + (h2ne0 : (2 : R) ≠ 0) + (p : MvPolynomial (Fin n) R) (hp : p ∈ restrictDegree (Fin n) R 1) : + (substPlus p + substMinus p) * C (2⁻¹) + + X 0 * ((substPlus p - substMinus p) * C (2⁻¹)) = p := by + have h_expand : + ∀ m ∈ p.support, + (substPlus (monomial m (p.coeff m)) + + substMinus (monomial m (p.coeff m))) * C (2⁻¹) + + X 0 * ((substPlus (monomial m (p.coeff m)) - + substMinus (monomial m (p.coeff m))) * C (2⁻¹)) = monomial m (p.coeff m) := + by aesop + (add unsafe [formula_for_monomial]) + (add simp [mem_restrictDegree]) + rw [MvPolynomial.as_sum p] + convert Finset.sum_congr rfl h_expand using 1 + simp only [substPlus, aeval_eq_bind₁, support_sum_monomial_coeff, substMinus, mul_comm, mul_add, + sum_add_distrib] + conv_lhs => rw [MvPolynomial.as_sum p] + simp only [map_sum] + simp [mul_sub, Finset.mul_sum] + +lemma even_and_odd_formula + (hchar : ¬CharP R 2) + {p : R⦃≤ 1⦄[X (Fin n)]} : + (even p).1 + (MvPolynomial.X 0) * (odd p).1 = p.1 := formula_generic + (by aesop (add simp [CharP.charP_iff_prime_eq_zero, Nat.prime_two])) p.1 p.2 + +private noncomputable def shiftDown (q : MvPolynomial (Fin n) R) : MvPolynomial (Fin (n - 1)) R := + q.aeval (fun i ↦ if h : i = (0 : Fin n) then 0 else X ⟨i.val - 1, by omega⟩) + +private lemma shiftDown_shiftUp_eq (q : MvPolynomial (Fin n) R) : + (shiftDown q).aeval + (fun i : Fin (n - 1) ↦ (X (⟨i.val + 1, by omega⟩ : Fin n) : MvPolynomial (Fin n) R)) = + q.aeval (fun i ↦ if h : i = (0 : Fin n) then 0 else X i) := by + unfold MvPolynomial.shiftDown + grind +suggestions + +private lemma substNoX0_eq_self_of_even + (p : restrictDegree (Fin n) R 1) : + (even p).1.aeval + (fun i : Fin n ↦ + if _ : i = (0 : Fin n) then (0 : MvPolynomial (Fin n) R) else X i) = (even p).1 := by + unfold even + simp only [aeval_eq_bind₁, substPlus, substMinus, map_mul, map_add, algHom_C, algebraMap_eq, + mul_eq_mul_right_iff, map_eq_zero, inv_eq_zero] + left + congr! 1 + all_goals induction p.val using MvPolynomial.induction_on <;> aesop + +private lemma substNoX0_eq_self_of_odd + (p : restrictDegree (Fin n) R 1) : + (odd p).1.aeval + (fun i : Fin n ↦ + if _ : i = (0 : Fin n) then (0 : MvPolynomial (Fin n) R) else X i) = (odd p).1 := by + unfold odd + unfold MvPolynomial.substPlus MvPolynomial.substMinus + simp only [aeval_eq_bind₁, sub_mul, map_sub, map_mul, algHom_C, algebraMap_eq] + congr! 2 + all_goals induction p.val using MvPolynomial.induction_on <;> aesop + +-- For the case m 0 ≠ 0: the product contains a zero factor +private lemma aeval_shift_monomial_zero_case {n : ℕ} [NeZero n] + (m : Fin n →₀ ℕ) (c : R) (hm : ∀ i, m i ≤ 1) (h0 : m 0 ≠ 0) : + (monomial m c).aeval (fun i : Fin n ↦ if h : i = (0 : Fin n) + then (0 : MvPolynomial (Fin (n - 1)) R) + else X ⟨i.val - 1, by omega⟩) = 0 := by + change bind₁ _ (monomial m c) = 0 + rw [bind₁_monomial] + have h01 : m 0 = 1 := Nat.le_antisymm (hm 0) (Nat.pos_of_ne_zero h0) + have h0s : (0 : Fin n) ∈ m.support := by simp [Finsupp.mem_support_iff, h0] + apply mul_eq_zero_of_right + apply Finset.prod_eq_zero h0s + simp [h01] + +/- +For the case m 0 = 0: the result is a shifted monomial +-/ +private lemma aeval_shift_monomial_nonzero_case + (m : Fin n →₀ ℕ) (c : R) (hm : ∀ i, m i ≤ 1) (h0 : m 0 = 0) : + (monomial m c).aeval (fun i : Fin n ↦ if h : i = (0 : Fin n) + then (0 : MvPolynomial (Fin (n - 1)) R) + else X ⟨i.val - 1, by omega⟩) ∈ restrictDegree (Fin (n - 1)) R 1 := by + rw [MvPolynomial.mem_restrictDegree] + intro s hs i + contrapose! hs + simp_all only [aeval_eq_bind₁, monomial_eq, Finsupp.prod_pow, map_mul, algHom_C, algebraMap_eq, + map_prod, map_pow, bind₁_X_right, dite_pow, pow_zero, mem_support_iff, coeff_C_mul, ne_eq, + mul_eq_zero, not_or, not_and, not_not] + have h_coeff : + coeff s (∏ x : Fin n, + if h : x = 0 + then 1 + else (MvPolynomial.X ⟨↑x - 1, by omega⟩ : MvPolynomial (Fin (n - 1)) R) ^ m x) = 0 := by + have h_coeff : + ∀ (t : Fin n → ℕ), + (∏ x : Fin n, + if h : x = 0 + then 1 + else (MvPolynomial.X ⟨↑x - 1, by omega⟩ : MvPolynomial (Fin (n - 1)) R) ^ t x) = + MvPolynomial.monomial + (∑ x : Fin n, if h : x = 0 then 0 else Finsupp.single ⟨↑x - 1, by omega⟩ (t x)) 1 := + by + intro t + induction (Finset.univ : Finset (Fin n)) using Finset.induction + <;> aesop + (add simp [Finset.prod_insert, MvPolynomial.monomial_mul, + MvPolynomial.X_pow_eq_monomial]) + simp_all only [coeff_monomial, ite_eq_right_iff, one_ne_zero, imp_false, ne_eq] + intro h + replace h := congr_arg (fun f ↦ f i) h + simp_all only [sum_apply'] + rw + [Finset.sum_eq_single ⟨i + 1, by grind⟩] at h + <;> aesop (add safe (by grind)) + exact fun _ => h_coeff + +lemma aeval_shift_monomial_mem {n : ℕ} [NeZero n] + (m : Fin n →₀ ℕ) (c : R) (hm : ∀ i, m i ≤ 1) : + (monomial m c).aeval (fun i : Fin n ↦ if h : i = (0 : Fin n) + then (0 : MvPolynomial (Fin (n - 1)) R) + else X ⟨i.val - 1, by omega⟩) ∈ restrictDegree (Fin (n - 1)) R 1 := by + by_cases h0 : m 0 = 0 + · exact aeval_shift_monomial_nonzero_case m c hm h0 + · rw [aeval_shift_monomial_zero_case m c hm h0]; exact zero_mem _ + +lemma aeval_shift_mem_restrictDegree + (q : MvPolynomial (Fin n) R) (hq : q ∈ restrictDegree (Fin n) R 1) : + q.aeval (fun i ↦ if h : i = (0 : Fin n) then (0 : MvPolynomial (Fin (n - 1)) R) + else X ⟨i.val - 1, by omega⟩) ∈ restrictDegree (Fin (n - 1)) R 1 := by + rw [MvPolynomial.as_sum q, map_sum] + apply Submodule.sum_mem + intro m hm + exact aeval_shift_monomial_mem m (q.coeff m) (fun i => (mem_restrictDegree _ q 1).mp hq m hm i) + +noncomputable def even_pred (p : R⦃≤ 1⦄[X (Fin n)]) : R⦃≤ 1⦄[X (Fin (n - 1))] := + ⟨(even p).1.aeval + (fun i ↦ if h : i = 0 then 0 else X (σ := Fin (n - 1)) ⟨i.val - 1, by omega⟩), + by exact aeval_shift_mem_restrictDegree (even p).1 (even p).2 + ⟩ + +noncomputable def odd_pred (p : R⦃≤ 1⦄[X (Fin n)]) : R⦃≤ 1⦄[X (Fin (n - 1))] := + ⟨(odd p).1.aeval + (fun i ↦ if h : i = 0 then 0 else X (σ := Fin (n - 1)) ⟨i.val - 1, by omega⟩), + by exact aeval_shift_mem_restrictDegree (odd p).1 (odd p).2⟩ + +lemma even_and_odd_formula' + (hchar : ¬CharP R 2) + {p : R⦃≤ 1⦄[X (Fin n)]} : + (even_pred p).1.aeval + (fun i ↦ X (⟨i.val + 1, by omega⟩ : Fin n)) + + (MvPolynomial.X 0) * (odd_pred p).1.aeval + (fun i ↦ X (⟨i.val + 1, by omega⟩ : Fin n)) = p.1 := by + change + (shiftDown (even p).1).aeval _ + X 0 * (shiftDown (odd p).1).aeval _ = p.1 + rw [shiftDown_shiftUp_eq, shiftDown_shiftUp_eq] + rw [substNoX0_eq_self_of_even, substNoX0_eq_self_of_odd] + exact even_and_odd_formula hchar + +lemma even_and_odd_eval + (hchar : ¬CharP R 2) + {p : R⦃≤ 1⦄[X (Fin n)]} + {α : R} : + p.1.aeval + (fun i ↦ if h : i = 0 then C α else (X ⟨i.val - 1, by omega⟩ : R[X (Fin (n - 1))])) = + (even_pred p).1 + C α * (odd_pred p).1 := by + conv_lhs => rw [←even_and_odd_formula' hchar] + aesop + (add safe [(by erw [MvPolynomial.aeval_bind₁])]) + +noncomputable def shiftedPowAlgHom : + MvPolynomial (Fin (n - 1)) R →ₐ[R] Polynomial R := + MvPolynomial.aeval fun j : Fin (n - 1) => Polynomial.X ^ (2 ^ (j.val + 1)) + +omit [NeZero n] in +open LinearMvExtension in +lemma shiftedPowAlgHom_eq_powAlgHom_comp_sq_x + {p : MvPolynomial (Fin (n - 1)) R} : + shiftedPowAlgHom p = (powAlgHom p).comp (Polynomial.X ^ 2) := by + induction p using MvPolynomial.induction_on + <;> aesop + (add simp [shiftedPowAlgHom, powAlgHom]) + (add unsafe (by ring_nf)) + +omit [NeZero n] in +open LinearMvExtension in +private lemma powAlgHom_aeval_shift (q : MvPolynomial (Fin (n - 1)) R) : + powAlgHom (q.aeval (fun i : Fin (n - 1) ↦ + (X (⟨i.val + 1, by omega⟩ : Fin n) : MvPolynomial (Fin n) R))) = + shiftedPowAlgHom q := by + induction q using MvPolynomial.induction_on + <;> aesop (add simp [powAlgHom, shiftedPowAlgHom]) + +open LinearMvExtension in +lemma powAlgHom_eq_even_add_odd + (hchar : ¬CharP R 2) + {p : R⦃≤ 1⦄[X (Fin n)]} : + powAlgHom p.1 = + shiftedPowAlgHom (even_pred p).1 + + Polynomial.X * shiftedPowAlgHom (odd_pred p).1 := by + conv_lhs => rw [←even_and_odd_formula' hchar] + aesop + (erase aeval_eq_bind₁) + (add simp [powAlgHom_aeval_shift, powAlgHom_aeval_shift]) + (add unsafe (by rw [powAlgHom])) + +open LinearMvExtension in +lemma powAlgHom_eq_even_add_odd_powAlgHom + (hchar : ¬CharP R 2) + {p : R⦃≤ 1⦄[X (Fin n)]} : + powAlgHom p.1 = + (powAlgHom (even_pred p).1).comp (Polynomial.X ^ 2) + + Polynomial.X * (powAlgHom (odd_pred p).1).comp (Polynomial.X ^ 2) := by + conv_lhs => rw [powAlgHom_eq_even_add_odd hchar] + simp [shiftedPowAlgHom_eq_powAlgHom_comp_sq_x] + +end MvPolynomial