feat(Interpolation): prove eq_of_degreeOf_lt_card_of_eval_eq, schwartz_zippel

[pitmonticone]

This PR adds proofs autoformalised by @Aristotle-Harmonic.

Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

[github-actions]

🤖 Gemini PR Summary

This Pull Request significantly expands the library’s mathematical foundations, coding theory implementations, and proof system frameworks. The primary highlight is the formalization of key algebraic lemmas (Schwartz-Zippel) and the introduction of various data structures designed for computational efficiency and definitional equality in Lean.

Features

• Mathematical Formalization:
  • Proves the Schwartz-Zippel lemma and multivariable polynomial identity theorems, replacing previous placeholders.
  • Introduces definitions for even and odd polynomial parts, supporting FFT-style operations and evaluations.
• Coding Theory & Cryptography:
  • Implements Reed-Muller codes and provides foundations for Tensor-based polynomial commitment schemes.
  • Introduces the Trivial commitment scheme where the prover sends raw data.
  • Adds an experimental Domain-Specific Language (DSL) for specifying Information-Theoretic Oracle Relations (IORs) over finite fields.
• Data Structures & Church Encodings:
  • Implements Church encodings for natural numbers, booleans, and vectors.
  • Introduces AssocNat and CNat hierarchies, providing representations of natural numbers where addition is definitionally associative.
  • Adds a heterogeneous list type (HList) as a list of sigma types with associated notations.
• Algebraic Typeclasses:
  • Defines new typeclasses for successor/predecessor operations (HasSucc, HasPred) and natural number conversion (ToNat), including "Lawful" variants to ensure algebraic consistency.
• Proof Systems:
  • Establishes entry points and module structures for the STIR and WHIR proof systems.

Fixes

• Proof Completion: Successfully replaces sorry stubs in ArkLib/Data/MvPolynomial/Interpolation.lean with complete formal proofs.
• CI Stability: Updates the GitHub Actions workflows to utilize lean-action caching and temporarily disables the linter to bypass existing errors and stabilize the CI pipeline.

Refactoring

• Module Organization: Consolidates multiple submodules into central entry points for ArkLib.lean and ArkLib.Data.CodingTheory to improve library discoverability.
• List & Vector Utilities:
  • Refactors list searching with findIdx' and idxOf' for better definitional properties.
  • Adds utility functions for interleaving vectors and grouping elements into pairs.
  • Provides theorems for partial sums and products in List.BigOperators.
• Integer Equivalences: Defines logical equivalences between Fin (2 ^ n) and standard fixed-precision types (e.g., UInt64, BitVec) to facilitate easier casting and reasoning.

Documentation

• Workflow Enhancements: Updated docs.yml to use standardized cache keys and integrated GitHub caching for Lean-specific documentation builds.
• Code Documentation: New modules such as ReedMuller.lean include updated documentation for error-correcting code families.

---

Analysis of Changes

Metric	Count
📝 Files Changed	24
✅ Lines Added	2299
❌ Lines Removed	3

---

Lean Declarations

❌ **Added:** 201 declaration(s)

