diff --git a/Zcash/Arithmetic.lean b/Zcash/Arithmetic.lean
new file mode 100644
index 000000000..a96090c05
--- /dev/null
+++ b/Zcash/Arithmetic.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2026 Ironwood Contributors.
+Released under the Apache License, Version 2.0.
+-/
+import Zcash.Arithmetic.Field
+import Zcash.Arithmetic.Group
+
+/-!
+# The arithmetic tier, and the two names it lends the whole repository
+
+`Zcash/Arithmetic/` holds the objects every other tier is stated over: the scalar field, the
+verifier group's reference string, the fingerprint MSM and the fast kernels behind them. Most
+of those names are local vocabulary and stay qualified — a module that wants `bestFftG` or
+`omegaOf` opens `Zcash.Arithmetic` for exactly that name.
+
+`Fp` and `URS` are the exceptions. They appear in nearly every statement in the repository, so
+they are re-exported at the `Zcash` root: any module declaring inside `Zcash.*` finds them by
+the enclosing-namespace walk, with no `open` at all. Nothing else earns root vocabulary.
+
+There is deliberately no `G` here. The verifier group is a type *variable* throughout
+(`URS (G : Type*)`, `variable {G : Type*}`); the concrete instantiations bind their own `G`
+locally, so there is no declaration to export.
+-/
+
+namespace Zcash
+
+export Arithmetic (Fp URS)
+
+end Zcash
diff --git a/Zcash/Arithmetic/CommitLagrange.lean b/Zcash/Arithmetic/CommitLagrange.lean
new file mode 100644
index 000000000..5ed9f6998
--- /dev/null
+++ b/Zcash/Arithmetic/CommitLagrange.lean
@@ -0,0 +1,113 @@
+import CompElliptic.Curves.Pasta.Fast.ProjectiveMontEquiv
+
+/-!
+# The fast Lagrange commitment
+
+`commit_lagrange` — a Pedersen vector commitment against a fixed basis, plus a blind — is the
+operation the verifying-key derivation runs 44 times over 2048-term columns, and it dominates
+that computation. This module gives the fast evaluation path for it (`commitLagrangeMontWith`)
+together with the PROVEN equality to the naive spec (`commitLagrangeMontWith_eq`), so a caller
+gets the speed without the statement ever mentioning the fast route.
+
+The speed comes from running the MSM over the **proven eight-limb Montgomery field**:
+`CompElliptic.Curves.Pasta.Fast.ProjectiveMontDefs` is the core-only twin of the group kernels
+(RCB addition, double-and-add, scatter Pippenger) there, compiled to native code through the
+`FastFieldNative` `precompileModules` leaf. This module is mathlib-side and deliberately NOT in
+that leaf's glob: it holds the `ZMod`-typed entry points — coordinates into Montgomery form,
+kernel, affine reading back — and chains the kernel's simulation theorem `msmM_spec` into the
+`_eq` ladder that lands on `Msm.commitLagrangeSpec`.
+
+`ofPVesM` must never be compared definitionally: unfolding it exposes the CIOS (Coarsely
+Integrated Operand Scanning) rounds, so the equalities below are stated and proved by rewriting only.
+-/
+
+namespace Zcash.Arithmetic
+
+open CompElliptic.Curves.Pasta.Fast
+open CompElliptic.Curves.Pasta.Fast.ProjectiveMont
+open CompElliptic.Curves.Pasta.Fast.ProjectiveMont (PM)
+open Montgomery.Native64x8
+open CompElliptic.Curves.Pasta.Fast.Projective
+open CompElliptic.Curves.Pasta.Fast.Projective.PVes
+-- The vendored `Msm` imported ironwood's scalar field, so `Fp` used to arrive here through the
+-- enclosing namespace. Upstream's `Msm` is standalone and carries its own (reducibly equal)
+-- `Fp := CompElliptic.Fields.Pasta.VestaScalarField`, which this module takes instead of
+-- importing `Zcash.Arithmetic.Field`.
+open CompElliptic.Curves.Pasta.Fast.Msm (Fp)
+
+local instance : Inhabited G := ⟨0⟩
+
+/-- Every `Fp` value's canonical representative is a 256-bit scalar. -/
+theorem val_lt_two_pow_256 (a : Fp) : a.val < 2 ^ 256 :=
+  lt_of_lt_of_le (ZMod.val_lt a) (by decide)
+
+/-- `PVes → PM`: each coordinate's canonical representative, entered into Montgomery form. -/
+def ofPVesM (P : PVes) : PM :=
+  ⟨VestaFq.ofNat P.X.val, VestaFq.ofNat P.Y.val, VestaFq.ofNat P.Z.val⟩
+
+theorem wfp_ofPVesM (P : PVes) : WFP (ofPVesM P) :=
+  ⟨wf_ofNat (ZMod.val_lt _), wf_ofNat (ZMod.val_lt _), wf_ofNat (ZMod.val_lt _)⟩
+
+theorem toPVesM_ofPVesM (P : PVes) : toPVesM (ofPVesM P) = P := by
+  cases P with
+  | mk X Y Z =>
+    simp only [toPVesM, ofPVesM, PVes.mk.injEq]
+    refine ⟨?_, ?_, ?_⟩ <;>
+      rw [montVal_ofNat (ZMod.val_lt _)]
+    exacts [ZMod.natCast_rightInverse X, ZMod.natCast_rightInverse Y, ZMod.natCast_rightInverse Z]
+
+theorem toGM_ofPVesM_ofAffine (g : G) : toGM (ofPVesM (ofAffine g)) = g := by
+  rw [toGM, toPVesM_ofPVesM, toAffine_ofAffine]
+
+theorem valid_toPVesM_ofPVesM_ofAffine (g : G) : Valid (toPVesM (ofPVesM (ofAffine g))) := by
+  rw [toPVesM_ofPVesM]
+  exact valid_ofAffine g
+
+/-- Entering Montgomery form and reading back is the identity, pointwise along a list.  Stated
+and proved by `rw` alone: the elaborator must never be asked for a *definitional* comparison
+across `ofPVesM`, since unfolding it exposes the CIOS rounds. -/
+theorem map_toGM_ofPVesM_ofAffine :
+    ∀ l : List G, (l.map fun g => ofPVesM (ofAffine g)).map toGM = l
+  | [] => rfl
+  | a :: l => by
+    rw [List.map_cons, List.map_cons, map_toGM_ofPVesM_ofAffine l, toGM_ofPVesM_ofAffine]
+
+/-- `commit_lagrange` through the Montgomery-lane kernel MSM. -/
+def commitLagrangeMontWith (c : ℕ) (blind : G) (basis : List G)
+    (coeffs : List Fp) : G :=
+  toGM (PM.msm c
+    ((coeffs.zip (basis ++ List.replicate (coeffs.length - basis.length) 0)).map
+      fun t => (t.1.val, ofPVesM (ofAffine t.2)))) + blind
+
+/-- **The Montgomery committer equals the naive `commit_lagrange` spec.** -/
+theorem commitLagrangeMontWith_eq (c : ℕ) (hc : 0 < c)
+    (blind : G) (basis : List G) (coeffs : List Fp) :
+    commitLagrangeMontWith c blind basis coeffs
+      = Msm.commitLagrangeSpec blind basis coeffs := by
+  unfold commitLagrangeMontWith
+  rw [toGM, ProjectiveMont.msmM_spec c hc _
+    (by intro t ht
+        rw [List.mem_map] at ht
+        obtain ⟨s, -, rfl⟩ := ht
+        exact wfp_ofPVesM _)
+    (by intro t ht
+        rw [List.mem_map] at ht
+        obtain ⟨s, -, rfl⟩ := ht
+        exact valid_toPVesM_ofPVesM_ofAffine s.2)
+    (by intro t ht
+        rw [List.mem_map] at ht
+        obtain ⟨s, -, rfl⟩ := ht
+        exact val_lt_two_pow_256 s.1)]
+  have hterms :
+      ((coeffs.zip (basis ++ List.replicate (coeffs.length - basis.length) 0)).map
+          fun t => (t.1.val, ofPVesM (ofAffine t.2))).map
+        (fun t => (t.1, toAffine (toPVesM t.2)))
+      = (coeffs.zip (basis ++ List.replicate (coeffs.length - basis.length) 0)).map
+          fun t => (t.1.val, t.2) := by
+    rw [List.map_map]
+    refine List.map_congr_left fun t _ => ?_
+    simp only [Function.comp_apply, toPVesM_ofPVesM, toAffine_ofAffine]
+  rw [hterms, Msm.zip_terms_eq, Msm.pippenger_eq_msm c hc, List.map_map]
+  rfl
+
+end Zcash.Arithmetic
diff --git a/Zcash/Arithmetic/Domain.lean b/Zcash/Arithmetic/Domain.lean
new file mode 100644
index 000000000..0a6b1a474
--- /dev/null
+++ b/Zcash/Arithmetic/Domain.lean
@@ -0,0 +1,117 @@
+import CompElliptic.Curves.Pasta
+import Zcash.Arithmetic.Field
+
+/-!
+# Evaluation-domain scalars (pasta `Fp` constants and facts)
+
+halo2's domain data as pure functions: binary exponentiation (`powFast`), the size-`2^k`
+domain root of unity `omegaOf` (pasta `Fp::GENERATOR = 5`, `ROOT_OF_UNITY` squared down,
+`EvaluationDomain::new`), `Fp::DELTA`, and the domain facts (primitive-root, power
+injectivity, size nonvanishing) bridged once to CompElliptic's certified Pasta root.
+Moved out of `Zcash/Bridge` per the Clean-boundary architecture
+(`Zcash/Circuits/Integration/clean-boundary.md`): these are verifier-native arithmetic
+facts, not bridge plumbing.
+-/
+
+namespace Zcash.Arithmetic
+
+/-- Binary exponentiation (`Monoid.npow`'s default recursion is linear — unusable for
+exponents of order `p/2^k`). -/
+def powFast (b : Fp) (n : ℕ) : Fp :=
+  if n = 0 then 1
+  else
+    let r := powFast (b * b) (n / 2)
+    if n % 2 = 1 then b * r else r
+  decreasing_by omega
+
+/-- Binary exponentiation agrees with the field's ordinary natural power. -/
+theorem powFast_eq_pow (b : Fp) (n : ℕ) :
+    powFast b n = b ^ n := by
+  induction n using Nat.strong_induction_on generalizing b with
+  | h n ih =>
+      rw [powFast]
+      by_cases hn : n = 0
+      · simp [hn]
+      · rw [if_neg hn]
+        have hhalf : n / 2 < n := Nat.div_lt_self (Nat.zero_lt_of_ne_zero hn) (by norm_num)
+        rw [ih (n / 2) hhalf]
+        by_cases hodd : n % 2 = 1
+        · rw [if_pos hodd]
+          have hn_split : n = 2 * (n / 2) + 1 := by omega
+          calc
+            b * (b * b) ^ (n / 2) =
+                b * (b ^ 2) ^ (n / 2) := by rw [pow_two]
+            _ = b ^ (2 * (n / 2) + 1) := by
+              rw [pow_add, pow_mul, pow_one]
+              ring
+            _ = b ^ n := congrArg (b ^ ·) hn_split.symm
+        · have heven : n % 2 = 0 := by omega
+          rw [if_neg hodd]
+          have hn_split : n = 2 * (n / 2) := by omega
+          calc
+            (b * b) ^ (n / 2) = (b ^ 2) ^ (n / 2) := by rw [pow_two]
+            _ = b ^ (2 * (n / 2)) := by rw [pow_mul]
+            _ = b ^ n := congrArg (b ^ ·) hn_split.symm
+
+/-- The size-`2^k` domain's root of unity: pasta `Fp::GENERATOR = 5`,
+`ROOT_OF_UNITY = 5^((p−1)/2^32)`, and `EvaluationDomain::new` squares it down `32 − k`
+times — so `omega = 5^((p−1)/2^k)`. Certified against the captured VK in `VkMatch`. -/
+def omegaOf (k : ℕ) : Fp :=
+  powFast 5 ((scalarFieldOrder - 1) / 2 ^ k)
+
+/--
+The executable generator spelling of every supported `omegaOf` agrees with powers of
+CompElliptic's certified Pasta root. This is the sole native-tier bridge in the domain
+facts below; `omegaOf` itself remains pure data and does not infect assignment
+definitions with the certificate's native axiom.
+-/
+private theorem omegaOf_eq_certifiedRootPow :
+    ∀ k : Fin 33,
+      omegaOf k =
+        powFast CompElliptic.Fields.Pasta.pallasBase.rootOfUnity
+          (2 ^ (32 - (k : ℕ))) := by
+  native_decide
+
+/-- `omegaOf k` is a primitive size-`2^k` domain root for every supported exponent. -/
+theorem omegaOf_isPrimitiveRoot (k : ℕ) (hk : k ≤ 32) :
+    IsPrimitiveRoot (omegaOf k) (2 ^ k) := by
+  have hroot :
+      IsPrimitiveRoot
+        CompElliptic.Fields.Pasta.pallasBase.rootOfUnity (2 ^ 32) :=
+    IsPrimitiveRoot.iff_orderOf.mpr
+      CompElliptic.Fields.Pasta.pallasBase.valid.rootOfUnity_order
+  rw [omegaOf_eq_certifiedRootPow ⟨k, Nat.lt_succ_of_le hk⟩, powFast_eq_pow]
+  apply IsPrimitiveRoot.pow (by positivity) hroot
+  rw [← pow_add, Nat.sub_add_cancel hk]
+
+/-- Every point `omegaOf k ^ row` lies in the size-`2^k` evaluation domain. -/
+theorem omegaOf_domain (k row : ℕ) (hk : k ≤ 32) :
+    (omegaOf k ^ row) ^ (2 ^ k) = 1 := by
+  rw [← pow_mul, mul_comm, pow_mul]
+  rw [(omegaOf_isPrimitiveRoot k hk).pow_eq_one, one_pow]
+
+/-- Distinct row indices below `2^k` name distinct evaluation-domain points. -/
+theorem omegaOf_powers_injective (k : ℕ) (hk : k ≤ 32) :
+    Function.Injective fun row : Fin (2 ^ k) => omegaOf k ^ (row : ℕ) := by
+  intro left right heq
+  apply Fin.ext
+  exact (omegaOf_isPrimitiveRoot k hk).pow_inj left.isLt right.isLt heq
+
+/-- The supported evaluation-domain size is nonzero when cast into `Fp`. -/
+theorem domainSize_cast_ne_zero (k : ℕ) (hk : k ≤ 32) :
+    ((2 ^ k : ℕ) : Fp) ≠ 0 := by
+  intro hzero
+  have hdiv : scalarFieldOrder ∣ 2 ^ k :=
+    (ZMod.natCast_eq_zero_iff (2 ^ k) scalarFieldOrder).mp hzero
+  apply Nat.not_dvd_of_pos_of_lt (by positivity) _ hdiv
+  calc
+    2 ^ k ≤ 2 ^ 32 := Nat.pow_le_pow_right (by omega) hk
+    _ < scalarFieldOrder := by
+      norm_num [scalarFieldOrder,
+        CompElliptic.Fields.Pasta.PALLAS_BASE_CARD]
+
+/-- pasta `Fp::DELTA = GENERATOR^(2^S) = 5^(2^32)`. -/
+def deltaFp : Fp := powFast 5 (2 ^ 32)
+
+
+end Zcash.Arithmetic
diff --git a/Zcash/Arithmetic/FastMsm.lean b/Zcash/Arithmetic/FastMsm.lean
new file mode 100644
index 000000000..766520220
--- /dev/null
+++ b/Zcash/Arithmetic/FastMsm.lean
@@ -0,0 +1,57 @@
+import Zcash.Arithmetic.Msm
+import CompElliptic.Curves.Pasta.Fast.Msm
+
+/-!
+# Fast compiled evaluation for the fingerprint MSM
+
+`Msm.evalNat` — the executable natural-scalar MSM the captured-fixture fingerprint
+checks evaluate (`capturedMsm_eval_eq_zero`) — is spelled as the specification: a
+`Finset` sum of per-generator `nsmul`s. Evaluated naively that is ~2050 binary
+double-and-add scalar multiplications (each paying one field inversion per affine
+point addition), which dominated the fixture modules' build times.
+
+`Msm.evalNatFast` computes the same value through the PROVEN windowed Pippenger
+accelerator (`CompElliptic.Curves.Pasta.Fast.Msm.pippengerFast`, generic over any
+`AddCommMonoid`), and `Msm.evalNat_eq_evalNatFast` is a kernel-checked equality
+registered with `@[csimp]`:
+the compiler substitutes the fast implementation at every subsequently compiled call
+site — in particular inside the fixtures' `native_decide` auxiliaries — while the
+statement surface and the kernel-level meaning of `evalNat` are untouched. This is
+the proven-equality counterpart of `implemented_by` (which is forbidden here because
+it is unchecked).
+-/
+
+namespace Zcash.Arithmetic.Msm
+
+open CompElliptic.Curves.Pasta.Fast.Msm (defaultWindow pippengerFastPar
+  pippengerFastPar_eq pippengerFast_eq pippenger_eq_msm)
+
+/-- `evalNat` through the proven windowed Pippenger accelerator, with the ~32 independent
+windows evaluated in parallel (`CompElliptic.Curves.Pasta.Fast.Msm.pippengerFastPar`):
+one bucketed MSM over the generator terms, the blinding/inner-product generators, and
+the extra term list.
+
+The replacement must stay generic over `[AddCommGroup G]` (a `@[csimp]` lemma replaces the
+whole constant), so the *affine* windows-parallel accelerator is the fastest admissible form
+here; the Vesta-specific projective interior
+(`CompElliptic.Curves.Pasta.Fast.MsmProj.pippengerProjScatterPar`) cannot be dispatched
+from a generic `G`. -/
+def evalNatFast {p : ℕ} {G : Type*} [AddCommGroup G]
+    (urs : URS G) (m : Msm urs.k (ZMod p) G) : G :=
+  pippengerFastPar defaultWindow
+    ((List.ofFn fun i => ((m.gScalars i).val, urs.g i))
+      ++ (m.wScalar.val, urs.w) :: (m.uScalar.val, urs.u)
+        :: m.other.map fun t => (t.1.val, t.2))
+
+/-- **The fast MSM evaluation is `evalNat`** — registered with `@[csimp]` so compiled
+code (including the fixtures' `native_decide` auxiliaries) runs the windows-parallel
+Pippenger form. -/
+@[csimp] theorem evalNat_eq_evalNatFast : @evalNat = @evalNatFast := by
+  funext p G inst urs m
+  unfold evalNat evalNatFast
+  rw [pippengerFastPar_eq, pippengerFast_eq, pippenger_eq_msm _ (by decide)]
+  simp only [List.map_append, List.map_cons, List.map_ofFn, List.map_map,
+    List.sum_append, List.sum_cons, List.sum_ofFn, Function.comp_def]
+  abel
+
+end Zcash.Arithmetic.Msm
diff --git a/Zcash/Arithmetic/Fft.lean b/Zcash/Arithmetic/Fft.lean
new file mode 100644
index 000000000..44993c466
--- /dev/null
+++ b/Zcash/Arithmetic/Fft.lean
@@ -0,0 +1,252 @@
+/-
+Copyright (c) 2026 Ironwood Contributors.
+Released under the Apache License, Version 2.0.
+-/
+import Zcash.Arithmetic.Domain
+import Zcash.Arithmetic.Group
+
+/-!
+# The Rust-mirroring group FFT and the derived Lagrange basis
+
+`bestFftG` is halo2's `best_fft` (`arithmetic.rs:192-256`) over an arbitrary `Fp`-module `G`:
+the bit-reversal permutation (`bitreverse`), a precomputed twiddle table, and `log_n` rounds of
+decimation-in-time butterflies. `derivedUrsGLagrange` runs it at the inverse root `omegaInvOf`
+and scales by `n⁻¹` to obtain the Lagrange-basis generators of a monomial URS
+(`Params::new`, `poly/commitment.rs:75-88`).
+
+These are pure arithmetic: they mention only `Fp`, `URS` and the module action, and nothing
+from the Clean circuit layer, so kernel transplants and accelerator lanes certify against
+them without importing the keygen pipeline. Keeping `bestFftG` generic over the `Fp`-module
+means its field instance (the scalar inverse DFT) and its group instances share one
+definition, so no scalar-vs-group agreement lemma ever needs to exist.
+
+The last section abstracts the loop nest itself (`fftGen`) and reduces it to pure folds
+(`fftGen_eq_folds`). That is the shared vocabulary every carrier transplant of this FFT is
+proven against — currently the scalar Montgomery one, `Zcash/Arithmetic/ScalarFftEquiv.lean`.
+-/
+
+namespace Zcash.Arithmetic
+
+variable {G : Type} [AddCommGroup G] [Inhabited G]
+
+/-! ## Lagrange URS derivation (`poly/commitment.rs:75-88`, `arithmetic.rs:192`) -/
+
+/-- `bitreverse(n, l)` — reverse the low `l` bits of `n` (`best_fft`'s local `bitreverse`,
+`arithmetic.rs:193-200`). -/
+def bitreverse (n l : ℕ) : ℕ := Id.run do
+  let mut r := 0
+  let mut m := n
+  for _ in [0:l] do
+    r := (r <<< 1) ||| (m &&& 1)
+    m := m >>> 1
+  return r
+
+/-- The size-`2^k` root of unity's inverse, `omega⁻¹ = omega^(2^k − 1)` (order `2^k`).
+This is halo2's `alpha_inv` (`ROOT_OF_UNITY_INV` squared `S − k` times,
+`poly/commitment.rs:76-79`), computed here from `omegaOf` since both are the same
+primitive `2^k`-th root. -/
+def omegaInvOf (k : ℕ) : Fp := powFast (omegaOf k) (2 ^ k - 1)
+
+/-- In-place radix-2 DIT FFT over the group `G` with `Fp` twiddles, mirroring
+`best_fft(a, omega, log_n)` (`arithmetic.rs:192-256`): bit-reversal permutation, precomputed
+twiddle powers `[omega^0 … omega^(n/2−1)]`, then `log_n` rounds of decimation-in-time
+butterflies `(a, b) ↦ (a + tw·b, a − tw·b)`. The scalar action `tw·b` is the same
+`ZMod.val • point` convention `commitLagrange` uses (Rust's iterative and recursive
+`best_fft` branches compute this identical result; we mirror the iterative one,
+`arithmetic.rs:223-252`). -/
+def bestFftG (a0 : Array G) (omega : Fp) (logN : ℕ) : Array G := Id.run do
+  let n := a0.size
+  let mut a := a0
+  -- bit-reversal permutation (`arithmetic.rs:207-212`)
+  for k in [0:n] do
+    let rk := bitreverse k logN
+    if k < rk then
+      let ak := a[k]!
+      let ark := a[rk]!
+      a := (a.set! k ark).set! rk ak
+  -- precompute twiddles `[omega^0 … omega^(n/2 − 1)]` (`arithmetic.rs:215-221`)
+  let mut tw : Array Fp := Array.mkEmpty (n / 2)
+  let mut w : Fp := 1
+  for _ in [0:n / 2] do
+    tw := tw.push w
+    w := w * omega
+  -- `log_n` rounds of butterflies (`arithmetic.rs:223-252`)
+  let mut half := 1
+  for _ in [0:logN] do
+    let chunk := 2 * half
+    let twiddleChunk := n / chunk
+    for c in [0:n / chunk] do
+      let s := c * chunk
+      for j in [0:half] do
+        let twdl := tw[j * twiddleChunk]!
+        let aIdx := s + j
+        let bIdx := s + half + j
+        let aOld := a[aIdx]!
+        let t := twdl.val • a[bIdx]!
+        a := a.set! aIdx (aOld + t)
+        a := a.set! bIdx (aOld - t)
+    half := chunk
+  return a
+
+/-- The Lagrange-basis generators derived from a monomial URS by inverse FFT and
+`n⁻¹` scaling, exactly as in halo2's `Params::new`. -/
+def derivedUrsGLagrange (urs : URS G) : List G :=
+  let monomial := List.ofFn urs.g
+  let minv : Fp := ((2 : Fp) ^ urs.k)⁻¹
+  (bestFftG monomial.toArray (omegaInvOf urs.k) urs.k).toList.map
+    fun point => minv.val • point
+
+/-! ## The loop nest, abstracted
+
+Every transplant of `bestFftG` onto a faster carrier (`Zcash/Vendor/CompPoly/ScalarFftDefs.lean`
+and the group kernels under `CompElliptic.Curves.Pasta.Fast`) is the *same* loop nest with the element
+type, the butterfly operations and the twiddle type swapped out. `fftGen` is that nest, so a
+transplant and its statement surface are recognized as two instances of it — both by `rfl`, since
+the loop bodies are textually the schedule below — and `fftGen_eq_folds` then converts the whole
+imperative nest into pure `List.foldl`s over three named steps (`permStep`, `butterflyGen`,
+`roundFoldGen`). A simulation proof only has to push its invariant through those three.
+
+Nothing here mentions `Fp`, `G` or the module action: these are the shape of the algorithm, not
+of the group FFT. -/
+
+/-- The radix-2 DIT FFT loop nest with the element type, the butterfly operations and the twiddle
+type all abstracted. `bestFftG` is the instance at the group's `(+)`, `(−)` and `ZMod.val`-smul
+(with the twiddle table factored out); a carrier transplant is the instance at its own
+operations. -/
+def fftGen {α τ : Type} [Inhabited α] [Inhabited τ] (add sub : α → α → α)
+    (smul : τ → α → α) (a0 : Array α) (tw : Array τ) (logN : ℕ) : Array α := Id.run do
+  let n := a0.size
+  let mut a := a0
+  for k in [0:n] do
+    let rk := bitreverse k logN
+    if k < rk then
+      let ak := a[k]!
+      let ark := a[rk]!
+      a := (a.set! k ark).set! rk ak
+  let mut half := 1
+  for _ in [0:logN] do
+    let chunk := 2 * half
+    let twiddleChunk := n / chunk
+    for c in [0:n / chunk] do
+      let s := c * chunk
+      for j in [0:half] do
+        let twdl := tw[j * twiddleChunk]!
+        let aIdx := s + j
+        let bIdx := s + half + j
+        let aOld := a[aIdx]!
+        let t := smul twdl a[bIdx]!
+        a := a.set! aIdx (add aOld t)
+        a := a.set! bIdx (sub aOld t)
+    half := chunk
+  return a
+
+/-- Phase 1 of `fftGen`, extracted verbatim: the bit-reversal permutation. -/
+private def brPermGen {α : Type} [Inhabited α] (a0 : Array α) (logN : ℕ) : Array α := Id.run do
+  let mut a := a0
+  for k in [0:a0.size] do
+    let rk := bitreverse k logN
+    if k < rk then
+      let ak := a[k]!
+      let ark := a[rk]!
+      a := (a.set! k ark).set! rk ak
+  return a
+
+/-- Phase 2 of `fftGen`, extracted verbatim: the `logN` butterfly rounds. -/
+private def roundsGen {α τ : Type} [Inhabited α] [Inhabited τ] (add sub : α → α → α)
+    (smul : τ → α → α) (n : ℕ) (tw : Array τ) (a0 : Array α) (logN : ℕ) : Array α := Id.run do
+  let mut a := a0
+  let mut half := 1
+  for _ in [0:logN] do
+    let chunk := 2 * half
+    let twiddleChunk := n / chunk
+    for c in [0:n / chunk] do
+      let s := c * chunk
+      for j in [0:half] do
+        let twdl := tw[j * twiddleChunk]!
+        let aIdx := s + j
+        let bIdx := s + half + j
+        let aOld := a[aIdx]!
+        let t := smul twdl a[bIdx]!
+        a := a.set! aIdx (add aOld t)
+        a := a.set! bIdx (sub aOld t)
+    half := chunk
+  return a
+
+private theorem fftGen_decompose {α τ : Type} [Inhabited α] [Inhabited τ] (add sub : α → α → α)
+    (smul : τ → α → α) (a0 : Array α) (tw : Array τ) (logN : ℕ) :
+    fftGen add sub smul a0 tw logN
+      = roundsGen add sub smul a0.size tw (brPermGen a0 logN) logN := rfl
+
+/-- One step of the bit-reversal permutation. -/
+def permStep {α : Type} [Inhabited α] (logN : ℕ) (a : Array α) (k : ℕ) : Array α :=
+  if k < bitreverse k logN then
+    (a.set! k a[bitreverse k logN]!).set! (bitreverse k logN) a[k]!
+  else a
+
+private theorem brPermGen_eq_foldl {α : Type} [Inhabited α] (a0 : Array α) (logN : ℕ) :
+    brPermGen a0 logN = (List.range a0.size).foldl (permStep logN) a0 := by
+  show (forIn (m := Id) [0:a0.size] a0 (fun k a =>
+      if k < bitreverse k logN then
+        pure (ForInStep.yield ((a.set! k a[bitreverse k logN]!).set! (bitreverse k logN) a[k]!))
+      else pure (ForInStep.yield a)) >>= fun r => (pure r : Id (Array α))) = _
+  simp only [← apply_ite (fun (z : Array α) => pure (f := Id) (ForInStep.yield z))]
+  simp only [Std.Legacy.Range.forIn_eq_forIn_range', Std.Legacy.Range.size, Nat.sub_zero,
+    Nat.add_sub_cancel, Nat.div_one, ← List.range_eq_range', List.forIn_pure_yield_eq_foldl]
+  rfl
+
+/-- A single butterfly `(c, j)` of a round at width `half`, as a pure array step. -/
+def butterflyGen {α τ : Type} [Inhabited α] [Inhabited τ] (add sub : α → α → α)
+    (smul : τ → α → α) (n half : ℕ) (tw : Array τ) (c j : ℕ) (a : Array α) : Array α :=
+  (a.set! (c * (2 * half) + j)
+      (add a[c * (2 * half) + j]!
+        (smul tw[j * (n / (2 * half))]! a[c * (2 * half) + half + j]!))).set!
+    (c * (2 * half) + half + j)
+      (sub a[c * (2 * half) + j]!
+        (smul tw[j * (n / (2 * half))]! a[c * (2 * half) + half + j]!))
+
+/-- One round of butterflies at width `half`, as a pure double fold. -/
+def roundFoldGen {α τ : Type} [Inhabited α] [Inhabited τ] (add sub : α → α → α)
+    (smul : τ → α → α) (n half : ℕ) (tw : Array τ) (a0 : Array α) : Array α :=
+  (List.range (n / (2 * half))).foldl
+    (fun a c => (List.range half).foldl
+      (fun a j => butterflyGen add sub smul n half tw c j a) a) a0
+
+private theorem roundsGen_eq_foldl {α τ : Type} [Inhabited α] [Inhabited τ] (add sub : α → α → α)
+    (smul : τ → α → α) (n : ℕ) (tw : Array τ) (a0 : Array α) (logN : ℕ) :
+    roundsGen add sub smul n tw a0 logN =
+      ((List.range logN).foldl (fun (p : MProd (Array α) ℕ) _ =>
+        ⟨roundFoldGen add sub smul n p.2 tw p.1, 2 * p.2⟩) ⟨a0, 1⟩).1 := by
+  show (forIn (m := Id) [0:logN] (⟨a0, 1⟩ : MProd (Array α) ℕ) (fun _ p =>
+      (forIn (m := Id) [0:n / (2 * p.2)] p.1 (fun c a =>
+        ForInStep.yield <$> forIn (m := Id) [0:p.2] a (fun j a =>
+          pure (ForInStep.yield (butterflyGen add sub smul n p.2 tw c j a)))) >>= fun a =>
+        pure (ForInStep.yield (⟨a, 2 * p.2⟩ : MProd (Array α) ℕ)))) >>= fun r =>
+      match r with | ⟨a, _⟩ => (pure a : Id (Array α))) = _
+  simp only [Std.Legacy.Range.forIn_eq_forIn_range', Std.Legacy.Range.size, Nat.sub_zero,
+    Nat.add_sub_cancel, Nat.div_one, ← List.range_eq_range', List.forIn_pure_yield_eq_foldl,
+    map_pure, pure_bind]
+  rfl
+
+private theorem foldl_rounds_half {α τ : Type} [Inhabited α] [Inhabited τ] (add sub : α → α → α)
+    (smul : τ → α → α) (n : ℕ) (tw : Array τ) (l : ℕ) (a : Array α) :
+    (List.range l).foldl (fun (p : MProd (Array α) ℕ) _ =>
+        ⟨roundFoldGen add sub smul n p.2 tw p.1, 2 * p.2⟩) ⟨a, 1⟩ =
+      ⟨(List.range l).foldl (fun a r => roundFoldGen add sub smul n (2 ^ r) tw a) a, 2 ^ l⟩ := by
+  induction l with
+  | zero => simp
+  | succ l ih =>
+    rw [List.range_succ, List.foldl_append, List.foldl_append, ih]
+    simp only [List.foldl_cons, List.foldl_nil]
+    refine congrArg₂ MProd.mk rfl ?_
+    rw [pow_succ]
+    ring
+
+/-- The generic loop nest as a permutation fold followed by `logN` round folds. -/
+theorem fftGen_eq_folds {α τ : Type} [Inhabited α] [Inhabited τ] (add sub : α → α → α)
+    (smul : τ → α → α) (a0 : Array α) (tw : Array τ) (logN : ℕ) :
+    fftGen add sub smul a0 tw logN
+      = (List.range logN).foldl (fun a r => roundFoldGen add sub smul a0.size (2 ^ r) tw a)
+          ((List.range a0.size).foldl (permStep logN) a0) := by
+  rw [fftGen_decompose, roundsGen_eq_foldl, foldl_rounds_half, brPermGen_eq_foldl]
+
+end Zcash.Arithmetic
diff --git a/Zcash/Snark/Core/Field.lean b/Zcash/Arithmetic/Field.lean
similarity index 95%
rename from Zcash/Snark/Core/Field.lean
rename to Zcash/Arithmetic/Field.lean
index 9d45c9b40..68a26f2ab 100644
--- a/Zcash/Snark/Core/Field.lean
+++ b/Zcash/Arithmetic/Field.lean
@@ -12,7 +12,7 @@ cardinality, which appears in the Schwartz–Zippel bounds. `Soundness.Vesta` pr
 order separately.
 -/
 
-namespace Zcash.Snark
+namespace Zcash.Arithmetic
 
 /-- The Vesta scalar-field order, equal to the Pallas base-field order. -/
 @[reducible] def scalarFieldOrder : ℕ := CompElliptic.Fields.Pasta.PALLAS_BASE_CARD
@@ -30,4 +30,4 @@ instance : NeZero scalarFieldOrder :=
 theorem card_Fp : Fintype.card Fp = scalarFieldOrder :=
   ZMod.card scalarFieldOrder
 
-end Zcash.Snark
+end Zcash.Arithmetic
diff --git a/Zcash/Snark/Core/Group.lean b/Zcash/Arithmetic/Group.lean
similarity index 96%
rename from Zcash/Snark/Core/Group.lean
rename to Zcash/Arithmetic/Group.lean
index 315ec158f..b55585bb2 100644
--- a/Zcash/Snark/Core/Group.lean
+++ b/Zcash/Arithmetic/Group.lean
@@ -16,7 +16,7 @@ The concrete instantiation is unconditional: CompElliptic's Vesta curve
 there with no change to this argument.
 -/
 
-namespace Zcash.Snark
+namespace Zcash.Arithmetic
 
 /-- The uniform reference string, mirroring halo2 `Params` (`poly/commitment.rs`): `k` is the
 `log₂` of the domain size, `g` the `n = 2 ^ k` generators, `w` the blinding generator, and `u`
@@ -28,4 +28,4 @@ structure URS (G : Type*) where
   w : G
   u : G
 
-end Zcash.Snark
+end Zcash.Arithmetic
diff --git a/Zcash/Snark/Core/Msm.lean b/Zcash/Arithmetic/Msm.lean
similarity index 98%
rename from Zcash/Snark/Core/Msm.lean
rename to Zcash/Arithmetic/Msm.lean
index 948e3404b..bd9d54d4f 100644
--- a/Zcash/Snark/Core/Msm.lean
+++ b/Zcash/Arithmetic/Msm.lean
@@ -1,5 +1,5 @@
 import Mathlib
-import Zcash.Snark.Core.Group
+import Zcash.Arithmetic.Group
 
 /-!
 # The fingerprint multiscalar multiplication
@@ -22,7 +22,7 @@ with (halo2 `MSM::{append_term, scale, add_msm}`). Everything stays generic over
 `F`-module `G`; the concrete instantiation is `F = F_p`, `G = E_q`.
 -/
 
-namespace Zcash.Snark
+namespace Zcash.Arithmetic
 
 /-- The fingerprint MSM (halo2 `MSM<C>`): `gScalars` are the coefficients of the `2 ^ k` URS
 generators, `wScalar` and `uScalar` the coefficients of the blinding and inner-product generators, and
@@ -136,4 +136,4 @@ theorem eval_addToGScalars {F G : Type*} [Field F] [AddCommGroup G] [Module F G]
 
 end Msm
 
-end Zcash.Snark
+end Zcash.Arithmetic
diff --git a/Zcash/Arithmetic/ScalarFftEquiv.lean b/Zcash/Arithmetic/ScalarFftEquiv.lean
new file mode 100644
index 000000000..ce1d45db3
--- /dev/null
+++ b/Zcash/Arithmetic/ScalarFftEquiv.lean
@@ -0,0 +1,312 @@
+/-
+Copyright (c) 2026 Ironwood Contributors.
+Released under the Apache License, Version 2.0.
+-/
+import Zcash.Vendor.CompPoly.ScalarFftDefs
+import CompElliptic.Vendor.CompPoly.Montgomery.Pasta
+import Zcash.Arithmetic.Fft
+
+/-!
+# The scalar Montgomery FFT is the proven group FFT at `G := Fp`
+
+`Zcash.Vendor.CompPoly.ScalarFftDefs` is a zero-import transplant of the radix-2 DIT FFT onto
+eight-limb Montgomery residues, generic over the modulus, so that it can sit in the
+`FastFieldNative` `precompileModules` leaf.  `fftS` below is its monomorphization at the Vesta
+**scalar** field (`PALLAS_BASE_CARD`, the Pallas *base* field in the Pasta naming), and this
+module — mathlib-side, and therefore *not* in that lane — proves that the transplant computes
+`bestFftG` instantiated at the `Fp`-module `Fp`.
+
+The bridge is the value map `montValS : Limbs8 → Fp`, `x ↦ x.toNat / 2 ^ 256`, which is
+`Montgomery.Native64x8.FastField.toField` read off raw limbs; it is correct on **well-formed**
+residues (`WFs x := x.Bounded ∧ x.toNat < p`), the carrier property of the proven
+`FastField PALLAS_BASE_CARD`.  Every scalar operation of the kernel is the corresponding
+`FastField` operation on the nose, so the per-operation cast lemmas are the vendored field's
+`toField_*` homomorphism lemmas.
+
+`fftS` and `bestFftG` are recognized as the same generic loop nest `fftGen`
+(`Zcash/Arithmetic/Fft.lean`, `rfl` on both sides), which `fftGen_eq_folds` turns into
+pure `List.foldl`s; the simulation invariant `SimS` is then pushed through the permutation and
+each butterfly.  The twiddle table of `bestFftG` is the only piece that differs: the kernel
+receives it in Montgomery form from the caller, so the butterflies compare `mul` against
+`t.val • ·` at corresponding entries.
+-/
+
+namespace Zcash.Arithmetic
+
+open Montgomery.Native64x8
+open Montgomery.Native64x8 (Limbs8)
+open CompElliptic.Fields.Pasta (PALLAS_BASE_CARD)
+
+/-- The vendored generic scalar FFT at the Vesta scalar field.  Its modulus limbs and Montgomery
+`negInv` are `Montgomery.Native64x8.PallasFq`'s: the Vesta scalar field *is* the Pallas base
+field (`PALLAS_BASE_CARD`), which is what `Fp` denotes — the Pasta naming swap, not a typo. -/
+def fftS (a0 : Array Limbs8) (tw : Array Limbs8) (logN : ℕ) : Array Limbs8 :=
+  Montgomery.ScalarFft.fft PallasFq.modulusLimbs PallasFq.negInv a0 tw logN
+
+/-! ## The field level -/
+
+/-- A well-formed Montgomery residue of the scalar field: bounded limbs holding a value below
+`p`.  This is exactly the carrier property of `FastField PALLAS_BASE_CARD`. -/
+def WFs (x : Limbs8) : Prop := x.Bounded ∧ x.toNat < PALLAS_BASE_CARD
+
+/-- The field value of a Montgomery residue: the residue divided by the radix `R = 2 ^ 256`. -/
+def montValS (x : Limbs8) : Fp := (x.toNat : Fp) * ((2 ^ 256 : ℕ) : Fp)⁻¹
+
+private def toFFs (x : Limbs8) (h : WFs x) : FastField PALLAS_BASE_CARD := ⟨x, h⟩
+
+theorem montValS_eq_toField {x : Limbs8} (h : WFs x) :
+    montValS x = FastField.toField (toFFs x h) := by
+  rw [montValS]
+  exact (FastField.toField_eq (toFFs x h)).symm
+
+theorem wfs_add {a b : Limbs8} (ha : WFs a) (hb : WFs b) : WFs (PallasFq.add a b) :=
+  (FastField.add (toFFs a ha) (toFFs b hb)).property
+
+theorem montValS_add {a b : Limbs8} (ha : WFs a) (hb : WFs b) :
+    montValS (PallasFq.add a b) = montValS a + montValS b := by
+  rw [montValS_eq_toField (wfs_add ha hb), montValS_eq_toField ha, montValS_eq_toField hb]
+  exact FastField.toField_add (toFFs a ha) (toFFs b hb)
+
+theorem wfs_sub {a b : Limbs8} (ha : WFs a) (hb : WFs b) : WFs (PallasFq.sub a b) :=
+  (FastField.sub (toFFs a ha) (toFFs b hb)).property
+
+theorem montValS_sub {a b : Limbs8} (ha : WFs a) (hb : WFs b) :
+    montValS (PallasFq.sub a b) = montValS a - montValS b := by
+  rw [montValS_eq_toField (wfs_sub ha hb), montValS_eq_toField ha, montValS_eq_toField hb]
+  exact FastField.toField_sub (toFFs a ha) (toFFs b hb)
+
+theorem wfs_mul {a b : Limbs8} (ha : WFs a) (hb : WFs b) : WFs (PallasFq.mul a b) :=
+  (FastField.mul (toFFs a ha) (toFFs b hb)).property
+
+theorem montValS_mul {a b : Limbs8} (ha : WFs a) (hb : WFs b) :
+    montValS (PallasFq.mul a b) = montValS a * montValS b := by
+  rw [montValS_eq_toField (wfs_mul ha hb), montValS_eq_toField ha, montValS_eq_toField hb]
+  exact FastField.toField_mul (toFFs a ha) (toFFs b hb)
+
+theorem wfs_zero : WFs PallasFq.zero := (FastField.zero PALLAS_BASE_CARD).property
+
+theorem montValS_zero : montValS PallasFq.zero = 0 := by
+  rw [montValS_eq_toField wfs_zero]
+  exact FastField.toField_zero
+
+/-- **Entering Montgomery form is the canonical cast**, for canonical naturals. -/
+theorem wfs_ofNat {k : ℕ} (h : k < PALLAS_BASE_CARD) : WFs (PallasFq.ofNat k) :=
+  (FastField.ofCanonicalNat k h).property
+
+theorem montValS_ofNat {k : ℕ} (h : k < PALLAS_BASE_CARD) :
+    montValS (PallasFq.ofNat k) = (k : Fp) := by
+  rw [montValS_eq_toField (wfs_ofNat h)]
+  exact FastField.toField_ofCanonicalNat h
+
+/-- Leaving Montgomery form yields the canonical representative of the field value. -/
+theorem toNat_toLimbs8 {x : Limbs8} (h : WFs x) :
+    (PallasFq.toLimbs8 x).toNat = (montValS x).val := by
+  have hlt : FastField.toNat (toFFs x h) < PALLAS_BASE_CARD := FastField.toNat_lt _
+  rw [montValS_eq_toField h, FastField.toField]
+  rw [ZMod.val_natCast_of_lt hlt]
+  rfl
+
+/-- `Array.get!` out of range hands back `default`, which is Montgomery zero. -/
+theorem default_eq_zero : (default : Limbs8) = PallasFq.zero := rfl
+
+theorem wfs_default : WFs (default : Limbs8) := wfs_zero
+
+theorem montValS_default : montValS (default : Limbs8) = (default : Fp) := by
+  rw [default_eq_zero, montValS_zero]
+  rfl
+
+/-! ## The twiddle table
+
+`bestFftG`'s twiddle table is built internally from `omega`; the kernel receives it from the
+caller in Montgomery form.  `twArrS` is that internal table extracted verbatim (so that
+`bestFftG_eq_genS` is `rfl`), and `twArrS_get` reads off its entries. -/
+
+private def twArrS (omega : Fp) (m : ℕ) : Array Fp := Id.run do
+  let mut tw : Array Fp := Array.mkEmpty m
+  let mut w : Fp := 1
+  for _ in [0:m] do
+    tw := tw.push w
+    w := w * omega
+  return tw
+
+private theorem twArrS_eq_foldl (omega : Fp) (m : ℕ) :
+    twArrS omega m = ((List.range m).foldl
+      (fun (p : MProd (Array Fp) Fp) _ => ⟨p.1.push p.2, p.2 * omega⟩)
+      ⟨Array.mkEmpty m, 1⟩).1 := by
+  show (forIn (m := Id) [0:m] (⟨Array.mkEmpty m, 1⟩ : MProd (Array Fp) Fp) (fun _ p =>
+      pure (ForInStep.yield ⟨p.1.push p.2, p.2 * omega⟩)) >>= fun r =>
+        match r with | ⟨tw, _⟩ => (pure tw : Id (Array Fp))) = _
+  simp only [Std.Legacy.Range.forIn_eq_forIn_range', Std.Legacy.Range.size, Nat.sub_zero,
+    Nat.add_sub_cancel, Nat.div_one, ← List.range_eq_range', List.forIn_pure_yield_eq_foldl]
+  rfl
+
+private theorem twFoldS_eq (omega : Fp) (m l : ℕ) :
+    (List.range l).foldl (fun (p : MProd (Array Fp) Fp) _ => ⟨p.1.push p.2, p.2 * omega⟩)
+        ⟨Array.mkEmpty m, 1⟩ =
+      ⟨((List.range l).map (omega ^ ·)).toArray, omega ^ l⟩ := by
+  induction l with
+  | zero => simp
+  | succ l ih =>
+    rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, ih]
+    refine congrArg₂ MProd.mk ?_ (by rw [pow_succ])
+    rw [List.map_append, List.map_cons, List.map_nil, ← List.push_toArray]
+
+private theorem twArrS_get (omega : Fp) (m i : ℕ) :
+    (twArrS omega m)[i]! = if i < m then omega ^ i else 0 := by
+  rw [twArrS_eq_foldl, twFoldS_eq]
+  by_cases hi : i < m
+  · rw [if_pos hi, getElem!_pos _ i (by simpa using hi)]
+    simp
+  · rw [if_neg hi, getElem!_neg _ i (by simp; omega)]
+    rfl
+
+/-! ## The loop nest -/
+
+/-- The kernel FFT is the generic loop nest at the scalar field operations. -/
+private theorem fftS_eq_gen (a0 : Array Limbs8) (tw : Array Limbs8) (logN : ℕ) :
+    fftS a0 tw logN
+      = fftGen PallasFq.add PallasFq.sub PallasFq.mul a0 tw logN := rfl
+
+/-- `bestFftG` at `G := Fp` is the generic loop nest at the field's own operations, with the
+twiddle table factored out. -/
+private theorem bestFftG_eq_genS (a0 : Array Fp) (omega : Fp) (logN : ℕ) :
+    bestFftG a0 omega logN
+      = fftGen (· + ·) (· - ·) (fun (t : Fp) p => t.val • p) a0
+          (twArrS omega (a0.size / 2)) logN := rfl
+
+/-! ## The simulation invariant -/
+
+/-- The kernel array simulates the field array: every cell is a well-formed residue, and the
+cellwise Montgomery readings are the field array. -/
+private def SimS (a : Array Limbs8) (b : Array Fp) : Prop :=
+  (∀ x ∈ a, WFs x) ∧ a.map montValS = b
+
+private theorem SimS.wf_get {a : Array Limbs8} {b : Array Fp} (h : SimS a b) (i : ℕ) :
+    WFs a[i]! := by
+  by_cases hi : i < a.size
+  · rw [getElem!_pos a i hi]
+    exact h.1 _ (Array.getElem_mem hi)
+  · rw [getElem!_neg a i hi]
+    exact wfs_default
+
+private theorem SimS.get {a : Array Limbs8} {b : Array Fp} (h : SimS a b) (i : ℕ) :
+    montValS a[i]! = b[i]! := by
+  rw [← h.2]
+  by_cases hi : i < a.size
+  · rw [getElem!_pos a i hi, getElem!_pos (a.map montValS) i (by simpa using hi),
+      Array.getElem_map]
+  · rw [getElem!_neg a i hi, getElem!_neg (a.map montValS) i (by simpa using hi),
+      montValS_default]
+
+private theorem SimS.set {a : Array Limbs8} {b : Array Fp} (h : SimS a b) (i : ℕ) {p : Limbs8}
+    (hp : WFs p) : SimS (a.set! i p) (b.set! i (montValS p)) := by
+  refine ⟨?_, ?_⟩
+  · intro q hq
+    rw [Array.set!_eq_setIfInBounds] at hq
+    rcases Array.mem_or_eq_of_mem_setIfInBounds hq with hq | rfl
+    · exact h.1 q hq
+    · exact hp
+  · rw [Array.set!_eq_setIfInBounds, Array.set!_eq_setIfInBounds, Array.map_setIfInBounds, h.2]
+
+private theorem foldl_relS {σ σ' β : Type} (R : σ → σ' → Prop) (l : List β)
+    (f : σ → β → σ) (g : σ' → β → σ')
+    (hstep : ∀ s s' x, R s s' → R (f s x) (g s' x)) :
+    ∀ s s', R s s' → R (l.foldl f s) (l.foldl g s') := by
+  induction l with
+  | nil => exact fun s s' h => h
+  | cons x l ih => exact fun s s' h => ih _ _ (hstep s s' x h)
+
+private theorem simS_permStep (logN : ℕ) {a : Array Limbs8} {b : Array Fp} (h : SimS a b)
+    (k : ℕ) : SimS (permStep logN a k) (permStep logN b k) := by
+  unfold permStep
+  split
+  · have h1 : SimS (a.set! k a[bitreverse k logN]!)
+        (b.set! k (montValS a[bitreverse k logN]!)) :=
+      h.set k (h.wf_get _)
+    rw [h.get (bitreverse k logN)] at h1
+    have h2 := h1.set (bitreverse k logN) (h.wf_get k)
+    rw [h.get k] at h2
+    exact h2
+  · exact h
+
+/-- **A single butterfly preserves the simulation**: `add`/`sub` are the field's own, and the
+Montgomery twiddle multiply is the `ZMod.val`-smul of the corresponding field twiddle. -/
+private theorem simS_bfly {a : Array Limbs8} {b : Array Fp} (h : SimS a b) (iA iB : ℕ)
+    (d : Limbs8) (e : Fp) (hd : WFs d) (he : montValS d = e) :
+    SimS ((a.set! iA (PallasFq.add a[iA]! (PallasFq.mul d a[iB]!))).set! iB
+            (PallasFq.sub a[iA]! (PallasFq.mul d a[iB]!)))
+        ((b.set! iA (b[iA]! + e.val • b[iB]!)).set! iB (b[iA]! - e.val • b[iB]!)) := by
+  have hwA : WFs a[iA]! := h.wf_get iA
+  have hwB : WFs a[iB]! := h.wf_get iB
+  have hwt : WFs (PallasFq.mul d a[iB]!) := wfs_mul hd hwB
+  have hst : montValS (PallasFq.mul d a[iB]!) = e.val • b[iB]! := by
+    rw [montValS_mul hd hwB, he, h.get iB,
+      ← Nat.cast_smul_eq_nsmul Fp e.val b[iB]!, ZMod.natCast_rightInverse e, smul_eq_mul]
+  have hplus : montValS (PallasFq.add a[iA]! (PallasFq.mul d a[iB]!))
+      = b[iA]! + e.val • b[iB]! := by
+    rw [montValS_add hwA hwt, h.get iA, hst]
+  have hminus : montValS (PallasFq.sub a[iA]! (PallasFq.mul d a[iB]!))
+      = b[iA]! - e.val • b[iB]! := by
+    rw [montValS_sub hwA hwt, h.get iA, hst]
+  have s1 := h.set iA (wfs_add hwA hwt)
+  rw [hplus] at s1
+  have s2 := s1.set iB (wfs_sub hwA hwt)
+  rw [hminus] at s2
+  exact s2
+
+private theorem simS_butterfly (n half : ℕ) (tw : Array Limbs8) (twFp : Array Fp)
+    (hwtw : ∀ i : ℕ, WFs tw[i]!) (htw : ∀ i : ℕ, montValS tw[i]! = twFp[i]!) (c j : ℕ)
+    {a : Array Limbs8} {b : Array Fp} (h : SimS a b) :
+    SimS (butterflyGen PallasFq.add PallasFq.sub PallasFq.mul n half tw c j a)
+        (butterflyGen (· + ·) (· - ·) (fun (t : Fp) p => t.val • p) n half twFp c j b) :=
+  simS_bfly h _ _ _ _ (hwtw (j * (n / (2 * half)))) (htw (j * (n / (2 * half))))
+
+private theorem simS_roundFold (n half : ℕ) (tw : Array Limbs8) (twFp : Array Fp)
+    (hwtw : ∀ i : ℕ, WFs tw[i]!) (htw : ∀ i : ℕ, montValS tw[i]! = twFp[i]!)
+    {a : Array Limbs8} {b : Array Fp} (h : SimS a b) :
+    SimS (roundFoldGen PallasFq.add PallasFq.sub PallasFq.mul n half tw a)
+        (roundFoldGen (· + ·) (· - ·) (fun (t : Fp) p => t.val • p) n half twFp b) :=
+  foldl_relS SimS _ _ _
+    (fun s s' c hs => foldl_relS SimS _ _ _
+      (fun _ _ j hr => simS_butterfly n half tw twFp hwtw htw c j hr) s s' hs) a b h
+
+/-! ## The simulation theorem -/
+
+/-- **The scalar kernel FFT is `bestFftG` at `G := Fp`.**  With Montgomery twiddles reading back
+as `ω^i`, the kernel's limb array stays well formed and maps cellwise, under `montValS`, onto
+`bestFftG` of the mapped input: the bit-reversal permutation moves cells, and every butterfly is
+the field's own add/sub/mul. -/
+theorem fftS_spec (a0 : Array Limbs8) (tw : Array Limbs8) (omega : Fp) (logN : ℕ)
+    (hwf : ∀ x ∈ a0, WFs x) (hwtw : ∀ i : ℕ, WFs tw[i]!)
+    (htwsize : tw.size = a0.size / 2)
+    (htw : ∀ i, i < a0.size / 2 → montValS tw[i]! = omega ^ i) :
+    (∀ x ∈ fftS a0 tw logN, WFs x)
+      ∧ (fftS a0 tw logN).map montValS
+          = bestFftG (a0.map montValS) omega logN := by
+  have hsize : (a0.map montValS).size = a0.size := Array.size_map ..
+  have htw' : ∀ i : ℕ, montValS tw[i]! = (twArrS omega (a0.size / 2))[i]! := by
+    intro i
+    rw [twArrS_get]
+    by_cases hi : i < a0.size / 2
+    · rw [if_pos hi, htw i hi]
+    · rw [if_neg hi, getElem!_neg tw i (by omega), montValS_default]
+      rfl
+  have hsim0 : SimS a0 (a0.map montValS) := ⟨hwf, rfl⟩
+  have hperm : SimS ((List.range a0.size).foldl (permStep logN) a0)
+      ((List.range a0.size).foldl (permStep logN) (a0.map montValS)) :=
+    foldl_relS SimS _ _ _ (fun s s' k hs => simS_permStep logN hs k) _ _ hsim0
+  have hrounds : SimS
+      ((List.range logN).foldl (fun a r =>
+        roundFoldGen PallasFq.add PallasFq.sub PallasFq.mul a0.size (2 ^ r) tw a)
+        ((List.range a0.size).foldl (permStep logN) a0))
+      ((List.range logN).foldl (fun a r =>
+        roundFoldGen (· + ·) (· - ·) (fun (t : Fp) p => t.val • p) a0.size (2 ^ r)
+          (twArrS omega (a0.size / 2)) a)
+        ((List.range a0.size).foldl (permStep logN) (a0.map montValS))) :=
+    foldl_relS SimS _ _ _
+      (fun s s' r hs => simS_roundFold a0.size (2 ^ r) tw _ hwtw htw' hs) _ _ hperm
+  rw [fftS_eq_gen, fftGen_eq_folds, bestFftG_eq_genS, fftGen_eq_folds,
+    hsize]
+  exact hrounds
+
+end Zcash.Arithmetic
diff --git a/Zcash/Arithmetic/VestaModule.lean b/Zcash/Arithmetic/VestaModule.lean
new file mode 100644
index 000000000..6ed4b52ad
--- /dev/null
+++ b/Zcash/Arithmetic/VestaModule.lean
@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2026 Ironwood Contributors.
+Released under the Apache License, Version 2.0.
+-/
+import CompElliptic.Curves.Pasta.Fast.Projective
+import Zcash.Arithmetic.Field
+import CompElliptic.Curves.PastaOrder
+
+/-!
+# The Vesta curve as an `Fp`-module, as a plain `def`
+
+The keygen bilinearity theorem (`commitLagrangeSpec_derivedUrsGLagrange`) needs the verifier
+group to be an `Fp`-module: `ZMod.val`-smuls only compose across the DFT because `p • P = 0`.
+`Zcash.Snark.Soundness.Vesta` installs exactly that instance (`vestaFpModule`) for the deployed
+curve, but its import closure is the whole soundness development, which the concrete keygen
+certificate has no reason to load.
+
+This module supplies the same structure for `Fast.Projective.G` from CompElliptic's pinned
+point count alone, and deliberately **not** as an `instance`: the theorems it feeds have
+`Fp`-module-free statements (`commitLagrangeSpec` smuls are `ℕ`-smuls), so the structure is
+only ever needed *inside* proofs, where it is introduced explicitly.  Keeping it out of
+instance search is what guarantees no second `Module Fp (SWPoint Vesta.curve)` can collide
+with `Soundness.Vesta`'s in a module that reaches both.
+-/
+
+namespace Zcash.Arithmetic
+
+open CompElliptic.Curves.Pasta
+open CompElliptic.Curves.Pasta.Fast.Projective
+
+/-- Every Vesta point is `p`-torsion, from CompElliptic's pinned `Vesta.card_eq` and the fact
+that a finite group is annihilated by its cardinality.  Mirrors `Zcash.Snark.vestaOrder`. -/
+theorem vestaGroupOrder (P : G) : (scalarFieldOrder : ℕ) • P = 0 := by
+  have hcard : Nat.card G = scalarFieldOrder := Vesta.card_eq
+  rw [← hcard]
+  exact addOrderOf_dvd_iff_nsmul_eq_zero.mp (addOrderOf_dvd_natCard P)
+
+/-- The deployed verifier group as an `Fp`-module.  NOT an instance — see the module
+docstring; introduce it with `haveI` inside a proof that needs it. -/
+@[implicit_reducible]
+def vestaFpModuleDef : Module Fp G := AddCommGroup.zmodModule vestaGroupOrder
+
+end Zcash.Arithmetic
diff --git a/Zcash/Common/ParMap.lean b/Zcash/Common/ParMap.lean
new file mode 100644
index 000000000..27052a395
--- /dev/null
+++ b/Zcash/Common/ParMap.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2026 Ironwood Contributors.
+Released under the Apache License, Version 2.0.
+-/
+import Mathlib.Data.List.Basic
+
+/-!
+# Parallel `List.map` via the task runtime, with a proof it is just `List.map`
+
+`List.parMap f xs` evaluates `f` on every element of `xs` concurrently, using the Lean
+task runtime (`Task.spawn` / `Task.get`), and collects the results in order. It is a *pure*
+function — `Task` is logically the one-field structure `⟨get : α⟩`, `Task.spawn fn = ⟨fn ()⟩`
+and `Task.get ⟨a⟩ = a` are both definitional — so it is provably equal to `List.map`
+(`List.parMap_eq_map`). The only thing `parMap` changes is the *evaluation strategy*: under
+`native_decide` (compiled to C, run on the real task scheduler) the elementwise work runs on
+the thread pool (up to `nproc` workers), which is the point for the independent
+`commit_lagrange` commitments of the VK-commitment certification.
+
+Because the equality to `List.map` is definitional, swapping `List.map` for `List.parMap` in a
+`native_decide`-backed definition changes nothing about the statement's meaning or trust base:
+the compiled `Task` primitives are already part of the `native_decide` trust boundary, and the
+`Std`/kernel view is literally `List.map`.
+
+## References
+* Lean task runtime: `Init/Core.lean` (`Task`, `Task.spawn`, `Task.get`); the runtime overrides
+  `Task`'s representation, `Task.spawn`/`Task.get` are `@[extern]` — but the reference Lean bodies
+  `Task.spawn fn = ⟨fn ()⟩`, `Task.get ⟨a⟩ = a` are what the kernel and `decide` see.
+-/
+
+universe u v
+
+/-- Parallel map: spawn a task per element, then collect the results in order. Pure — equal to
+`List.map` (`List.parMap_eq_map`) — but evaluates the elementwise work concurrently on the task
+runtime under `native_decide`/compiled execution. -/
+def _root_.List.parMap {α : Type u} {β : Type v} (f : α → β) (xs : List α) : List β :=
+  (xs.map (fun x => Task.spawn (fun _ => f x))).map Task.get
+
+/-- `List.parMap` is `List.map`: the task round-trip `Task.get (Task.spawn (fun _ => f x))` is
+`f x` definitionally, so nothing but the evaluation strategy differs. -/
+@[simp] theorem _root_.List.parMap_eq_map {α : Type u} {β : Type v} (f : α → β) (xs : List α) :
+    xs.parMap f = xs.map f := by
+  rw [List.parMap, List.map_map]; rfl
diff --git a/Zcash/FastFieldNative.lean b/Zcash/FastFieldNative.lean
new file mode 100644
index 000000000..f40584d58
--- /dev/null
+++ b/Zcash/FastFieldNative.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2026 Ironwood Contributors.
+Released under the Apache License, Version 2.0.
+-/
+import CompElliptic.Vendor.CompPoly.Montgomery.Native64x8Defs
+import CompElliptic.Curves.Pasta.Fast.ProjectiveMontDefs
+import Zcash.Vendor.CompPoly.ScalarFftDefs
+
+/-!
+# The precompiled native lane
+
+Root module of the `Zcash.FastFieldNative` library: the only `precompileModules` target in this
+repository.  It exists so that the shared library Lake emits
+(`.lake/build/lib/libZcash_Zcash_FastFieldNative.so`) carries an initializer whose name matches
+the library — Lean's dynlib loader derives the expected `initialize_…` symbol from the file name.
+
+The library name is namespaced rather than a bare `FastFieldNative`, which is what the
+CompElliptic pin calls its own precompiled lane.  Lean module names are global across the build,
+so two `FastFieldNative.lean` roots collide — and they collide *silently*: `lake build` stays
+green while Lake emits no ironwood shared object at all and `Zcash.Arithmetic.ScalarFftEquiv`
+is handed only the pin's plugin, leaving `ScalarFftDefs` interpreted.  A dotted `lean_lib` name
+works fine (the symbol becomes `initialize_Zcash_Zcash_FastFieldNative`) and keeps the two lanes
+distinguishable by construction.
+
+Its import closure is core-only by construction: the field definitions
+(`CompElliptic.Vendor.CompPoly.Montgomery.Native64x8Defs`), the Vesta point definitions
+(`CompElliptic.Curves.Pasta.Fast.ProjectiveMontDefs`) and the scalar FFT
+(`Zcash.Vendor.CompPoly.ScalarFftDefs`) import nothing beyond Lean core, so native compilation
+stays at a handful of modules instead of a mathlib closure.  The first two are natively
+compiled by the pin's own lane and only crossed into here; this library's glob covers just this
+root and `ScalarFftDefs`.
+-/
diff --git a/Zcash/Snark.lean b/Zcash/Snark.lean
index 4a839c445..02d31bcee 100644
--- a/Zcash/Snark.lean
+++ b/Zcash/Snark.lean
@@ -1,8 +1,11 @@
 -- The Orchard SNARK verifier: transcription and soundness.
 --
 -- Library layout:
--- * `Core/` — the shared objects: the scalar field `F_p`, the verifier group and URS, the typed
---   proof string, the challenges, and the fingerprint MSM.
+-- * `Core/` — the shared objects that are specific to the verifier: the typed proof string and
+--   the challenges. The arithmetic-tier objects the verifier is built from (the scalar field
+--   `F_p`, the verifier group and URS, the fingerprint MSM and its Pippenger accelerator) live
+--   one tier down, in `Zcash/Arithmetic/`; `Core.lean` is a one-name compatibility alias for
+--   the byte-locked fixture captures and nothing else.
 -- * `Verifier/` — the transcription layer: the deployed halo2 verifier's MSM assembly as a pure
 --   Lean function (queries, expressions, multiopen, IPA fold, Fiat–Shamir schedule).
 -- * `Fingerprint/` — the faithfulness cross-check: the captured-fixture match (`native_decide`,
@@ -13,11 +16,16 @@
 --
 -- Import modules here that should be built as part of the library.
 
-import Zcash.Snark.Core.Field
-import Zcash.Snark.Core.Group
+-- The arithmetic tier the verifier is stated over. The umbrella also re-exports `Fp` and `URS`
+-- at the `Zcash` root, which is how they resolve unqualified across the repository.
+import Zcash.Arithmetic
+import Zcash.Arithmetic.Msm
+import Zcash.Arithmetic.FastMsm
+-- The `Zcash.Snark`-namespace compatibility alias for the byte-locked fixture captures. Kept in
+-- the closure so the captures still elaborate; no editable module depends on it.
+import Zcash.Snark.Core
 import Zcash.Snark.Core.ProofString
 import Zcash.Snark.Core.Challenges
-import Zcash.Snark.Core.Msm
 import Zcash.Snark.Fingerprint.SchwartzZippel
 import Zcash.Snark.Fingerprint.Batch
 import Zcash.Snark.Verifier.Ipa
diff --git a/Zcash/Snark/Core.lean b/Zcash/Snark/Core.lean
new file mode 100644
index 000000000..123f66181
--- /dev/null
+++ b/Zcash/Snark/Core.lean
@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2026 Ironwood Contributors.
+Released under the Apache License, Version 2.0.
+-/
+import Zcash.Arithmetic.Msm
+
+/-!
+# Compatibility shim: `Msm` under `Zcash.Snark`
+
+The generated fixture captures spell the fingerprint MSM bare (`Msm shape.k Fp G`) while
+declaring inside `namespace Zcash.Snark.Fixture`, so the enclosing-namespace walk needs the name
+to exist at `Zcash.Snark`. It lives in `Zcash.Arithmetic.Msm` and is not common enough to earn
+root vocabulary the way `Fp` and `URS` do, so this one alias carries it. Delete this file when
+the captures are next regenerated; no editable module depends on it.
+-/
+
+namespace Zcash.Snark
+
+export Zcash.Arithmetic (Msm)
+
+end Zcash.Snark
diff --git a/Zcash/Snark/Fingerprint/Batch.lean b/Zcash/Snark/Fingerprint/Batch.lean
index 894e01565..00869d297 100644
--- a/Zcash/Snark/Fingerprint/Batch.lean
+++ b/Zcash/Snark/Fingerprint/Batch.lean
@@ -1,5 +1,5 @@
 import Mathlib
-import Zcash.Snark.Core.Field
+import Zcash.Arithmetic
 
 /-!
 # The batch random-linear-combination soundness bound
@@ -24,6 +24,8 @@ Requires `[NoZeroSMulDivisors Fp G]` — the prime-order property of the verifie
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (card_Fp scalarFieldOrder)
+
 open Finset
 
 variable {G : Type*} [AddCommGroup G] [Module Fp G]
diff --git a/Zcash/Snark/Fingerprint/Match.lean b/Zcash/Snark/Fingerprint/Match.lean
index 79c5a4bbe..c68c44c0e 100644
--- a/Zcash/Snark/Fingerprint/Match.lean
+++ b/Zcash/Snark/Fingerprint/Match.lean
@@ -1,5 +1,5 @@
 import Mathlib
-import Zcash.Snark.Core.Msm
+import Zcash.Arithmetic.Msm
 import Zcash.Snark.Fingerprint.SchwartzZippel
 import Zcash.Snark.Verifier.Assemble
 
@@ -44,6 +44,8 @@ fixture-generation boundary rather than being reimplemented in Lean.
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm scalarFieldOrder)
+
 /-- Two MSMs match iff their `g`/`w`/`u` coefficients are equal and their `other` term lists agree
 up to reordering (`List.Perm`) — term order is only a serialization artifact of how each assembler
 appends, and the term sum is order-independent (`msmMatch_eval`). -/
diff --git a/Zcash/Snark/Fingerprint/SchwartzZippel.lean b/Zcash/Snark/Fingerprint/SchwartzZippel.lean
index 80d2eb95b..d758335f5 100644
--- a/Zcash/Snark/Fingerprint/SchwartzZippel.lean
+++ b/Zcash/Snark/Fingerprint/SchwartzZippel.lean
@@ -1,5 +1,5 @@
 import Mathlib
-import Zcash.Snark.Core.Field
+import Zcash.Arithmetic
 
 /-!
 # The Schwartz–Zippel soundness bound for the fingerprint
@@ -19,6 +19,8 @@ fingerprint polynomial remains open; see `Zcash.Snark.Fingerprint.Match`.)
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (card_Fp scalarFieldOrder)
+
 open MvPolynomial Finset Fintype
 
 /-- **Schwartz–Zippel for the fingerprint field.** A nonzero polynomial `p` of total degree `d` in `n`
diff --git a/Zcash/Snark/Fixtures/MultiAction/Negative.lean b/Zcash/Snark/Fixtures/MultiAction/Negative.lean
index 61102261e..a7be83724 100644
--- a/Zcash/Snark/Fixtures/MultiAction/Negative.lean
+++ b/Zcash/Snark/Fixtures/MultiAction/Negative.lean
@@ -15,6 +15,7 @@ positive checks: the fingerprint match (`MsmMatch`) and the captured Fiat–Sham
 namespace Zcash.Snark.Fixture2
 
 open Zcash.Snark
+open Zcash.Arithmetic (Msm)
 
 theorem valid_capture_assembles : (assemble? vk derivedInstanceCommitment ps ch).isSome = true := by
   native_decide
diff --git a/Zcash/Snark/Fixtures/MultiAction/TrustBoundary.lean b/Zcash/Snark/Fixtures/MultiAction/TrustBoundary.lean
index 5e676e0af..52496969d 100644
--- a/Zcash/Snark/Fixtures/MultiAction/TrustBoundary.lean
+++ b/Zcash/Snark/Fixtures/MultiAction/TrustBoundary.lean
@@ -31,7 +31,7 @@ assert_axioms capturedInit_startsWith_vkTranscriptRepr +native
 assert_axioms fingerprint_matches +native
 assert_axioms capturedMsm_eval_eq_zero +native
 assert_axioms assembledMsm_eval_eq_zero +native
-assert_axioms Msm.evalNat
+assert_axioms Zcash.Arithmetic.Msm.evalNat
 assert_axioms assemble
 
 -- The instance-commitment derivation: the two captured claims, plus the data and functions they
diff --git a/Zcash/Snark/Fixtures/SingleAction/TrustBoundary.lean b/Zcash/Snark/Fixtures/SingleAction/TrustBoundary.lean
index 6ab97dc5c..78f1f8521 100644
--- a/Zcash/Snark/Fixtures/SingleAction/TrustBoundary.lean
+++ b/Zcash/Snark/Fixtures/SingleAction/TrustBoundary.lean
@@ -44,7 +44,7 @@ assert_axioms capturedPointCoordinatesValid_eq_true +native
 assert_axioms capturedInit_startsWith_vkTranscriptRepr +native
 assert_axioms capturedMsm_eval_eq_zero +native
 assert_axioms assembledMsm_eval_eq_zero +native
-assert_axioms Msm.evalNat
+assert_axioms Zcash.Arithmetic.Msm.evalNat
 assert_axioms assemble
 
 -- The instance-commitment derivation: the two captured claims, plus the data and functions they
diff --git a/Zcash/Snark/Soundness/AGM/ProbabilityVesta.lean b/Zcash/Snark/Soundness/AGM/ProbabilityVesta.lean
index 26f604406..dfdb23eb7 100644
--- a/Zcash/Snark/Soundness/AGM/ProbabilityVesta.lean
+++ b/Zcash/Snark/Soundness/AGM/ProbabilityVesta.lean
@@ -21,6 +21,8 @@ open scoped ENNReal
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (card_Fp)
+
 open CompElliptic.Curves.Pasta CompElliptic.CurveForms.ShortWeierstrass CompElliptic.CurveOrder
 
 /-- Run the computed opening-or-DL endpoint over Vesta. All transcript and AGM data are explicit. -/
diff --git a/Zcash/Snark/Soundness/Composition/Completeness.lean b/Zcash/Snark/Soundness/Composition/Completeness.lean
index d5e9b1c86..285e02ca5 100644
--- a/Zcash/Snark/Soundness/Composition/Completeness.lean
+++ b/Zcash/Snark/Soundness/Composition/Completeness.lean
@@ -37,6 +37,8 @@ by `deployed_member_budget`, the residual `hcont` pays for. -/
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm scalarFieldOrder)
+
 -- The deployed grouping definitions appear inside index types, so a defeq check on an index can
 -- pull the whole `constructIntermediateSets (assembleQueries …)` computation through `whnf`.
 -- Sealing them keeps those checks syntactic; the proofs below use their equation lemmas.
diff --git a/Zcash/Snark/Soundness/Constraints.lean b/Zcash/Snark/Soundness/Constraints.lean
index b5ea4aaf8..7d0c9f2f9 100644
--- a/Zcash/Snark/Soundness/Constraints.lean
+++ b/Zcash/Snark/Soundness/Constraints.lean
@@ -1,5 +1,5 @@
 import Mathlib
-import Zcash.Snark.Core.Field
+import Zcash.Arithmetic
 import Zcash.Snark.Verifier.Expressions
 import Zcash.Snark.Verifier.Assemble
 
@@ -35,6 +35,8 @@ on the full path covers gates, the permutation argument, and the lookup argument
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (scalarFieldOrder)
+
 open Polynomial Finset
 
 /-- The verifier's vanishing/quotient check at the challenge `x`: the claimed quotient `h` satisfies the
diff --git a/Zcash/Snark/Soundness/Deployed/ConcreteBounds.lean b/Zcash/Snark/Soundness/Deployed/ConcreteBounds.lean
index b23e0d09f..19d101f2f 100644
--- a/Zcash/Snark/Soundness/Deployed/ConcreteBounds.lean
+++ b/Zcash/Snark/Soundness/Deployed/ConcreteBounds.lean
@@ -1,4 +1,4 @@
-import Zcash.Snark.Core.Field
+import Zcash.Arithmetic
 import Zcash.Snark.Soundness.Forking.KnowledgeError
 
 /-!
@@ -21,6 +21,8 @@ module records what that floor evaluates to:
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (card_Fp scalarFieldOrder)
+
 open scoped ENNReal
 
 /-- **The deployed fork-tree knowledge error is exactly `3k/|F_p|`.** At any IPA depth `k` the
diff --git a/Zcash/Snark/Soundness/Deployed/Verification.lean b/Zcash/Snark/Soundness/Deployed/Verification.lean
index c9dea43b9..ce6274ad5 100644
--- a/Zcash/Snark/Soundness/Deployed/Verification.lean
+++ b/Zcash/Snark/Soundness/Deployed/Verification.lean
@@ -20,6 +20,8 @@ and ties that equation to the deployed accept condition:
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm Msm.zero)
+
 variable {F G : Type*} [Field F] [AddCommGroup G] [Module F G]
 
 omit [Field F] [AddCommGroup G] [Module F G] in
diff --git a/Zcash/Snark/Soundness/Forking/Adversary/Algebraic.lean b/Zcash/Snark/Soundness/Forking/Adversary/Algebraic.lean
index 8a4725731..2ac99da3a 100644
--- a/Zcash/Snark/Soundness/Forking/Adversary/Algebraic.lean
+++ b/Zcash/Snark/Soundness/Forking/Adversary/Algebraic.lean
@@ -14,6 +14,8 @@ reduction. Acceptance with an opening mismatch yields a relation.
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm Msm.zero)
+
 open scoped ENNReal
 
 local instance : Inhabited VestaG := ⟨0⟩
diff --git a/Zcash/Snark/Soundness/Forking/Adversary/Provenance.lean b/Zcash/Snark/Soundness/Forking/Adversary/Provenance.lean
index f1170105a..022a0067c 100644
--- a/Zcash/Snark/Soundness/Forking/Adversary/Provenance.lean
+++ b/Zcash/Snark/Soundness/Forking/Adversary/Provenance.lean
@@ -8,6 +8,8 @@ Every point appended by the deployed multiopen MSM comes from the proof or verif
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm)
+
 /-- The first component of a zipped pair is a member of the first list. -/
 private theorem mem_of_mem_zip_fst {α β : Type*} {a : α} {b : β}
     {l₁ : List α} {l₂ : List β} (h : (a, b) ∈ l₁.zip l₂) : a ∈ l₁ := by
