Concrete additive NTT instances

Compatibility entry point for the generic executable additive NTT algorithms, together with concrete binary tower bases, instances and the existing example. Generic algorithm clients can import CompPoly.Fields.Binary.AdditiveNTT.Executable; generic correctness clients can import CompPoly.Fields.Binary.AdditiveNTT.Correctness.

instance AdditiveNTT.instNeZeroHPowNatOfNat_compPoly (k : ℕ) : NeZero (2 ^ k)

def AdditiveNTT.computableBasisExplicit (k : ℕ) (i : Fin (2 ^ k)) : ConcreteBinaryTower.ConcreteBTField k

Computable basis for ConcreteBTField k over ConcreteBTField 0. This is the explicit product of Z's.

theorem AdditiveNTT.computableBasisExplicit_eq_multilinearBasis (k : ℕ) : computableBasisExplicit k = fun (i : Fin (2 ^ (k - 0))) => (ConcreteBinaryTower.multilinearBasis 0 k ⋯) i

The executable bit-indexed basis equals the multilinear tower basis over level zero.

theorem AdditiveNTT.hβ_lin_indep_concrete (k : ℕ) : LinearIndependent (ConcreteBinaryTower.ConcreteBTField 0) (computableBasisExplicit k)

@[reducible, inline]

abbrev AdditiveNTT.BTF₃ : Type

instance AdditiveNTT.instNeZeroHPowOfNat_compPoly : NeZero (2 ^ 3)

@[instance_reducible]

instance AdditiveNTT.instFieldBTF₃ : Field BTF₃

@[instance_reducible]

instance AdditiveNTT.instDecidableEqBTF₃ : DecidableEq BTF₃

@[instance_reducible]

instance AdditiveNTT.instFintypeBTF₃ : Fintype BTF₃

def AdditiveNTT.testNTTBTF₃ : Fin (2 ^ (2 + 2)) → BTF₃

Test of the computable additive NTT over BTF₃ (an 8-bit binary tower field BTF₃). Input polynomial: p(x) = x (novel coefficients [7, 1, 0, 0]) of size 2^ℓ in BTF₃

• ℓ = 2
• R_rate = 2: Repetition rate, evaluating at S₀ of size 2^(ℓ + R_rate) = 16 points
• r = 2^3 = 8: Dimension of the basis for BTF₃ over GF(2) Output: A function Fin 16 → BTF₃ giving the evaluations of p(x) = x at 16 points in the evaluation domain S₀ defined by the spanning basis elements {β₀, ..., β_{ℓ + 𝓡 - 1}} of BTF₃ over GF(2).