• lemma evenPart_x_eval_eq {f : Polynomial F} {s : F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• def partialProd {α : Type*} [Monoid α] (l : List α) : List α in ArkLib/Data/List/BigOperators.lean
• theorem zero_mul {a : AssocNat} : 0 * a = 0 in ArkLib/Data/CNat/AssocNat.lean
• def ChurchNat (α : Type) : Type in ArkLib/Data/CNat/Church.lean
• def mul (a b : AssocNat) : AssocNat in ArkLib/Data/CNat/AssocNat.lean
• -- def CNat₂ : Type in ArkLib/Data/CNat/Church.lean
• def leq {α : Type} (m n : ChurchNat α) : ChurchBool α in ArkLib/Data/CNat/Church.lean
• theorem mul_one {a : CNat 50} : a * 1 = a in ArkLib/Data/CNat/Defs.lean
• def findFinIdx (p : α → Bool) (l : List α) : Fin (l.length + 1) in ArkLib/Data/List/Find.lean
• instance [ToString α] (αs : List Type) [HListString (HList αs)] : in ArkLib/Data/List/HList.lean
• -- theorem toNat_eq_iff [LawfulToNat α] (a b : α) : ToNat.toNat a = ToNat.toNat b ↔ a = b in ArkLib/Data/Classes/ToNat.lean
• -- theorem ne_of_toNat_ne (a b : α) (h : ToNat.toNat a ≠ ToNat.toNat b) : a ≠ b in ArkLib/Data/Classes/ToNat.lean
• def mul (m n : ChurchNat α) : ChurchNat α in ArkLib/Data/CNat/Church.lean
• def ValidChurchNat : Type in ArkLib/Data/CNat/Church.lean
• instance [Repr α] (αs : List Type) [HListRepr (HList αs)] : HListRepr (HList (α :: αs)) where in ArkLib/Data/List/HList.lean
• def churchFalse : ChurchBool α in ArkLib/Data/CNat/Church.lean
• def churchNot (p : ChurchBool α) : ChurchBool α in ArkLib/Data/CNat/Church.lean
• theorem one_mul (n : ChurchNat α) : mul one n = n in ArkLib/Data/CNat/Church.lean
• def isZero {α : Type} (n : ChurchNat α) : ChurchBool α in ArkLib/Data/CNat/Church.lean
• lemma evenize_is_even {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• theorem mul_succ (m n : ChurchNat α) : mul n (succ m) = add n (mul n m) in ArkLib/Data/CNat/Church.lean
• def finUInt32Equiv : Fin (2 ^ 32) ≃ UInt32 where in ArkLib/ToMathlib/UInt/Equiv.lean
• -- theorem DVec.toHList_getTypes (l : DVec (m in ArkLib/Data/List/HList.lean
• def somePairs : HList' (fun x => x × x) someTypes in ArkLib/Data/List/HList.lean
• -- def join {αs : List (Type u)} {βs : αs → List (Type v)} : HList (List (HList βs)) → HList αs in ArkLib/Data/List/HList.lean
• lemma HList.toDVec_eq_getValue (l : HList) (i : Fin l.length) : l.toDVec i = l.getValue i in ArkLib/Data/List/HList.lean
• def churchOr (p q : ChurchBool α) : ChurchBool α in ArkLib/Data/CNat/Church.lean
• lemma evenize_coeff {f : Polynomial F} {n : ℕ} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• instance instHasPred {n : ℕ} : HasPred (CNat n) in ArkLib/Data/CNat/Defs.lean
• theorem pow_one {a : CNat 50} : a ^ 1 = a in ArkLib/Data/CNat/Defs.lean
• theorem partialSum_length (l : List ℕ) : l.partialSum.length = l.length + 1 in ArkLib/Data/List/BigOperators.lean
• instance instNatPow {n : ℕ} : NatPow (CNat n) in ArkLib/Data/CNat/Defs.lean
• instance instAdd {n : ℕ} : Add (CNat n) in ArkLib/Data/CNat/Defs.lean
• def someValues : HList' (fun x => x) someTypes in ArkLib/Data/List/HList.lean
• def one : ChurchNat α in ArkLib/Data/CNat/Church.lean
• def churchCons (x : α) (xs : ChurchVec α) : ChurchVec α in ArkLib/Data/CNat/Church.lean
• abbrev CNat (n : ℕ) : Type in ArkLib/Data/CNat/Defs.lean
• def succ (n : ChurchNat α) : ChurchNat α in ArkLib/Data/CNat/Church.lean
• theorem toNat_ofNat (n : ℕ) : toNat (ofNat n) = n in ArkLib/Data/CNat/Church.lean
• def get (mls : HList' β ls) : member a ls → β a in ArkLib/Data/List/HList.lean
• theorem partialSum_succ {a : α} {l : List α} : in ArkLib/Data/List/BigOperators.lean
• lemma length_nil : nil.length = 0 in ArkLib/Data/List/HList.lean
• lemma getTypes_eq_get_fst (l : HList) (i : Fin l.length) : l.getTypes[i] = l[i].1 in ArkLib/Data/List/HList.lean
• theorem toNat_succ (n : ChurchNat ℕ) : toNat (succ n) = n.toNat.succ in ArkLib/Data/CNat/Church.lean
• theorem toFun_eq_const_plus (t : AssocNat) : ∀ m : Nat, t m = t 0 + m in ArkLib/Data/CNat/AssocNat.lean
• -- theorem mul_distrib_add {a b c : CNat 2} : a * (b + c) = a * b + a * c in ArkLib/Data/CNat/Defs.lean
• instance instOfNat {n : ℕ} : OfNat (CNat n) n in ArkLib/Data/CNat/Defs.lean
• def nil : HList in ArkLib/Data/List/HList.lean
• lemma f_eq_evenPart_plus_x_oddPart {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• theorem add_assoc (a b c : AssocNat) : (a + b) + c = a + (b + c) in ArkLib/Data/CNat/AssocNat.lean
• theorem ext' {a b : AssocNat} (h : a 0 = b 0) : a = b in ArkLib/Data/CNat/AssocNat.lean
• lemma getTypes_hcons (x : Σ α : Type u, α) (xs : HList) : in ArkLib/Data/List/HList.lean
• -- theorem mul_succ {a b : AssocNat} : a * (succ b) = a + a * b in ArkLib/Data/CNat/AssocNat.lean
• def pred (n : ChurchNat α) : ChurchNat α in ArkLib/Data/CNat/Church.lean
• lemma getTypes_cons (x : Σ α : Type u, α) (xs : HList) : in ArkLib/Data/List/HList.lean
• def EvenPoly (f : Polynomial F) : Prop in ArkLib/Data/Polynomial/EvenAndOdd.lean
• def churchTrue : ChurchBool α in ArkLib/Data/CNat/Church.lean
• theorem mul_add {a b c : AssocNat} : a * (b + c) = a * b + a * c in ArkLib/Data/CNat/AssocNat.lean
• def powNat [Zero T] [One T] [ToNat T] (a : Cayley T) : Nat → Cayley T in ArkLib/Data/CNat/Defs.lean
• lemma oddPart_coeff {f : Polynomial F} {n : ℕ} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• -- def CNat : Type in ArkLib/Data/CNat/Church.lean
• def finBitVecEquiv {n : ℕ} : Fin (2 ^ n) ≃ BitVec n where in ArkLib/ToMathlib/UInt/Equiv.lean
• lemma length_getTypes (l : HList) : l.getTypes.length = l.length in ArkLib/Data/List/HList.lean
• lemma evenize_eval {f : Polynomial F} {s : F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• def partialSum {α : Type*} [AddMonoid α] (l : List α) : List α in ArkLib/Data/List/BigOperators.lean
• def churchVecFold (xs : ChurchVec α) (f : α → List α → List α) (base : List α) : List α in ArkLib/Data/CNat/Church.lean
• theorem mul_zero (n : ChurchNat α) : mul n zero = zero in ArkLib/Data/CNat/Church.lean
• def getTypes {αs : List Type} (_ : HList αs) : List Type in ArkLib/Data/List/HList.lean
• def sub (a b : AssocNat) : AssocNat in ArkLib/Data/CNat/AssocNat.lean
• instance instOne {n : ℕ} : One (CNat n) in ArkLib/Data/CNat/Defs.lean
• theorem succ_eq_one_add (n : ChurchNat α) : succ n = add one n in ArkLib/Data/CNat/Church.lean
• instance instPow {n : ℕ} : Pow (CNat n) Nat in ArkLib/Data/CNat/Defs.lean
• theorem add_zero : @add α zero = @id (ChurchNat α) in ArkLib/Data/CNat/Church.lean
• def findSumIdxWith (l : List ℕ) (j : Fin l.sum) : (i : Fin l.length) × Fin (l.get i) in ArkLib/Data/List/BigOperators.lean
• theorem ranges_length_eq_self_length {l : List ℕ} : l.ranges.length = l.length in ArkLib/Data/List/BigOperators.lean
• lemma deevenize_comp_x_squared {f : Polynomial F} (hEven : EvenPoly f) : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• theorem ofNat_zero : ofNat 0 = @zero α in ArkLib/Data/CNat/Church.lean
• instance instToNat {n : ℕ} : ToNat (CNat n) in ArkLib/Data/CNat/Defs.lean
• -- instance instDiv {n : ℕ} : Div (CNat n) in ArkLib/Data/CNat/Defs.lean
• def example1 : ChurchVec ℕ in ArkLib/Data/CNat/Church.lean
• def DVec {m : Type v} (α : m → Type u) : Type (max u v) in ArkLib/Data/List/HList.lean
• lemma eq_evenize_deevenize {f : Polynomial F} (hEven : EvenPoly f) : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• -- theorem zero_mul (n : ChurchNat α) : mul zero n = zero in ArkLib/Data/CNat/Church.lean
• def cons (x : Σ α : Type u, α) (xs : HList) : HList in ArkLib/Data/List/HList.lean
• def finUInt64Equiv : Fin (2 ^ 64) ≃ UInt64 where in ArkLib/ToMathlib/UInt/Equiv.lean
• theorem ranges_succ {a : ℕ} {l : List ℕ} : in ArkLib/Data/List/BigOperators.lean
• lemma evenPart_def : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• theorem add_assoc {n : ℕ} (a b c : CNat (n + 1)) : (a + b) + c = a + (b + c) in ArkLib/Data/CNat/Defs.lean
• -- theorem mul_distrib_add_one {a b : CNat 2} : a * (b + 1) = a * b + a in ArkLib/Data/CNat/Defs.lean
• def toAssocNat (f : AssocFin n) : AssocNat in ArkLib/Data/CNat/AssocNat.lean
• def subNat (c : AssocNat) : Nat → AssocNat in ArkLib/Data/CNat/AssocNat.lean
• theorem ofNat_succ (n : ℕ) : @ofNat α (n.succ) = succ (ofNat n) in ArkLib/Data/CNat/Church.lean
• def chunkPairwise {α : Type} : {n : Nat} → Vector α (2 * n) → Vector (α × α) n in ArkLib/Data/List/Vector.lean
• def modNat [Zero T] [DecidableEq T] [ToNat T] in ArkLib/Data/CNat/Defs.lean
• -- theorem mul_distrib_add (m n p : ChurchNat α) : mul m (add n p) = add (mul m n) (mul m p) in ArkLib/Data/CNat/Church.lean
• -- def pairwise {α : Type} {n : Nat} (v : Vector α (2 * n)) : Vector (α × α) n in ArkLib/Data/List/Vector.lean
• theorem pow_zero {a : CNat 50} : a ^ 0 = 1 in ArkLib/Data/CNat/Defs.lean
• theorem findIdx'_eq_findIdx : @findIdx' = @findIdx in ArkLib/Data/List/Find.lean
• lemma cons_eq_List.cons : x ::ₕ xs = x :: xs in ArkLib/Data/List/HList.lean
• theorem add_comm (m n : ChurchNat α) : add m n = add n m in ArkLib/Data/CNat/Church.lean
• theorem sum_mem_partialSum (l : List ℕ) : l.sum ∈ l.partialSum in ArkLib/Data/List/BigOperators.lean
• lemma getTypes_nil : getTypes [] = [] in ArkLib/Data/List/HList.lean
• def three : ChurchNat α in ArkLib/Data/CNat/Church.lean
• lemma oddPart_def : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• instance instHasSucc {n : ℕ} : HasSucc (CNat n) in ArkLib/Data/CNat/Defs.lean
• def finUInt16Equiv : Fin (2 ^ 16) ≃ UInt16 where in ArkLib/ToMathlib/UInt/Equiv.lean
• theorem succ'_injective : Function.Injective (succ' : Nat → Nat) in ArkLib/Data/Classes/HasSucc.lean
• def toList (xs : ChurchVec α) : List α in ArkLib/Data/CNat/Church.lean
• -- def mapNthNoMetaEval : (n : Fin αs.length) → ((αs.get n) → β) → HList αs → HList (αs.repla n β) in ArkLib/Data/List/HList.lean
• theorem add_assoc (m n p : ChurchNat α) : add (add m n) p = add m (add n p) in ArkLib/Data/CNat/Church.lean
• -- def churchNatIso : ValidChurchNat ≃ ℕ in ArkLib/Data/CNat/Church.lean
• theorem add_zero {n : ℕ} (a : CNat (n + 1)) : a + 0 = a in ArkLib/Data/CNat/Defs.lean
• -- theorem mul_add_distrib (m n p : ChurchNat α) : mul (add m n) p = add (mul m p) (mul n p) in ArkLib/Data/CNat/Church.lean
• def mulNat [Zero T] (a : Cayley T) : Nat → Cayley T in ArkLib/Data/CNat/Defs.lean
• def zero : ChurchNat α in ArkLib/Data/CNat/Church.lean
• theorem succ_succ {T : Type u} [HasSucc T] [Add T] [One T] [LawfulHasSucc T] (x : T) : in ArkLib/Data/Classes/HasSucc.lean
• lemma oddPart_even {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• def sub (m n : ChurchNat α) : ChurchNat α in ArkLib/Data/CNat/Church.lean
• theorem mul_one (n : ChurchNat α) : mul n one = n in ArkLib/Data/CNat/Church.lean
• theorem partialSum_nil : [].partialSum = [0] in ArkLib/Data/List/BigOperators.lean
• theorem zero_add (n : ChurchNat α) : add zero n = n in ArkLib/Data/CNat/Church.lean
• def churchAnd (p q : ChurchBool α) : ChurchBool α in ArkLib/Data/CNat/Church.lean
• def toNat (f : ValidChurchNat) : ℕ in ArkLib/Data/CNat/Church.lean
• theorem toNat_zero : toNat zero = 0 in ArkLib/Data/CNat/Church.lean
• -- theorem toNat_injective : Function.Injective (@ToNat.toNat α _ _) in ArkLib/Data/Classes/ToNat.lean
• def interleave {n : Nat} (xs : Vector α n) (ys : Vector α n) : Vector α (2 * n) in ArkLib/Data/List/Vector.lean
• def two : ChurchNat α in ArkLib/Data/CNat/Church.lean
• -- def CNat₂.add (m n : CNat₂) : CNat₂ in ArkLib/Data/CNat/Church.lean
• theorem findSum_of_le_sum {l : List ℕ} {j : ℕ} (h : j < l.sum) : ∃ n, findSum l j = some n in ArkLib/Data/List/BigOperators.lean
• def divNat [Zero T] [DecidableEq T] [ToNat T] in ArkLib/Data/CNat/Defs.lean
• lemma deevenize_evenize {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• instance instSub {n : ℕ} : Sub (CNat n) in ArkLib/Data/CNat/Defs.lean
• def head {α : Type u} {αs : List (Type u)} : HList (α :: αs) → α in ArkLib/Data/List/HList.lean
• def HList.ofDVec {α : Fin n → Type u} (l : DVec (m in ArkLib/Data/List/HList.lean
• lemma length_cons (x : Σ α : Type u, α) (xs : HList) : (x ::ₕ xs).length = xs.length + 1 in ArkLib/Data/List/HList.lean
• -- def mapNth (n : Fin' αs.length) (f : (αs.get' n) → β) (h : HList αs) : in ArkLib/Data/List/HList.lean
• def mulNat (a : AssocNat) : Nat → AssocNat in ArkLib/Data/CNat/AssocNat.lean
• theorem le_iff_toNat_le (a b : AssocNat) : a ≤ b ↔ toNat a ≤ toNat b in ArkLib/Data/CNat/AssocNat.lean
• def idxOf' [BEq α] (a : α) (l : List α) : ℕ in ArkLib/Data/List/Find.lean
• def findIdx' (p : α → Bool) (l : List α) : ℕ in ArkLib/Data/List/Find.lean
• theorem mul_two_eq_add {a : CNat 50} : a * 2 = a + a in ArkLib/Data/CNat/Defs.lean
• theorem succ'_ne_zero (n : Nat) : succ' n ≠ 0 in ArkLib/Data/Classes/HasSucc.lean
• instance [Zero T] [ToNat T] : DecidableRel (@LE.le (Cayley T) _) in ArkLib/Data/CNat/Defs.lean
• def lt {α : Type} (m n : ChurchNat α) : ChurchBool α in ArkLib/Data/CNat/Church.lean
• -- theorem mul_zero {n : ℕ} (a : CNat (n + 1)) : a * 0 = 0 in ArkLib/Data/CNat/Defs.lean
• theorem lt_iff_toNat_lt (a b : AssocNat) : a < b ↔ toNat a < toNat b in ArkLib/Data/CNat/AssocNat.lean
• lemma List.get_nil (i : Fin 0) (a : α) : [].get i = a in ArkLib/Data/List/HList.lean
• def finUInt8Equiv : Fin (2 ^ 8) ≃ UInt8 where in ArkLib/ToMathlib/UInt/Equiv.lean
• theorem zero_add {n : ℕ} (a : CNat (n + 1)) : 0 + a = a in ArkLib/Data/CNat/Defs.lean
• theorem add_succ (m n : ChurchNat α) : add (succ m) n = succ (add m n) in ArkLib/Data/CNat/Church.lean
• def ofNat (n : ℕ) : ValidChurchNat in ArkLib/Data/CNat/Church.lean
• -- theorem mulNat_distrib_add_one {a : CNat 1} {b _ : Nat} : in ArkLib/Data/CNat/Defs.lean
• theorem ranges_nil : List.ranges [] = [] in ArkLib/Data/List/BigOperators.lean
• def findFinIdxIfTrue (p : α → Bool) (l : List α) (h : ∃ x ∈ l, p x) : Fin l.length in ArkLib/Data/List/Find.lean
• def length : HList' β ls → Nat in ArkLib/Data/List/HList.lean
• lemma ext {m n : ChurchNat α} (h : ∀ f x, m f x = n f x) : m = n in ArkLib/Data/CNat/Church.lean
• def toFin (f : AssocFin n) : Fin (AssocNat.toNat n) in ArkLib/Data/CNat/AssocNat.lean
• def subNat [Zero T] [ToNat T] (a : Cayley T) : Nat → Cayley T in ArkLib/Data/CNat/Defs.lean
• lemma evenize_eq_comp_x_squared {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• -- theorem mul_assoc {a b c : CNat 2} : (a * b) * c = a * (b * c) in ArkLib/Data/CNat/Defs.lean
• def add (m n : ChurchNat α) : ChurchNat α in ArkLib/Data/CNat/Church.lean
• instance instMul {n : ℕ} : Mul (CNat n) in ArkLib/Data/CNat/Defs.lean
• def churchNil : ChurchVec α in ArkLib/Data/CNat/Church.lean
• def finIdxOf [BEq α] [LawfulBEq α] (a : α) (l : List α) : Fin (l.length + 1) in ArkLib/Data/List/Find.lean
• lemma evenPart_by_2 : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• theorem succ_mul {a b : AssocNat} : (succ a) * b = a * b + b in ArkLib/Data/CNat/AssocNat.lean
• theorem mul_two (n : ChurchNat α) : mul n two = add n n in ArkLib/Data/CNat/Church.lean
• instance instZero {n : ℕ} : Zero (CNat n) in ArkLib/Data/CNat/Defs.lean
• def ChurchVec (α : Type) : Type in ArkLib/Data/CNat/Church.lean
• def churchRec {α : Type} (n : ChurchNat α) (step : α → α) (base : α) : α in ArkLib/Data/CNat/Church.lean
• def ChurchBool (α : Type) : Type in ArkLib/Data/CNat/Church.lean
• theorem pred_succ {T : Type u} [HasSucc T] [Zero T] [ToNat T] (x : Cayley T) : in ArkLib/Data/CNat/Defs.lean
• theorem mul_assoc (m n p : ChurchNat α) : mul (mul m n) p = mul m (mul n p) in ArkLib/Data/CNat/Church.lean
• def getValue (l : HList) (i : Fin l.length) in ArkLib/Data/List/HList.lean
• lemma even_eval {f : Polynomial F} {s : F} (hEven : EvenPoly f) : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma oddPart_x_eval_eq {f : Polynomial F} {s : F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma oddPart_by_2 : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• def findSumIdx (l : List α) (j : α) : ℕ in ArkLib/Data/List/BigOperators.lean
• lemma evenPart_coeff {f : Polynomial F} {n : ℕ} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• theorem pow_three_eq_mul_sq {a : CNat 1} : a ^ 3 = a * (a * a) in ArkLib/Data/CNat/Defs.lean
• theorem ofNat_toNat (n : ChurchNat ℕ) : ofNat (toNat n) = n in ArkLib/Data/CNat/Church.lean
• lemma deevenize_coeff {f : Polynomial F} {n : ℕ} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• theorem idxOf'_eq_idxOf : @idxOf' = @idxOf in ArkLib/Data/List/Find.lean
• -- theorem pow_add_self {a : CNat 2} : a ^ 2 * a = a ^ 3 in ArkLib/Data/CNat/Defs.lean
• -- def DVec.toHList (l : DVec (m in ArkLib/Data/List/HList.lean
• -- def pow (m n : ChurchNat α) : ChurchNat α in ArkLib/Data/CNat/Church.lean
• def churchRecNat {β : Type} (n : ChurchNat ℕ) (step : β → β) (base : β) : β in ArkLib/Data/CNat/Church.lean
• -- -- def CNat.mul (m n : CNat) : CNat in ArkLib/Data/CNat/Church.lean
• theorem pow_two_eq_mul {a : CNat 2} : a ^ 2 = a * a in ArkLib/Data/CNat/Defs.lean
• def findSum (l : List α) (j : α) : Option α in ArkLib/Data/List/BigOperators.lean
• def findSumIdx' (l : List ℕ) (j : Fin l.sum) : Fin l.length in ArkLib/Data/List/BigOperators.lean
• def tail {α : Type u} {αs : List (Type u)} : HList (α :: αs) → HList αs in ArkLib/Data/List/HList.lean
• def ofFin {n : AssocNat} (f : Fin (AssocNat.toNat n)) : AssocFin n in ArkLib/Data/CNat/AssocNat.lean
• def test : HList [Nat, String, Nat] in ArkLib/Data/List/HList.lean
• -- theorem mul_assoc_self {a : CNat 2} : (a * a) * a = a * (a * a) in ArkLib/Data/CNat/Defs.lean
• theorem polynomial_sum_ext.{u, u_1} in ArkLib/Data/CodingTheory/BerlekampWelch/ToMathlib.lean
• def finIdxOfIfTrue [BEq α] [LawfulBEq α] (a : α) (l : List α) (h : a ∈ l) : Fin l.length in ArkLib/Data/List/Find.lean
• abbrev HList in ArkLib/Data/List/HList.lean
• def HList.toDVec (l : HList) : DVec (m in ArkLib/Data/List/HList.lean
• def someTypes : List Type in ArkLib/Data/List/HList.lean
• lemma evenPart_even {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean

---

sorry Tracking

✅ **Removed:** 2 `sorry`(s)

• theorem eq_of_degreeOf_lt_card_of_eval_eq {p q : R[X σ]} (S : σ → Finset R) in ArkLib/Data/MvPolynomial/Interpolation.lean
• lemma schwartz_zippel' {p : MvPolynomial σ R} (hp : p ≠ 0) (S : σ → Finset R) : in ArkLib/Data/MvPolynomial/Interpolation.lean

❌ **Added:** 14 `sorry`(s)

• theorem add_comm (m n : ChurchNat α) : add m n = add n m in ArkLib/Data/CNat/Church.lean
• def findSumIdx' (l : List ℕ) (j : Fin l.sum) : Fin l.length in ArkLib/Data/List/BigOperators.lean
• def pred (n : ChurchNat α) : ChurchNat α in ArkLib/Data/CNat/Church.lean
• theorem succ_mul {a b : AssocNat} : (succ a) * b = a * b + b in ArkLib/Data/CNat/AssocNat.lean
• def sub (m n : ChurchNat α) : ChurchNat α in ArkLib/Data/CNat/Church.lean
• theorem zero_mul {a : AssocNat} : 0 * a = 0 in ArkLib/Data/CNat/AssocNat.lean
• theorem toFun_eq_const_plus (t : AssocNat) : ∀ m : Nat, t m = t 0 + m in ArkLib/Data/CNat/AssocNat.lean
• instance [Zero T] [ToNat T] : DecidableEq (Cayley T) in ArkLib/Data/CNat/Defs.lean
• theorem ofNat_toNat (n : ChurchNat ℕ) : ofNat (toNat n) = n in ArkLib/Data/CNat/Church.lean
• theorem mul_distrib_add {a b : CNat 1} : a * (b + 1) = a * b + a in ArkLib/Data/CNat/Defs.lean
• theorem mul_add {a b c : AssocNat} : a * (b + c) = a * b + a * c in ArkLib/Data/CNat/AssocNat.lean
• def findSumIdxWith (l : List ℕ) (j : Fin l.sum) : (i : Fin l.length) × Fin (l.get i) in ArkLib/Data/List/BigOperators.lean
• theorem pred_succ {T : Type u} [HasSucc T] [Zero T] [ToNat T] (x : Cayley T) : in ArkLib/Data/CNat/Defs.lean
• def interleave {n : Nat} (xs : Vector α n) (ys : Vector α n) : Vector α (2 * n) in ArkLib/Data/List/Vector.lean

---

🎨 **Style Guide Adherence**

• ArkLib/Data/CNat/AssocNat.lean:1: "Use standard file headers including copyright, license (Apache 2.0), and authors."
• ArkLib/Data/CNat/AssocNat.lean:1: "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references."
• ArkLib/Data/CNat/AssocNat.lean:7: "Line Length: Keep lines under 100 characters."
• ArkLib/Data/CNat/AssocNat.lean:32: "Every definition and major theorem should have a docstring." (Violation also on lines 44, 48, 52, 57, 61, 65, 69, 72, 80, 85, 94, 99, 119, 122, 125, 128, 131, 140, 146, 149, 152, 161, 166, 173, 178, 184, 201, 205, 210, 215, 219, 224, 241, 245, 271, 282, 285, 289)
• ArkLib/Data/CNat/AssocNat.lean:81: "Indentation: Use 2 spaces for indentation."
• ArkLib/Data/CNat/Church.lean:45: "Every definition and major theorem should have a docstring." (Violation also on lines 55, 58, 63, 66, 77, 81, 84, 88, 111, 117, 123, 133, 135, 138, 141, 143, 145, 147, 149, 151, 153, 175, 183, 213, 217, 221, 237, 241, 245, 249, 260, 263, 278, 282)
• ArkLib/Data/CNat/Defs.lean:29: "Every definition and major theorem should have a docstring." (Violation also on lines 48, 52, 56, 62, 67, 73, 79, 83, 89, 93, 100, 112, 115, 123, 127, 134, 138, 144, 148, 158, 167, 175, 183, 191, 199, 208, 213, 217, 222, 226, 230, 234, 258, 262, 276, 279, 283, 287, 291, 295, 299, 303, 306, 309, 312, 314, 315, 317, 319, 321, 323, 324)
• ArkLib/Data/CNat/Defs.lean:222: "standardize on ≤ (le) and < (lt). Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."
• ArkLib/Data/CNat/Defs.lean:226: "standardize on ≤ (le) and < (lt). Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."
• ArkLib/Data/CNat/Defs.lean:245: "Place by at the end of the line preceding the tactic block. Indent the tactic block."
• ArkLib/Data/CNat/Defs.lean:341: "Operators: Put spaces on both sides of :, :=, and infix operators."
• ArkLib/Data/Classes/HasPred.lean:34: "Every definition and major theorem should have a docstring." (Violation also on line 49)
• ArkLib/Data/Classes/HasSucc.lean:31: "Every definition and major theorem should have a docstring." (Violation also on lines 43, 64, 69, 73)
• ArkLib/Data/Classes/ToNat.lean:21: "Every definition and major theorem should have a docstring." (Violation also on line 37)
• ArkLib/Data/CodingTheory.lean:1: "Use standard file headers including copyright, license (Apache 2.0), and authors."
• ArkLib/Data/CodingTheory.lean:1: "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references."
• ArkLib/Data/CodingTheory/BerlekampWelch/ToMathlib.lean:8: "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references."
• ArkLib/Data/CodingTheory/BerlekampWelch/ToMathlib.lean:8: "Every definition and major theorem should have a docstring."
• ArkLib/Data/CodingTheory/ReedMuller.lean:9: "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references."
• ArkLib/Data/List/BigOperators.lean:18: "Every definition and major theorem should have a docstring." (Violation also on lines 24, 29, 35, 41, 45, 54, 62, 65, 68, 71, 74, 79, 83)
• ArkLib/Data/List/Find.lean:16: "Every definition and major theorem should have a docstring." (Violation also on lines 21, 24, 27, 32, 35, 38, 41, 44, 48, 51, 54)
• ArkLib/Data/List/HList.lean:27: "Every definition and major theorem should have a docstring." (Violation also on lines 30, 32, 47, 50, 53, 57, 61, 66, 71, 81, 85, 93, 98, 101, 108)
• ArkLib/Data/List/Vector.lean:22: "Every definition and major theorem should have a docstring." (Violation also on line 30)
• ArkLib/Data/Polynomial/EvenAndOdd.lean:37: "Every definition and major theorem should have a docstring." (Violation also on lines 44, 52, 56, 59, 63, 83, 87, 98, 106, 113, 115)
• ArkLib/Data/Polynomial/EvenAndOdd.lean:148: "Use descriptive names for arithmetic/algebraic properties (e.g., mul_comm, add_assoc)."
• ArkLib/ProofSystem/DSL.lean:1: "Use standard file headers including copyright, license (Apache 2.0), and authors."
• ArkLib/ProofSystem/Stir.lean:1: "Use standard file headers including copyright, license (Apache 2.0), and authors."
• ArkLib/ProofSystem/Stir.lean:1: "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references."
• ArkLib/ProofSystem/Whir.lean:1: "Use standard file headers including copyright, license (Apache 2.0), and authors."
• ArkLib/ProofSystem/Whir.lean:1: "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references."
• ArkLib/ToMathlib/UInt/Equiv.lean:9: "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references."
• ArkLib/ToMathlib/UInt/Equiv.lean:9: "Every definition and major theorem should have a docstring." (Violation also on lines 15, 21, 27, 33)

---

📄 **Per-File Summaries**

• .github/workflows/ci.yml: Simplifies the CI workflow by utilizing the default lean-action caching and disabling the linter to avoid existing errors.
• .github/workflows/docs.yml: Update the documentation workflow to use standardized cache keys and enable integrated GitHub caching for the Lean build action.
• ArkLib.lean: Updates the ArkLib.lean entry point by importing several new modules across commitment schemes, coding theory, data structures, and proof systems.
• ArkLib/CommitmentScheme/Tensor.lean: This PR introduces a new file defining the framework for tensor-based polynomial commitment schemes and their underlying square-root IOP structures.
• ArkLib/CommitmentScheme/Trivial.lean: Introduces the Trivial commitment scheme module, which defines basic schemes where the prover sends raw data directly to the verifier for validation.
• ArkLib/Data/CNat/AssocNat.lean: Defines AssocNat, a representation of natural numbers as successor-preserving endomorphisms that makes addition definitionally associative.
• ArkLib/Data/CNat/Church.lean: Implements Church encodings for natural numbers, booleans, and vectors in Lean to demonstrate their computational and definitional properties.
• ArkLib/Data/CNat/Defs.lean: Defines the Cayley transformation and the CNat hierarchy, an iterated encoding of natural numbers where arithmetic operations like addition are definitionally associative.
• ArkLib/Data/Classes/HasPred.lean: Defines the HasPred and LawfulHasPred typeclasses to provide a predecessor operation and ensure it behaves as a left inverse to the successor operation.
• ArkLib/Data/Classes/HasSucc.lean: Defines the HasSucc and LawfulHasSucc typeclasses to provide an abstract successor operation and ensure its consistency with addition.
• ArkLib/Data/Classes/ToNat.lean: Defines the ToNat and LawfulToNat type classes to provide a uniform interface and algebraic laws for converting values into natural numbers.
• ArkLib/Data/CodingTheory.lean: This change creates a central entry point for the ArkLib.Data.CodingTheory module by consolidating and exporting all its constituent submodules.
• ArkLib/Data/CodingTheory/BerlekampWelch/ToMathlib.lean: Adds the polynomial_sum_ext theorem to establish extensionality for polynomial sums.
• ArkLib/Data/CodingTheory/ReedMuller.lean: Adds a new file to define and document Reed-Muller codes as a family of error-correcting codes within the library.
• ArkLib/Data/List/BigOperators.lean: Introduces definitions and theorems for partial sums and products of lists, including utilities for finding values and indices relative to cumulative sums.
• ArkLib/Data/List/Find.lean: Introduces findIdx' and idxOf' for improved definitional equality along with variants that return indices as Fin types.
• ArkLib/Data/List/HList.lean: Defines a heterogeneous list type as a list of sigma types and provides basic operations, notation, and conversions to dependent vectors.
• ArkLib/Data/List/Vector.lean: Adds a new utility file for List.Vector providing functions to interleave vectors and group elements into pairs.
• ArkLib/Data/MvPolynomial/Interpolation.lean: Formally prove the Schwartz-Zippel lemma and multivariable polynomial identity theorems, replacing previous sorry stubs.
• ArkLib/Data/Polynomial/EvenAndOdd.lean: Defines even and odd parts of polynomials and provides supporting lemmas for FFT-style splitting, transformations, and evaluation.
• ArkLib/ProofSystem/DSL.lean: Introduces an experimental Domain-Specific Language (DSL) for specifying vector and polynomial-based Information-Theoretic Oracle Relations (IORs) over finite fields.
• ArkLib/ProofSystem/Stir.lean: This file creates a top-level module for the Stir proof system by aggregating all of its sub-components through imports.
• ArkLib/ProofSystem/Whir.lean: This file creates a top-level module for the WHIR proof system by aggregating its core components and submodules through imports.
• ArkLib/ToMathlib/UInt/Equiv.lean: This file defines logical equivalences between Fin (2 ^ n) and various fixed-precision integer types, specifically UInt8, UInt16, UInt32, UInt64, and BitVec.

---

Last updated: 2026-02-25 00:10 UTC.

[quangvdao]

Can you remove this version and just keep the corrected theorem?

[quangvdao]

I would prefer if this proof does not need to set max heartbeat to be 8x the default. Could you ask Aristotle to identify the bottleneck and refactor the proof?