@@ -27,19 +29,23 @@ section MsmPoints
 
 variable {k : ℕ} {F G : Type*}
 
+-- `Msm` lives in `Zcash.Arithmetic`, so these accessors have to be declared into its own
+-- namespace (`_root_.`) for generalized field notation to find them.
+
 /-- The group points an MSM's appended terms reference. -/
-def Msm.otherPoints (m : Msm k F G) : List G := m.other.map Prod.snd
+def _root_.Zcash.Arithmetic.Msm.otherPoints (m : Msm k F G) : List G := m.other.map Prod.snd
 
-theorem Msm.otherPoints_zero [Zero F] : (Msm.zero k F G).otherPoints = [] := rfl
+theorem _root_.Zcash.Arithmetic.Msm.otherPoints_zero [Zero F] :
+    (Msm.zero k F G).otherPoints = [] := rfl
 
-theorem Msm.otherPoints_appendTerm (c : F) (P : G) (m : Msm k F G) :
+theorem _root_.Zcash.Arithmetic.Msm.otherPoints_appendTerm (c : F) (P : G) (m : Msm k F G) :
     (m.appendTerm c P).otherPoints = P :: m.otherPoints := rfl
 
-theorem Msm.otherPoints_scale [Mul F] (c : F) (m : Msm k F G) :
+theorem _root_.Zcash.Arithmetic.Msm.otherPoints_scale [Mul F] (c : F) (m : Msm k F G) :
     (m.scale c).otherPoints = m.otherPoints := by
   simp [Msm.otherPoints, Msm.scale, List.map_map, Function.comp_def]
 
