Basic NTTFast correctness facts

Cached-plan well-formedness, twiddle-table facts, and shared proof helpers for NTTFast correctness.

def CompPoly.CPolynomial.NTTFast.Plan.WellFormed {R : Type u_1} [Field R] (P : Plan R) : Prop

Well-formedness condition for cached plan data.

theorem CompPoly.CPolynomial.NTTFast.Plan.twiddlePowers_size {R : Type u_1} [Field R] (D : NTT.Domain R) (stage : ℕ) : (twiddlePowers D stage).size = 2 ^ stage

The cached twiddle powers for a stage have exactly one entry per butterfly offset.

theorem CompPoly.CPolynomial.NTTFast.Plan.twiddlePowers_getD_eq_pow {R : Type u_1} [Field R] (D : NTT.Domain R) (stage j : ℕ) (hj : j < 2 ^ stage) : (twiddlePowers D stage).getD j 0 = (D.omega ^ (D.n / 2 ^ (stage + 1))) ^ j

Entries of the cached twiddle powers are the corresponding powers of the stage root.

theorem CompPoly.CPolynomial.NTTFast.Plan.twiddleTable_getD_eq_twiddlePowers {R : Type u_1} [Field R] (D : NTT.Domain R) (stage : ℕ) (hstage : stage < D.logN) : (twiddleTable D).getD stage #[] = twiddlePowers D stage

Looking up a valid stage in the twiddle table returns that stage's twiddle powers.

theorem CompPoly.CPolynomial.NTTFast.Plan.ofDomain_wellFormed {R : Type u_1} [Field R] (D : NTT.Domain R) : (ofDomain D).WellFormed

A plan built directly from a domain has well-formed cached data.

theorem CompPoly.CPolynomial.NTTFast.Plan.loadNaturalArray_eq {R : Type u_1} [Field R] (D : NTT.Domain R) (a : Array R) : NTT.loadNaturalArray D a = Array.ofFn fun (i : D.Idx) => a.getD (↑i) 0

Loading raw coefficients into a domain-sized array is Array.ofFn with zero padding.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_range_eq_rec {α : Type u_2} (f : ℕ → α → α) (x : α) (n : ℕ) : List.foldl (fun (acc : α) (i : ℕ) => f i acc) x (List.range n) = Nat.rec x (fun (i : ℕ) (acc : α) => f i acc) n

Folding over List.range is equivalent to the corresponding natural recursion.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_range_eq_rec_fst {α : Type u_2} {β : Type u_3} (f : ℕ → α × β → α × β) (x : α × β) (n : ℕ) : (List.foldl (fun (acc : α × β) (i : ℕ) => f i acc) x (List.range n)).1 = (Nat.rec x (fun (i : ℕ) (acc : α × β) => f i acc) n).1

First projections of pair-valued folds over List.range match natural recursion.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_range_congr {α : Type u_2} (f g : α → ℕ → α) (n : ℕ) : (∀ i < n, ∀ (acc : α), f acc i = g acc i) → ∀ (acc : α), List.foldl f acc (List.range n) = List.foldl g acc (List.range n)

Two fold functions give the same range fold when they agree at every step.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_range_preserve {α : Type u_2} (p : α → Prop) (f : α → ℕ → α) (n : ℕ) : (∀ i < n, ∀ (acc : α), p acc → p (f acc i)) → ∀ (acc : α), p acc → p (List.foldl f acc (List.range n))

A property preserved by every step is preserved by folding over List.range.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_range_congr_inv {α : Type u_2} (p : α → Prop) (f g : α → ℕ → α) (n : ℕ) : (∀ i < n, ∀ (acc : α), p acc → f acc i = g acc i) → (∀ i < n, ∀ (acc : α), p acc → p (f acc i)) → ∀ (acc : α), p acc → List.foldl f acc (List.range n) = List.foldl g acc (List.range n)

