Define computable Additive NTT and transfer correctness

[dhsorens]

Context

CompPoly/Fields/Binary/AdditiveNTT/AdditiveNTT.lean has a module-level TODO:

Define computable additive NTT and transfer correctness proof to it

The current definitions are focused on noncomputable/theory-side constructions.

Proposed work

• Add a computable version of Additive NTT.
• Relate the existing correctness statement to the computable version.

Acceptance criteria

• A clear theorem/lemma connects the computable implementation to the existing correctness result.
• proofs and/or tests to show correctness

[chung-thai-nguyen]

This is now realized in https://github.com/Verified-zkEVM/CompPoly/blob/master/CompPoly/Fields/Binary/AdditiveNTT/Impl.lean so I'm closing it.