-theorem Msm.otherPoints_add [Add F] (m₁ m₂ : Msm k F G) :
+theorem _root_.Zcash.Arithmetic.Msm.otherPoints_add [Add F] (m₁ m₂ : Msm k F G) :
     (m₁.add m₂).otherPoints = m₁.otherPoints ++ m₂.otherPoints := by
   simp [Msm.otherPoints, Msm.add]
 
diff --git a/Zcash/Snark/Soundness/Forking/Oracle.lean b/Zcash/Snark/Soundness/Forking/Oracle.lean
index 9bd946eba..7750a6b8e 100644
--- a/Zcash/Snark/Soundness/Forking/Oracle.lean
+++ b/Zcash/Snark/Soundness/Forking/Oracle.lean
@@ -1,6 +1,6 @@
 import Mathlib.Probability.Distributions.Uniform
 import Zcash.Snark.Verifier.FiatShamir
-import Zcash.Snark.Core.Field
+import Zcash.Arithmetic
 
 /-!
 # Random-oracle model for Fiat–Shamir
diff --git a/Zcash/Snark/Soundness/InnerProduct.lean b/Zcash/Snark/Soundness/InnerProduct.lean
index 4209db4bf..e63b6f98d 100644
--- a/Zcash/Snark/Soundness/InnerProduct.lean
+++ b/Zcash/Snark/Soundness/InnerProduct.lean
@@ -1,5 +1,5 @@
 import Mathlib