Congruence for range folds under an invariant preserved by the left fold.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_range'_succ_shift {α : Type u_2} (f : ℕ → α → α) (n offset : ℕ) (acc : α) : List.foldl (fun (acc : α) (t : ℕ) => f (t + 1) acc) acc (List.range' offset n) = List.foldl (fun (acc : α) (t : ℕ) => f t acc) acc (List.range' (offset + 1) n)

Shift a List.range' fold by one when the folded function shifts its index.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_range'_eq_range_add {α : Type u_2} (f : ℕ → α → α) (n offset : ℕ) (acc : α) : List.foldl (fun (acc : α) (t : ℕ) => f t acc) acc (List.range' offset n) = List.foldl (fun (acc : α) (t : ℕ) => f (offset + t) acc) acc (List.range n)

Reindex a List.range' fold as a fold over List.range with an offset.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_range'_append_split {α : Type u_2} (f : α → ℕ → α) (acc : α) (s m n : ℕ) : List.foldl f acc (List.range' s (m + n)) = List.foldl f (List.foldl f acc (List.range' s m)) (List.range' (s + m) n)

Split a List.range' fold over an appended interval into two folds.

theorem CompPoly.CPolynomial.NTTFast.Plan.three_mul_add_eq_add_two_mul_add (q b : ℕ) : 3 * q + b = q + (2 * q + b)

Arithmetic normal form used when rearranging adjacent radix-4 block indices.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_commute {α : Type u_2} (op : α → α) (f : ℕ → α → α) (n : ℕ) : (∀ i < n, ∀ (x : α), op (f i x) = f i (op x)) → ∀ (x : α), op (List.foldl (fun (x : α) (i : ℕ) => f i x) x (List.range n)) = List.foldl (fun (x : α) (i : ℕ) => f i x) (op x) (List.range n)

Move an operation through a range fold when it commutes with every step.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_commute_foldl {α : Type u_2} (f g : ℕ → α → α) (m n : ℕ) (hcomm : ∀ (i j : ℕ), i < m → j < n → ∀ (x : α), g j (f i x) = f i (g j x)) (x : α) : List.foldl (fun (x : α) (i : ℕ) => f i x) (List.foldl (fun (x : α) (j : ℕ) => g j x) x (List.range n)) (List.range m) = List.foldl (fun (x : α) (j : ℕ) => g j x) (List.foldl (fun (x : α) (i : ℕ) => f i x) x (List.range m)) (List.range n)

Swap two range folds when every step of one commutes with every step of the other.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_pair {α : Type u_2} (f g : ℕ → α → α) (n : ℕ) : (∀ (i j : ℕ), i < j → j < n → ∀ (x : α), f j (g i x) = g i (f j x)) → ∀ (x : α), List.foldl (fun (x : α) (i : ℕ) => g i (f i x)) x (List.range n) = List.foldl (fun (x : α) (i : ℕ) => g i x) (List.foldl (fun (x : α) (i : ℕ) => f i x) x (List.range n)) (List.range n)

Split a fold of paired same-index operations into two separate range folds.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_range_pair {α : Type u_2} (f : ℕ → α → α) (n : ℕ) (acc : α) : List.foldl (fun (acc : α) (b : ℕ) => f (2 * b + 1) (f (2 * b) acc)) acc (List.range n) = List.foldl (fun (acc : α) (k : ℕ) => f k acc) acc (List.range (2 * n))

Fold a pair of consecutive indexed operations as one fold over twice the range.

theorem CompPoly.CPolynomial.NTTFast.Plan.foldl_quad {α : Type u_2} (l₁ l₂ h₁ h₂ : ℕ → α → α) (n : ℕ) : (∀ (i j : ℕ), i < j → j < n → ∀ (x : α), l₁ j (l₂ i x) = l₂ i (l₁ j x)) → (∀ (i j : ℕ), i < j → j < n → ∀ (x : α), l₁ j (h₁ i x) = h₁ i (l₁ j x)) → (∀ (i j : ℕ), i < j → j < n → ∀ (x : α), l₁ j (h₂ i x) = h₂ i (l₁ j x)) → (∀ (i j : ℕ), i < j → j < n → ∀ (x : α), l₂ j (h₁ i x) = h₁ i (l₂ j x)) → (∀ (i j : ℕ), i < j → j < n → ∀ (x : α), l₂ j (h₂ i x) = h₂ i (l₂ j x)) → (∀ (i j : ℕ), i < j → j < n → ∀ (x : α), h₁ j (h₂ i x) = h₂ i (h₁ j x)) → ∀ (x : α), List.foldl (fun (x : α) (i : ℕ) => h₂ i (h₁ i (l₂ i (l₁ i x)))) x (List.range n) = List.foldl (fun (x : α) (i : ℕ) => h₂ i x) (List.foldl (fun (x : α) (i : ℕ) => h₁ i x) (List.foldl (fun (x : α) (i : ℕ) => l₂ i x) (List.foldl (fun (x : α) (i : ℕ) => l₁ i x) x (List.range n)) (List.range n)) (List.range n)) (List.range n)

Split a fold of four same-index operations into four separate range folds.

theorem CompPoly.CPolynomial.NTTFast.Plan.butterflyDITBlocks_eq_foldl {R : Type u_1} [Field R] (twiddles : Array R) (blockSize half : ℕ) (wm : R) (htwiddles : ∀ j < half, twiddles.getD j 0 = wm ^ j) (n blocks block : ℕ) (acc : Array R) : blocks = block + n → butterflyDITBlocks twiddles blockSize half blocks block acc = List.foldl (fun (acc : Array R) (block : ℕ) => NTT.Transform.butterflyBlockStep blockSize half wm block acc) acc (List.range' block n)

Express the recursive DIT block loop as a fold over baseline NTT block steps.

@[simp]

theorem CompPoly.CPolynomial.NTTFast.Plan.size_butterflyDITInner {R : Type u_1} [Field R] (twiddles : Array R) (limit j i0 i1 : ℕ) (acc : Array R) : (butterflyDITInner twiddles limit j i0 i1 acc).size = acc.size

@[simp]

theorem CompPoly.CPolynomial.NTTFast.Plan.size_butterflyDITBlocks {R : Type u_1} [Field R] (twiddles : Array R) (blockSize half blocks block : ℕ) (acc : Array R) : (butterflyDITBlocks twiddles blockSize half blocks block acc).size = acc.size

@[simp]

theorem CompPoly.CPolynomial.NTTFast.Plan.size_butterflyStageWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (stage : ℕ) (twiddles a : Array R) : (butterflyStageWithTwiddles D stage twiddles a).size = a.size

@[simp]

theorem CompPoly.CPolynomial.NTTFast.Plan.size_butterflyDITRadix4Inner {R : Type u_1} [Field R] (twiddlesLow twiddlesHigh : Array R) (limit j i0 i1 i2 i3 : ℕ) (acc : Array R) : (butterflyDITRadix4Inner twiddlesLow twiddlesHigh limit j i0 i1 i2 i3 acc).size = acc.size

@[simp]

theorem CompPoly.CPolynomial.NTTFast.Plan.size_butterflyDITRadix4Blocks {R : Type u_1} [Field R] (twiddlesLow twiddlesHigh : Array R) (blockSize quarter blocks block : ℕ) (acc : Array R) : (butterflyDITRadix4Blocks twiddlesLow twiddlesHigh blockSize quarter blocks block acc).size = acc.size

@[simp]

theorem CompPoly.CPolynomial.NTTFast.Plan.size_butterflyRadix4StageWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (lowStage : ℕ) (twiddlesLow twiddlesHigh a : Array R) : (butterflyRadix4StageWithTwiddles D lowStage twiddlesLow twiddlesHigh a).size = a.size

@[simp]

theorem CompPoly.CPolynomial.NTTFast.Plan.size_butterflyDIFInner {R : Type u_1} [Field R] (twiddles : Array R) (limit j i0 i1 : ℕ) (acc : Array R) : (butterflyDIFInner twiddles limit j i0 i1 acc).size = acc.size

@[simp]

theorem CompPoly.CPolynomial.NTTFast.Plan.size_butterflyDIFBlocks {R : Type u_1} [Field R] (twiddles : Array R) (blockSize half blocks block : ℕ) (acc : Array R) : (butterflyDIFBlocks twiddles blockSize half blocks block acc).size = acc.size

@[simp]

theorem CompPoly.CPolynomial.NTTFast.Plan.size_butterflyStageDIFWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (stage : ℕ) (twiddles a : Array R) : (butterflyStageDIFWithTwiddles D stage twiddles a).size = a.size

@[simp]

theorem CompPoly.CPolynomial.NTTFast.Plan.size_butterflyDIFRadix4Inner {R : Type u_1} [Field R] (twiddlesHigh twiddlesLow : Array R) (limit j i0 i1 i2 i3 : ℕ) (acc : Array R) : (butterflyDIFRadix4Inner twiddlesHigh twiddlesLow limit j i0 i1 i2 i3 acc).size = acc.size

@[simp]

theorem CompPoly.CPolynomial.NTTFast.Plan.size_butterflyDIFRadix4Blocks {R : Type u_1} [Field R] (twiddlesHigh twiddlesLow : Array R) (blockSize quarter blocks block : ℕ) (acc : Array R) : (butterflyDIFRadix4Blocks twiddlesHigh twiddlesLow blockSize quarter blocks block acc).size = acc.size

@[simp]

theorem CompPoly.CPolynomial.NTTFast.Plan.size_butterflyRadix4StageDIFWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (lowStage : ℕ) (twiddlesHigh twiddlesLow a : Array R) : (butterflyRadix4StageDIFWithTwiddles D lowStage twiddlesHigh twiddlesLow a).size = a.size