Forward NTT

This file provides spec-level forward NTT definitions together with an iterative radix-2 implementation.

@[inline]

def CompPoly.CPolynomial.NTT.Forward.nttAt {R : Type u_1} [Field R] (D : Domain R) (a : Array R) (k : D.Idx) : R

DFT/NTT formula at one output index.

@[inline]

def CompPoly.CPolynomial.NTT.Forward.forwardSpec {R : Type u_1} [Field R] (D : Domain R) (a : Array R) : Array R

Full forward transform specified directly from the NTT formula.

def CompPoly.CPolynomial.NTT.Forward.forwardStageSpec {R : Type u_1} [Field R] (D : Domain R) (completed : ℕ) (a : Array R) : Array R

Proof-oriented stagewise specification for the forward transform.

forwardStageSpec D completed a means: start from the bit-reversed input a, then apply exactly the first completed radix-2 butterfly stages.

def CompPoly.CPolynomial.NTT.Forward.forwardStagePureSpec {R : Type u_1} [Field R] (D : Domain R) (completed : ℕ) (a : Array R) : Array R

Stagewise pure specification built from butterflyStageSpec.

This removes the mutable-array implementation details but still mirrors the radix-2 control flow exactly.

def CompPoly.CPolynomial.NTT.Forward.forwardMathStageSpec {R : Type u_1} [Field R] (D : Domain R) (completed : ℕ) (a : Array R) : Array R

Mathematical partial-DFT state after completed radix-2 stages.

Each contiguous block of size 2^completed has already been transformed, while the remaining D.logN - completed bits are still encoded by bit-reversed block selection.

@[simp]

theorem CompPoly.CPolynomial.NTT.Forward.forwardStageSpec_zero {R : Type u_1} [Field R] (D : Domain R) (a : Array R) : forwardStageSpec D 0 a = Transform.bitRevPermute D a

@[simp]

theorem CompPoly.CPolynomial.NTT.Forward.forwardStageSpec_succ {R : Type u_1} [Field R] (D : Domain R) (stage : ℕ) (a : Array R) : forwardStageSpec D (stage + 1) a = Transform.butterflyStage D stage (forwardStageSpec D stage a)

@[simp]

theorem CompPoly.CPolynomial.NTT.Forward.forwardStagePureSpec_zero {R : Type u_1} [Field R] (D : Domain R) (a : Array R) : forwardStagePureSpec D 0 a = Transform.bitRevPermute D a

@[simp]

theorem CompPoly.CPolynomial.NTT.Forward.forwardStagePureSpec_succ {R : Type u_1} [Field R] (D : Domain R) (stage : ℕ) (a : Array R) : forwardStagePureSpec D (stage + 1) a = Transform.butterflyStageSpec D stage (forwardStagePureSpec D stage a)

@[simp]

theorem CompPoly.CPolynomial.NTT.Forward.size_forwardStageSpec {R : Type u_1} [Field R] (D : Domain R) (completed : ℕ) (a : Array R) : (forwardStageSpec D completed a).size = D.n

@[simp]

theorem CompPoly.CPolynomial.NTT.Forward.size_forwardStagePureSpec {R : Type u_1} [Field R] (D : Domain R) (completed : ℕ) (a : Array R) : (forwardStagePureSpec D completed a).size = D.n

theorem CompPoly.CPolynomial.NTT.Forward.forwardStageSpec_eq_forwardStagePureSpec {R : Type u_1} [Field R] (D : Domain R) (a : Array R) (completed : ℕ) : forwardStageSpec D completed a = forwardStagePureSpec D completed a

The algorithmic stage recursion agrees with the pure stage recursion.

This is the global bookkeeping bridge from the recursive algorithmic stages to their pointwise closed-form counterparts.

theorem CompPoly.CPolynomial.NTT.Forward.forwardMathStageSpec_zero {R : Type u_1} [Field R] (D : Domain R) (a : Array R) : forwardMathStageSpec D 0 a = Transform.bitRevPermute D a

Base case of the mathematical stage invariant: before any butterflies, the state is exactly the bit-reversed input.

theorem CompPoly.CPolynomial.NTT.Forward.butterflyStageSpec_forwardMathStageSpec_succ {R : Type u_1} [Field R] (D : Domain R) (stage : ℕ) (a : Array R) (hstage : stage < D.logN) : Transform.butterflyStageSpec D stage (forwardMathStageSpec D stage a) = forwardMathStageSpec D (stage + 1) a

theorem CompPoly.CPolynomial.NTT.Forward.forwardStagePureSpec_eq_forwardMathStageSpec {R : Type u_1} [Field R] (D : Domain R) (a : Array R) (completed : ℕ) : completed ≤ D.logN → forwardStagePureSpec D completed a = forwardMathStageSpec D completed a

The pure stage recursion matches the mathematical partial-DFT state at every stage.

theorem CompPoly.CPolynomial.NTT.Forward.runStages_bitRevPermute_eq_forwardStageSpec {R : Type u_1} [Field R] (D : Domain R) (a : Array R) : Transform.runStages D (Transform.bitRevPermute D a) = forwardStageSpec D D.logN a

Algorithmic stages coincide with the proof-oriented stagewise specification.

This is the loop-invariant bridge: the imperative for stage in [0:D.logN] implementation computes the same intermediate states as forwardStageSpec. Basically, this is recursion vs. for loop bookkeeping.

theorem CompPoly.CPolynomial.NTT.Forward.forwardMathStageSpec_final_eq_forwardSpec {R : Type u_1} [Field R] (D : Domain R) (a : Array R) : forwardMathStageSpec D D.logN a = forwardSpec D a

Once all logN stages are completed, the stagewise specification matches the direct NTT formula.

theorem CompPoly.CPolynomial.NTT.Forward.forwardStageSpec_final_eq_forwardSpec {R : Type u_1} [Field R] (D : Domain R) (a : Array R) : forwardStageSpec D D.logN a = forwardSpec D a

Once all logN stages are completed, the stagewise specification matches the direct NTT formula.

@[inline]

def CompPoly.CPolynomial.NTT.Forward.forwardImpl {R : Type u_1} [Field R] (D : Domain R) (p : Raw R) : Array R

Intended fast implementation entry point for NTT.

@[simp]

theorem CompPoly.CPolynomial.NTT.Forward.size_forwardSpec {R : Type u_1} [Field R] (D : Domain R) (a : Array R) : (forwardSpec D a).size = D.n

theorem CompPoly.CPolynomial.NTT.Forward.forwardImpl_correct {R : Type u_1} [Field R] (D : Domain R) (p : Raw R) : forwardImpl D p = forwardSpec D p