-import Zcash.Snark.Core.Group
+import Zcash.Arithmetic
 
 /-!
 # Inner-product opening relation
diff --git a/Zcash/Snark/Soundness/KnowledgeSoundness.lean b/Zcash/Snark/Soundness/KnowledgeSoundness.lean
index 60b3bed52..a29fbf9be 100644
--- a/Zcash/Snark/Soundness/KnowledgeSoundness.lean
+++ b/Zcash/Snark/Soundness/KnowledgeSoundness.lean
@@ -22,6 +22,8 @@ and `2^k`. The fallback is `(2·|F|+1)^k`; adversary PPT time remains external.
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (scalarFieldOrder)
+
 open Polynomial
 
 variable {G : Type*} [AddCommGroup G] [Module Fp G]
diff --git a/Zcash/Snark/Soundness/Main.lean b/Zcash/Snark/Soundness/Main.lean
index 78bf65dac..7a3023430 100644
--- a/Zcash/Snark/Soundness/Main.lean
+++ b/Zcash/Snark/Soundness/Main.lean
@@ -48,6 +48,8 @@ This conditional family leaves those components opaque. The computed route is in
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm)
+
 variable {G : Type*} [AddCommGroup G] [Module Fp G]
 
 /-- Conditional interface: acceptance supplies a consistent transcript, IPA opening, and circuit
