DIF NTTFast correctness

Correctness proofs for the decimation-in-frequency stage loop used by NTTFast.

def CompPoly.CPolynomial.NTTFast.Plan.difMathValueAt {R : Type u_1} [Field R] (D : NTT.Domain R) (completed : ℕ) (a : Array R) (idx : ℕ) : R

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

Mathematical state after completing completed descending DIF stages.

theorem CompPoly.CPolynomial.NTTFast.Plan.difMathStageSpec_zero {R : Type u_1} [Field R] (D : NTT.Domain R) (a : Array R) : difMathStageSpec D 0 a = NTT.loadNaturalArray D a

The initial DIF mathematical state is the naturally ordered input.

theorem CompPoly.CPolynomial.NTTFast.Plan.difMathStageSpec_final {R : Type u_1} [Field R] (D : NTT.Domain R) (a : Array R) : difMathStageSpec D D.logN a = NTT.Transform.bitRevPermute D (NTT.Forward.forwardSpec D a)

The final DIF mathematical state is the bit-reversed forward NTT output.

theorem CompPoly.CPolynomial.NTTFast.Plan.butterflyStageDIFWithTwiddles_difMathStageSpec_succ {R : Type u_1} [Field R] (D : NTT.Domain R) (stage : ℕ) (twiddles a : Array R) (hstage : stage < D.logN) (htw : ∀ j < 2 ^ stage, twiddles.getD j 0 = (D.omega ^ (D.n / 2 ^ (stage + 1))) ^ j) : butterflyStageDIFWithTwiddles D stage twiddles (difMathStageSpec D (D.logN - (stage + 1)) a) = difMathStageSpec D (D.logN - stage) a

One executable DIF butterfly stage advances the mathematical DIF stage spec.

theorem CompPoly.CPolynomial.NTTFast.Plan.runStagesDIFWithTwiddles_correct {R : Type u_1} [Field R] (D : NTT.Domain R) (a : Array R) : runStagesDIFWithTwiddles D (twiddleTable D) (NTT.loadNaturalArray D a) = NTT.Transform.bitRevPermute D (NTT.Forward.forwardSpec D a)

The DIF stage loop computes the bit-reversed forward NTT output.