diff --git a/Zcash/Snark/Soundness/Multiopen/Compat.lean b/Zcash/Snark/Soundness/Multiopen/Compat.lean
index 50ba556ca..aba50b02e 100644
--- a/Zcash/Snark/Soundness/Multiopen/Compat.lean
+++ b/Zcash/Snark/Soundness/Multiopen/Compat.lean
@@ -20,8 +20,14 @@ decoded-column constraint bridges
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm)
+
 namespace Msm
 
+-- The MSM operations these lemmas are about live in `Zcash.Arithmetic.Msm`; this namespace only
+-- adds the evaluation spine lemmas the decode proofs need.
+open Zcash.Arithmetic.Msm (eval zero scale add)
+
 /-- The zero MSM evaluates to the group identity. -/
 theorem eval_zero {F G : Type*} [Field F] [AddCommGroup G] [Module F G] (urs : URS G) :
     (Msm.zero urs.k F G).eval urs = 0 := by
diff --git a/Zcash/Snark/Soundness/Multiopen/DecodeFixture.lean b/Zcash/Snark/Soundness/Multiopen/DecodeFixture.lean
index e0cb8ac72..4e3cb6ccc 100644
--- a/Zcash/Snark/Soundness/Multiopen/DecodeFixture.lean
+++ b/Zcash/Snark/Soundness/Multiopen/DecodeFixture.lean
@@ -41,6 +41,9 @@ challenge.
 -/
 
 namespace Zcash.Snark
+
+open Zcash.Arithmetic (Msm.zero)
+
 namespace MultiopenDecodeFixture
 
 open Polynomial
diff --git a/Zcash/Snark/Soundness/Multiopen/Deployed.lean b/Zcash/Snark/Soundness/Multiopen/Deployed.lean
index 99b3bd603..9c7f6d1bb 100644
--- a/Zcash/Snark/Soundness/Multiopen/Deployed.lean
+++ b/Zcash/Snark/Soundness/Multiopen/Deployed.lean
@@ -53,6 +53,8 @@ deployed-status section).
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm Msm.eval_appendTerm Msm.zero)
+
 /-! ## The scale-and-add fold in closed power form -/
 
 section PowerFold
diff --git a/Zcash/Snark/Soundness/Multiopen/NodeBinding.lean b/Zcash/Snark/Soundness/Multiopen/NodeBinding.lean
index 2a4d88e81..3fd120e22 100644
--- a/Zcash/Snark/Soundness/Multiopen/NodeBinding.lean
+++ b/Zcash/Snark/Soundness/Multiopen/NodeBinding.lean
@@ -30,6 +30,8 @@ end-to-end from the accept floors. The capstones consume that chain.
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm Msm.zero)
+
 -- The deployed grouping definitions appear inside index types, so a defeq check on an index can
 -- pull the whole `constructIntermediateSets (assembleQueries …)` computation through `whnf`.
 -- Sealing them keeps those checks syntactic; the proofs below use their equation lemmas.
diff --git a/Zcash/Snark/Soundness/Multiopen/Opened.lean b/Zcash/Snark/Soundness/Multiopen/Opened.lean
index 491bdf6b7..47147dbe9 100644
--- a/Zcash/Snark/Soundness/Multiopen/Opened.lean
+++ b/Zcash/Snark/Soundness/Multiopen/Opened.lean
@@ -58,6 +58,8 @@ evaluations at the original rotated points and the gate/`x`→`x₃` transport
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm.zero)
+
 -- The deployed grouping definitions appear inside index types (`Fin (deployedSetQueries …).length`),
 -- so every defeq check on an index invites `whnf` to unfold the whole
 -- `constructIntermediateSets (assembleQueries …)` computation. Sealing them keeps those checks
diff --git a/Zcash/Snark/Soundness/Vesta.lean b/Zcash/Snark/Soundness/Vesta.lean
index 7bcc17e5c..adf360cab 100644
--- a/Zcash/Snark/Soundness/Vesta.lean
+++ b/Zcash/Snark/Soundness/Vesta.lean
@@ -34,6 +34,8 @@ turns the curve into an `Fp`-module and the abstract theorems specialize to Vest
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm Msm.evalNat_eq_eval scalarFieldOrder)
+
 -- The deployed grouping definitions appear inside index types, so a defeq check on an index can
 -- pull the whole `constructIntermediateSets (assembleQueries …)` computation through `whnf`.
 -- Sealing them keeps those checks syntactic; the proofs below use their equation lemmas.
diff --git a/Zcash/Snark/Verifier/Assemble.lean b/Zcash/Snark/Verifier/Assemble.lean
index d47a09208..2f4d63cf4 100644
--- a/Zcash/Snark/Verifier/Assemble.lean
+++ b/Zcash/Snark/Verifier/Assemble.lean
@@ -32,6 +32,8 @@ instances) and bundled here for the assembly.
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm Msm.zero)
+
 /-- A permutation column's evaluation reference (halo2 `get_any_query_index` + `column_type`): the
 column's value is the advice / fixed / instance evaluation at the given query index. -/
 inductive ColumnRef where
diff --git a/Zcash/Snark/Verifier/Checks.lean b/Zcash/Snark/Verifier/Checks.lean
index 26d41bb9a..c2d6d1cce 100644
--- a/Zcash/Snark/Verifier/Checks.lean
+++ b/Zcash/Snark/Verifier/Checks.lean
@@ -1,5 +1,6 @@
 import Mathlib
-import Zcash.Snark.Core.Msm
+import Zcash.Arithmetic
+import Zcash.Arithmetic.Msm
 
 /-!
 # The verifier's MSM assembly
@@ -23,6 +24,8 @@ folds and the combined value `v`) is computed here.
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm Msm.zero)
+
 /-- A multiopen query's commitment reference (halo2 `CommitmentReference`): either a single group
 element, or an MSM — the vanishing argument's folded `h` commitment is supplied as an MSM. -/
 inductive CommitmentRef (k : ℕ) (F G : Type*) where
diff --git a/Zcash/Snark/Verifier/FiatShamir.lean b/Zcash/Snark/Verifier/FiatShamir.lean
index 31120c95f..b61e6ac94 100644
--- a/Zcash/Snark/Verifier/FiatShamir.lean
+++ b/Zcash/Snark/Verifier/FiatShamir.lean
@@ -19,6 +19,8 @@ field conversion with it is external. Fixtures use trusted typed captures, not t
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm)
+
 /-- A point, scalar, or challenge-domain marker written to the Fiat–Shamir transcript.
 
 The constructors correspond to halo2's three Blake2b domain prefixes. A squeeze absorbs `challenge`;
diff --git a/Zcash/Snark/Verifier/Ipa.lean b/Zcash/Snark/Verifier/Ipa.lean
index 2d4411a48..5ce8fec8a 100644
--- a/Zcash/Snark/Verifier/Ipa.lean
+++ b/Zcash/Snark/Verifier/Ipa.lean
@@ -1,5 +1,6 @@
 import Mathlib
-import Zcash.Snark.Core.Msm
+import Zcash.Arithmetic
+import Zcash.Arithmetic.Msm
 
 /-!
 # The inner-product-argument opening
@@ -20,6 +21,8 @@ separate equivalence proof.
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm Msm.eval_addToGScalars Msm.eval_addToUScalar Msm.eval_addToWScalar Msm.eval_appendTerm)
+
 /-- halo2 `compute_s`: the `2 ^ u.length` coefficients of `init · ∏ᵢ (1 + u_{k-1-i} · X^{2ⁱ})`.
 With `init = -c` these are the fingerprint's URS-generator coefficients for `[-c] G'`, where `G'`
 is the fully folded generator. Built by the same left-half doubling as the Rust. -/
diff --git a/Zcash/Snark/Verifier/Queries.lean b/Zcash/Snark/Verifier/Queries.lean
index 196ab0838..89a160fac 100644
--- a/Zcash/Snark/Verifier/Queries.lean
+++ b/Zcash/Snark/Verifier/Queries.lean
@@ -23,6 +23,8 @@ permutation, lookups; then shared: fixed, permutation-common, vanishing); that c
 
 namespace Zcash.Snark
 
+open Zcash.Arithmetic (Msm)
+
 /-- halo2 `domain.rotate_omega(x, Rotation(rot))`: the rotated evaluation point `x · ω^rot`, with `ω`
 the domain generator (VK-fixed). Negative rotations use the field's integer power. -/
 def rotateOmega {F : Type*} [Field F] (omega x : F) (rot : ℤ) : F := x * omega ^ rot
diff --git a/Zcash/Vendor/CompPoly/README.md b/Zcash/Vendor/CompPoly/README.md
new file mode 100644
index 000000000..eaac3649d
--- /dev/null
+++ b/Zcash/Vendor/CompPoly/README.md
@@ -0,0 +1,31 @@
+# Vendored CompPoly material (temporary)
+
+This directory holds code that is destined for **CompPoly** and lives here only until the
+ironwood pin can provide it. Nothing outside this directory should be added to it, and it
+must not import anything from the rest of ironwood.
+
+**Delete this directory** when ironwood's CompPoly pin moves past
+[CompPoly#274](https://github.com/…/CompPoly/pull/274) (the scalar FFT); the only changes
+needed then are the import paths.
+
+The eight-limb Montgomery field that used to be vendored here as `Montgomery/` now comes from
+the CompElliptic pin (`CompElliptic.Vendor.CompPoly.Montgomery.*`, same `Montgomery.Native64x8`
+namespaces), which vendors it on the same terms until CompPoly#258 lands.
+
+## `ScalarFftDefs.lean` — radix-2 DIT FFT over the scalar field
+
+Developed in ironwood, destined for **CompPoly#274**. It is the scalar twin of the group FFT
+that the CompElliptic pin used to carry: the same bit-reversal-plus-butterflies loop nest with
+the group operations replaced by eight-limb Montgomery field operations. Like the pin's
+`Native64x8Defs.lean` it is core-only, so it can sit in the `FastFieldNative` precompiled lane.
+Keep it that way — codegen runs over the whole import closure, and one mathlib-side import is
+what OOM-crashed a 16 GB box on 2026-07-24 (see the note in `/root/bin/lake-capped`). Its
+correctness proof is *not* here: it is mathlib-side and therefore ironwood-permanent, in
+`Zcash/Arithmetic/ScalarFftEquiv.lean`.
+
+The file is now upstream's text verbatim — CompPoly branch `fast_multilimb_fields`,
+`CompPoly/Fields/Montgomery/ScalarFft.lean`, namespace `Montgomery.ScalarFft`, generic over the
+modulus `(q, negInv)`. The only local edit is the import line, which points at the
+CompElliptic-vendored limb definitions instead of CompPoly's own; that is exactly the
+"import paths only" change the deletion criterion above promises. The monomorphization at the
+Vesta scalar field is *not* vendored: it is ironwood's `Zcash.Arithmetic.fftS`.
diff --git a/Zcash/Vendor/CompPoly/ScalarFftDefs.lean b/Zcash/Vendor/CompPoly/ScalarFftDefs.lean
new file mode 100644
index 000000000..e90d886ab
--- /dev/null
+++ b/Zcash/Vendor/CompPoly/ScalarFftDefs.lean
@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2026 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gregor Mitscha-Baude
+-/
+import CompElliptic.Vendor.CompPoly.Montgomery.Native64x8Defs
+
+/-
+Vendored **verbatim** from CompPoly branch `fast_multilimb_fields`
+(`CompPoly/Fields/Montgomery/ScalarFft.lean`); see `README.md` in this directory.
+
+The single edit is the import line: upstream imports its own
+`CompPoly.Fields.Montgomery.Native64x8Defs`, whereas on this branch the eight-limb definitions
+(same `Montgomery.Native64x8` namespace) arrive through the CompElliptic pin's vendored copy,
+`CompElliptic.Vendor.CompPoly.Montgomery.Native64x8Defs`. Everything below — including the
+`Montgomery.ScalarFft` namespace and the explicit `(q, negInv)` parameters — is upstream's text,
+so a pin bump that carries the scalar FFT is an import-line change only. The monomorphic entry
+point ironwood needs lives mathlib-side in `Zcash.Arithmetic.ScalarFftEquiv`.
+-/
+
+/-!
+# Radix-2 DIT FFT over eight-limb Montgomery elements (zero-import)
+
+An in-place radix-2 decimation-in-time FFT over `Limbs8` Montgomery residues: a bit-reversal
+permutation followed by `logN` rounds of butterflies against a precomputed Montgomery-form
+twiddle table.  Like the arithmetic in `CompPoly.Fields.Montgomery.Native64x8Defs`, the loop
+nest is generic over the modulus, taking `q` and `negInv` explicitly.
+
+As explained in `CompPoly.Fields.Montgomery.Native64x8Defs`, this module deliberately imports
+nothing beyond that (itself zero-import) module: downstream consumers put it into
+`precompileModules` native-compilation lanes, and `precompileModules` compiles the
+entire import closure — so the runtime definitions must not pull in mathlib.
+
+This module contains runtime definitions only; correctness specifications live downstream
+for now.
+-/
+
+namespace Montgomery
+namespace ScalarFft
+
+open Native64x8 (Limbs8 add sub mul)
+
+/-- Bit-reversal permutation index. -/
+def bitreverse (n l : Nat) : Nat := Id.run do
+  let mut r := 0
+  let mut m := n
+  for _ in [0:l] do
+    r := (r <<< 1) ||| (m &&& 1)
+    m := m >>> 1
+  return r
+
+/-- In-place radix-2 DIT FFT over eight-limb Montgomery residues modulo `q`: bit-reversal
+permutation, then `logN` rounds of butterflies against the Montgomery-form twiddles `tw`. -/
+def fft (q : Limbs8) (negInv : UInt64) (a0 : Array Limbs8) (tw : Array Limbs8)
+    (logN : Nat) : Array Limbs8 := Id.run do
+  let n := a0.size
+  let mut a := a0
+  for k in [0:n] do
+    let rk := bitreverse k logN
+    if k < rk then
+      let ak := a[k]!
+      let ark := a[rk]!
+      a := (a.set! k ark).set! rk ak
+  let mut half := 1
+  for _ in [0:logN] do
+    let chunk := 2 * half
+    let twiddleChunk := n / chunk
+    for c in [0:n / chunk] do
+      let s := c * chunk
+      for j in [0:half] do
+        let twdl := tw[j * twiddleChunk]!
+        let aIdx := s + j
+        let bIdx := s + half + j
+        let aOld := a[aIdx]!
+        let t := mul q negInv twdl a[bIdx]!
+        a := a.set! aIdx (add q aOld t)
+        a := a.set! bIdx (sub q aOld t)
+    half := chunk
+  return a
+
+end ScalarFft
+end Montgomery
diff --git a/_typos.toml b/_typos.toml
index 579417a6e..537bac01f 100644
--- a/_typos.toml
+++ b/_typos.toml
@@ -28,4 +28,5 @@ extend-ignore-identifiers-re = [
 advices = "advices"
 thr = "thr"  # threshold identifiers (`thr`, `thr1`, `thr4`) in Composition/Completeness
 hsi = "hsi"  # hypothesis identifiers (`hsiN`) in Verifier/Assemble
+padd = "padd"  # projective point addition (`padd`) in Vendor/CompElliptic and Arithmetic
 Hom = "Hom"  # `RingHom`, `evalRingHom` — Mathlib's homomorphism naming
diff --git a/lake-manifest.json b/lake-manifest.json
index 458a047e2..f66f23d80 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,10 +15,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a549e4555b17bbbe3c8d48aa7d5b493912ccfbe9",
+   "rev": "fd9977340d728b704436894f87f9967f117ad5f7",
    "name": "CompElliptic",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "a549e4555b17bbbe3c8d48aa7d5b493912ccfbe9",
+   "inputRev": "fd9977340d728b704436894f87f9967f117ad5f7",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/Verified-zkEVM/clean",
diff --git a/lakefile.toml b/lakefile.toml
index ea9810c84..b01a12784 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,7 +1,7 @@
 name = "Zcash"
 version = "0.1.0"
 keywords = ["cryptography", "math", "protocols"]
-defaultTargets = ["Zcash", "FixtureCheck"]
+defaultTargets = ["Zcash", "FixtureCheck", "Arithmetic"]
 
 [leanOptions]
 pp.unicode.fun = true # pretty-prints `fun a ↦ b`
@@ -15,7 +15,7 @@ rev = "fca63dc777ca9de7f533a50196cdd1357d569f4f"
 [[require]]
 name = "CompElliptic"
 git = "https://github.com/daira/CompElliptic"
-rev = "a549e4555b17bbbe3c8d48aa7d5b493912ccfbe9"
+rev = "fd9977340d728b704436894f87f9967f117ad5f7"
 
 # mathlib last, so that its pinned versions of the common transitive dependencies
 # (batteries, aesop, Qq, proofwidgets, ...) take precedence over CompPoly's.
@@ -39,3 +39,42 @@ name = "Zcash"
 [[lean_lib]]
 name = "FixtureCheck"
 globs = ["Zcash.Snark.Fixtures.+"]
+
+# The fast Pasta arithmetic: the umbrella root `Zcash/Arithmetic.lean` (which re-exports `Fp`
+# and `URS` at the `Zcash` root), the tree below it (ironwood-permanent, mathlib-side), and the
+# remaining temporary vendoring `Zcash/Vendor/CompPoly/` (the scalar FFT definitions), whose
+# README states its deletion criteria. Only part of these trees is reachable from the `Zcash`
+# library (`Zcash.Arithmetic.CommitLagrange` and `Zcash.Arithmetic.ScalarFftEquiv` have no
+# importer at all), so without a target of their own the unreached modules would silently stop
+# being compiled and warning-checked. In `defaultTargets`
+# so plain `lake build` -- what CI runs -- keeps every module honest.
+[[lean_lib]]
+name = "Arithmetic"
+globs = ["Zcash.Arithmetic", "Zcash.Arithmetic.+", "Zcash.Vendor.CompPoly.+"]
+
+# The ONLY library in this repo with `precompileModules`. It is a core-only leaf: its modules
+# import nothing beyond Lean core, so native compilation covers a couple of files rather than a
+# mathlib import closure -- the latter is what OOM-crashed a 16 GB box on 2026-07-24. The field
+# and Vesta-point definitions now come from the CompElliptic pin's own precompiled
+# `FastFieldNative` lane; only the scalar FFT is still local. Everything mathlib-side about
+# these definitions lives in `Zcash/Arithmetic/`, which is NOT in this lane.
+#
+# `Zcash.FastFieldNative` must keep a root module of the same name
+# (`Zcash/FastFieldNative.lean`): Lean derives the dynlib's expected `initialize_…` symbol from
+# the shared object's file name, and without a matching module every importer fails with
+# `error loading plugin, initializer not found`.
+#
+# The name may NOT be a bare `FastFieldNative`, which is what the CompElliptic pin calls its own
+# precompiled lane. Lean module names are global across the build, so two `FastFieldNative.lean`
+# roots collide -- and they collide *silently*: `lake build` stays green, but Lake never emits
+# ironwood's shared object and `Zcash.Arithmetic.ScalarFftEquiv` is handed only the pin's
+# plugin, so `ScalarFftDefs` runs interpreted. A dotted `lean_lib` name is enough to keep them
+# apart; it yields `libZcash_Zcash_FastFieldNative.so`. Note this module is NOT in the `Zcash`
+# library: that lib's default glob is its root module alone, so the native lane stays a leaf.
+[[lean_lib]]
+name = "Zcash.FastFieldNative"
+precompileModules = true
+globs = [
+  "Zcash.FastFieldNative",
+  "Zcash.Vendor.CompPoly.ScalarFftDefs",
+]