diff --git a/CompElliptic/CurveForms/ShortWeierstrass.lean b/CompElliptic/CurveForms/ShortWeierstrass.lean
index 180ed93..84a2ab6 100644
--- a/CompElliptic/CurveForms/ShortWeierstrass.lean
+++ b/CompElliptic/CurveForms/ShortWeierstrass.lean
@@ -60,6 +60,18 @@ theorem not_onCurve_zero {a b : F} (hb : b ≠ 0) : ¬ OnCurve a b (0, 0) := by
   have h' : (0 : F) ^ 2 = (0 : F) ^ 3 + a * 0 + b := h
   simpa using h'.symm
 
+omit [DecidableEq F] in
+/-- Two points on the curve sharing an `x`-coordinate have `y`-coordinates equal up to sign,
+because their curve equations subtract to `(y₁ - y₂)·(y₁ + y₂) = 0`. -/
+theorem y_eq_pm_of_onCurve_x_eq {a b x y₁ y₂ : F}
+    (h₁ : OnCurve a b (x, y₁)) (h₂ : OnCurve a b (x, y₂)) : y₁ = y₂ ∨ y₁ = -y₂ := by
+  have h : (y₁ - y₂) * (y₁ + y₂) = 0 := by
+    simp only [OnCurve] at h₁ h₂
+    linear_combination h₁ - h₂
+  rcases mul_eq_zero.mp h with h | h
+  · exact Or.inl (sub_eq_zero.mp h)
+  · exact Or.inr (by linear_combination h)
+
 /-- Negation `(x, y) ↦ (x, -y)`; fixes the `(0, 0)` sentinel. -/
 def neg (p : F × F) : F × F := (p.1, -p.2)
 
@@ -426,6 +438,36 @@ omit [DecidableEq F] in
 /-- Negation negates the `y`-coordinate — the one fact that makes `2 • P = 0` say `P.y = -P.y`. -/
 @[simp] theorem SWPoint.neg_y {E : SWCurve F} (P : SWPoint E) : (-P).y = -P.y := rfl
 
+/-- Addition computes its `x`-coordinate by the raw `add` on the coordinate pairs. -/
+lemma SWPoint.add_x {E : SWCurve F} (P Q : SWPoint E) :
+    (P + Q).x = (add E.A (P.x, P.y) (Q.x, Q.y)).1 := rfl
+
+/-- Addition computes its `y`-coordinate by the raw `add` on the coordinate pairs. -/
+lemma SWPoint.add_y {E : SWCurve F} (P Q : SWPoint E) :
+    (P + Q).y = (add E.A (P.x, P.y) (Q.x, Q.y)).2 := rfl
+
+omit [DecidableEq F] in
+/-- A nonzero representable point is on the curve: its `Valid` disjunction cannot be the `(0, 0)`
+sentinel. -/
+theorem SWPoint.onCurve_of_ne_zero {E : SWCurve F} {P : SWPoint E} (h : P ≠ 0) :
+    OnCurve E.A E.B (P.x, P.y) := by
+  rcases P.onCurve with hc | h0
+  · exact hc
+  · exact absurd (SWPoint.ext_pair (by rw [h0]; rfl)) h
+
+omit [DecidableEq F] in
+/-- Nonzero representable points sharing an `x`-coordinate are equal up to sign: both are on the
+curve (`onCurve_of_ne_zero`), so their `y`-coordinates agree up to sign
+(`y_eq_pm_of_onCurve_x_eq`). -/
+theorem SWPoint.eq_pm_of_x_eq {E : SWCurve F} {P Q : SWPoint E}
+    (hP : P ≠ 0) (hQ : Q ≠ 0) (hx : P.x = Q.x) : P = Q ∨ P = -Q := by
+  have hPC := onCurve_of_ne_zero hP
+  have hQC := onCurve_of_ne_zero hQ
+  rw [hx] at hPC
+  rcases y_eq_pm_of_onCurve_x_eq hPC hQC with hy | hy
+  · exact Or.inl (ext_pair (by rw [hx, hy]))
+  · exact Or.inr (ext_pair (by rw [hx, hy]; rfl))
+
 /-! ### Fast (logarithmic) scalar multiplication
 
 The spec-level `smul` is linear (`n` additions), so it cannot be evaluated by `decide` or
diff --git a/CompElliptic/Fields/Pasta.lean b/CompElliptic/Fields/Pasta.lean
index d0ea181..4bcdc89 100644
--- a/CompElliptic/Fields/Pasta.lean
+++ b/CompElliptic/Fields/Pasta.lean
@@ -166,6 +166,11 @@ abbrev VestaBaseField := PallasScalarField
 /-- Vesta scalar field = Pallas base field. -/
 abbrev VestaScalarField := PallasBaseField
 
+/-- The Pallas base field (= the Vesta scalar field), under its `pasta_curves` letter. -/
+abbrev Fp := PallasBaseField
+/-- The Pallas scalar field (= the Vesta base field), under its `pasta_curves` letter. -/
+abbrev Fq := PallasScalarField
+
 /-- Tonelli–Shanks data for the Pallas base field `𝔽ₚ`: `p-1 = 2^32 · T`, with `rootOfUnity = 5ᵀ`
 (`pallas.py`). -/
 def pallasBase : TonelliShanks PallasBaseField where
diff --git a/CompElliptic/Hashing/FibreBound.lean b/CompElliptic/Hashing/FibreBound.lean
new file mode 100644
index 0000000..95331cd
--- /dev/null
+++ b/CompElliptic/Hashing/FibreBound.lean
@@ -0,0 +1,221 @@
+/-
+Copyright (c) 2026 CompElliptic Contributors.
+Released under the Apache License, Version 2.0, or the MIT license, at your option,
+as described in the files LICENSE-APACHE and LICENSE-MIT.
+Authors: Daira-Emma Hopwood
+-/
+import CompElliptic.Hashing.SimplifiedSWU
+import Mathlib.Algebra.Polynomial.Roots
+import Mathlib.Tactic.ComputeDegree
+
+/-!
+# Fibre bounds for the simplified SWU mapping
+
+Away from the input `u = 0`, every point of the target curve has at most 10
+preimages under `SSWUParams.map`. This is the counting fact the
+indifferentiability arc's rejection sampler consumes (zcash/ironwood#198,
+CompElliptic#25): to sample a uniform preimage of a point under the deployed
+two-term construction, the sampler needs each single-term fibre to be
+computable and small; smallness is what makes its acceptance probability an
+explicit constant. The input `u = 0` is excluded rather than counted: the
+probability analysis already carries a negligible correction for pairs
+containing `0` (the deployed-vs-zero-repaired transport), and the sampler
+rides the same correction.
+
+The bound is by abscissa, and the argument is elementary root counting. On a
+field where `-1` is a square (both Pasta base fields, `q ≡ 1 (mod 4)`), a
+nonzero input is never exceptional: `ta = t² + t = 0` forces `t = 0` (which
+is `u = 0`) or `t = -1` (which would make `-1/Z = u²` a square against `Z`
+nonsquare). So a nonzero preimage `u` of a point with abscissa `x` satisfies
+`xnum/xdiv = x`, where `xnum` is one of the two branch numerators and the
+denominator is `xdiv = A·(-ta)`. Clearing the denominator turns membership
+in *either* branch into the vanishing of the product polynomial
+
+`Φ_x(u) = (x·(-A·ta) - x1num) · (x·(-A·ta) - x2num)`.
+
+This is an explicit polynomial in `u` through `t = Z·u²`. Its second factor has
+degree exactly 6 with leading coefficient `-B·Z³ ≠ 0`, so `Φ_x` is a nonzero
+polynomial of degree at most 10, and has at most 10 roots.
+
+The constant is deliberately crude; the proof stays at the level of one
+product polynomial. The optimal constant is 4: each branch equation is a
+quadratic in `t`, and oddness pairs `±u` across `P` and `-P` (which are
+distinct — the target curves have no 2-torsion), so each `t` contributes one
+preimage. Tightening to that constant is a planned follow-up.
+-/
+
+namespace CompElliptic.Hashing
+
+open Finset Polynomial CompElliptic.CurveForms.ShortWeierstrass
+
+namespace SSWUParams
+
+variable {F : Type*} [Field F] [Fintype F] [DecidableEq F]
+
+/-- The polynomial `t = Z·u²`, as a polynomial in `u`. -/
+noncomputable def tPoly (G : SSWUParams F) : Polynomial F := C G.Z * X^2
+
+/-- The polynomial `ta = t² + t`, as a polynomial in `u`. -/
+noncomputable def taPoly (G : SSWUParams F) : Polynomial F :=
+  G.tPoly^2 + G.tPoly
+
+/-- The abscissa-fibre polynomial `Φ_x`: away from `u = 0`, a preimage of
+abscissa `x` under either branch is a root. The first factor is the branch-1
+equation `x·(-A·ta) = x1num`, the second the branch-2 equation
+`x·(-A·ta) = x2num`, both cleared of the denominator `xdiv = A·(-ta)`. -/
+noncomputable def fibrePoly (G : SSWUParams F) (x : F) : Polynomial F :=
+  (C x * (-(C G.E.A) * G.taPoly) - C G.E.B * (G.taPoly + 1)) *
+    (C x * (-(C G.E.A) * G.taPoly) - G.tPoly * (C G.E.B * (G.taPoly + 1)))
+
+/-- The second factor of `Φ_x` has degree exactly 6, because its leading
+coefficient `-B·Z³` does not vanish for any `x`. -/
+theorem fibrePoly_snd_natDegree (G : SSWUParams F) (x : F) :
+    (C x * (-(C G.E.A) * G.taPoly)
+      - G.tPoly * (C G.E.B * (G.taPoly + 1))).natDegree = 6 := by
+  rw [taPoly, tPoly]
+  compute_degree!
+  exact ⟨G.Z_nonzero, G.E.B_nonzero, G.Z_nonzero⟩
+
+/-- The second factor of `Φ_x` is nonzero, because it has degree 6. -/
+theorem fibrePoly_snd_ne_zero (G : SSWUParams F) (x : F) :
+    C x * (-(C G.E.A) * G.taPoly)
+      - G.tPoly * (C G.E.B * (G.taPoly + 1)) ≠ 0 := by
+  intro h
+  have hdeg := G.fibrePoly_snd_natDegree x
+  rw [h, natDegree_zero] at hdeg
+  exact absurd hdeg (by norm_num)
+
+/-- The first factor of `Φ_x` is nonzero, because it either has degree 4
+(when `A·x + B ≠ 0`) or is the nonzero constant `-B`. -/
+theorem fibrePoly_fst_ne_zero (G : SSWUParams F) (x : F) :
+    C x * (-(C G.E.A) * G.taPoly) - C G.E.B * (G.taPoly + 1) ≠ 0 := by
+  have hexpand : C x * (-(C G.E.A) * G.taPoly) - C G.E.B * (G.taPoly + 1)
+      = -(C (G.E.A * x + G.E.B)) * G.taPoly - C G.E.B := by
+    rw [map_add, map_mul]
+    ring
+  rw [hexpand]
+  intro h
+  by_cases hAB : G.E.A * x + G.E.B = 0
+  · rw [hAB, map_zero, neg_zero, zero_mul, zero_sub, neg_eq_zero,
+      C_eq_zero] at h
+    exact G.E.B_nonzero h
+  · have hdeg : (-(C (G.E.A * x + G.E.B)) * G.taPoly - C G.E.B).natDegree
+        = 4 := by
+      rw [taPoly, tPoly]
+      compute_degree!
+      refine ⟨fun hc => hAB ?_, G.Z_nonzero⟩
+      linear_combination -hc
+    rw [h, natDegree_zero] at hdeg
+    exact absurd hdeg (by norm_num)
+
+/-- `Φ_x` is nonzero, because both its factors are. -/
+theorem fibrePoly_ne_zero (G : SSWUParams F) (x : F) : G.fibrePoly x ≠ 0 :=
+  mul_ne_zero (G.fibrePoly_fst_ne_zero x) (G.fibrePoly_snd_ne_zero x)
+
+theorem fibrePoly_natDegree_le (G : SSWUParams F) (x : F) :
+    (G.fibrePoly x).natDegree ≤ 10 := by
+  refine natDegree_mul_le.trans ?_
+  have h1 : (C x * (-(C G.E.A) * G.taPoly)
+      - C G.E.B * (G.taPoly + 1)).natDegree ≤ 4 := by
+    rw [taPoly, tPoly]
+    compute_degree
+  have h2 := (G.fibrePoly_snd_natDegree x).le
+  omega
+
+/-- Away from `u = 0`, a preimage of abscissa `x` is a root of `Φ_x`. The
+denominator is `A·(-ta)` with `ta ≠ 0`, and whichever branch the square-root
+split took, the corresponding factor of `Φ_x` vanishes. -/
+theorem eval_fibrePoly_eq_zero (G : SSWUParams F) {x u : F}
+    (hta : (G.Z * u^2)^2 + G.Z * u^2 ≠ 0)
+    (hx : (G.mapXYUpToSign u).1 = x) :
+    (G.fibrePoly x).eval u = 0 := by
+  have heval_t : G.tPoly.eval u = G.Z * u^2 := by
+    simp [tPoly]
+  have heval_ta : G.taPoly.eval u = (G.Z * u^2)^2 + G.Z * u^2 := by
+    simp [taPoly, tPoly]
+  simp only [mapXYUpToSign] at hx
+  rw [if_neg hta] at hx
+  have hxdiv : G.E.A * -((G.Z * u^2)^2 + G.Z * u^2) ≠ 0 :=
+    mul_ne_zero G.A_nonzero (neg_ne_zero.mpr hta)
+  rw [div_eq_iff hxdiv] at hx
+  rw [fibrePoly, eval_mul]
+  split_ifs at hx with hsr
+  · apply mul_eq_zero_of_left
+    simp only [eval_sub, eval_mul, eval_neg, eval_C, eval_add, eval_one,
+      heval_ta]
+    linear_combination -hx
+  · apply mul_eq_zero_of_right
+    simp only [eval_sub, eval_mul, eval_neg, eval_C, eval_add, eval_one,
+      heval_ta, heval_t]
+    linear_combination -hx
+
+/-- A nonzero input is never exceptional when `-1` is a square, because
+`ta = 0` forces `t = 0` (that is, `u = 0`) or `t = -1`, and the latter would
+exhibit the nonsquare `Z` as `-1` times a square of an inverse. -/
+theorem ta_ne_zero_of_u_ne_zero (G : SSWUParams F) (hsq : IsSquare (-1 : F)) {u : F}
+    (hu : u ≠ 0) : (G.Z * u^2)^2 + G.Z * u^2 ≠ 0 := by
+  intro h
+  have hfac : G.Z * u^2 * (G.Z * u^2 + 1) = 0 := by linear_combination h
+  rcases mul_eq_zero.mp hfac with h0 | h1
+  · rcases mul_eq_zero.mp h0 with hZ | hu2
+    · exact G.Z_nonzero hZ
+    · exact hu (sq_eq_zero_iff.mp hu2)
+  · obtain ⟨s, hs⟩ := hsq
+    have hZu : G.Z * u^2 = -1 := by linear_combination h1
+    refine G.Z_nonsquare ⟨s/u, ?_⟩
+    rw [div_mul_div_comm, show u*u = u^2 from (pow_two u).symm]
+    exact (eq_div_iff (pow_ne_zero 2 hu)).mpr (hZu.trans hs)
+
+/-- **At most 10 nonzero preimages per abscissa.** On a field where `-1` is
+a square, every nonzero preimage is a root of the degree-≤10 polynomial
+`Φ_x`. -/
+theorem card_abscissaFibre_le (G : SSWUParams F) (hsq : IsSquare (-1 : F))
+    (x : F) :
+    (univ.filter fun u => u ≠ 0 ∧ (G.mapXYUpToSign u).1 = x).card ≤ 10 := by
+  have hsub : univ.filter (fun u => u ≠ 0 ∧ (G.mapXYUpToSign u).1 = x)
+      ⊆ (G.fibrePoly x).roots.toFinset := by
+    intro u hu
+    rw [mem_filter] at hu
+    rw [Multiset.mem_toFinset, mem_roots (G.fibrePoly_ne_zero x)]
+    exact G.eval_fibrePoly_eq_zero (G.ta_ne_zero_of_u_ne_zero hsq hu.2.1) hu.2.2
+  calc (univ.filter fun u => u ≠ 0 ∧ (G.mapXYUpToSign u).1 = x).card
+      ≤ (G.fibrePoly x).roots.toFinset.card := Finset.card_le_card hsub
+    _ ≤ (G.fibrePoly x).roots.card := Multiset.toFinset_card_le _
+    _ ≤ (G.fibrePoly x).natDegree := (G.fibrePoly x).card_roots'
+    _ ≤ 10 := G.fibrePoly_natDegree_le x
+
+/-- **At most 10 nonzero preimages per point** under the simplified SWU
+mapping. A preimage of `P` is in particular a preimage of its abscissa. The
+optimal constant is 4 (a planned follow-up); the input `u = 0` is excluded,
+priced by the probability analysis's existing zero-pair correction. -/
+theorem card_map_fibre_le (G : SSWUParams F) (hsq : IsSquare (-1 : F))
+    (P : SWPoint G.E) :
+    (univ.filter fun u => u ≠ 0 ∧ G.map u = P).card ≤ 10 := by
+  refine (Finset.card_le_card ?_).trans (G.card_abscissaFibre_le hsq P.x)
+  intro u hu
+  rw [mem_filter] at hu ⊢
+  exact ⟨mem_univ u, hu.2.1,
+    by rw [show (G.mapXYUpToSign u).1 = (G.map u).x from rfl, hu.2.2]⟩
+
+end SSWUParams
+
+/-- Composing with an injective map does not grow fibres: a fibre bound for
+`f` is a fibre bound for `g ∘ f`. Stated with the auxiliary predicate that
+the fibre-bound statements carry. -/
+theorem card_fibre_comp_le {α β γ : Type*} [Fintype α] [DecidableEq β]
+    [DecidableEq γ] {f : α → β} {g : β → γ} (hg : Function.Injective g)
+    {pred : α → Prop} [DecidablePred pred] {n : ℕ}
+    (h : ∀ Q : β, (univ.filter fun u => pred u ∧ f u = Q).card ≤ n)
+    (P : γ) :
+    (univ.filter fun u => pred u ∧ g (f u) = P).card ≤ n := by
+  rcases (univ.filter fun u => pred u ∧ g (f u) = P).eq_empty_or_nonempty
+    with he | ⟨u₀, hu₀⟩
+  · rw [he, Finset.card_empty]
+    exact Nat.zero_le n
+  · rw [mem_filter] at hu₀
+    refine (Finset.card_le_card ?_).trans (h (f u₀))
+    intro u hu
+    rw [mem_filter] at hu ⊢
+    exact ⟨mem_univ u, hu.2.1, hg (hu.2.2.trans hu₀.2.2.symm)⟩
+
+end CompElliptic.Hashing
diff --git a/CompElliptic/Hashing/PastaSSWU.lean b/CompElliptic/Hashing/PastaSSWU.lean
index b90a1a1..fa2b28b 100644
--- a/CompElliptic/Hashing/PastaSSWU.lean
+++ b/CompElliptic/Hashing/PastaSSWU.lean
@@ -9,6 +9,7 @@ import CompElliptic.Isogenies.Homomorphism
 import CompElliptic.Curves.PastaOrder
 import CompElliptic.Hashing.SimplifiedSWU
 import CompElliptic.Hashing.SignedLift
+import CompElliptic.Hashing.FibreBound
 import Mathlib.Tactic.ReduceModChar
 
 /-!
@@ -71,6 +72,12 @@ theorem neg_thirteen_not_isSquare : ¬ IsSquare (-13 : PallasBaseField) := by
   reduce_mod_char
   decide
 
+/-- `-1` is a square in the Pallas base field (`q ≡ 1 (mod 4)`), by Euler's
+criterion with the power evaluated by fast modular exponentiation. -/
+theorem isSquare_neg_one : IsSquare (-1 : PallasBaseField) := by
+  rw [ZMod.euler_criterion PALLAS_BASE_CARD (by decide : (-1 : PallasBaseField) ≠ 0)]
+  reduce_mod_char
+
 /-- The precomputed resolvent root for RFC 9380's criterion 3 on iso-Pallas is not
 a cube, by `not_exists_pow_eq_of_pow_ne_one` with the power evaluated by fast
 modular exponentiation, as for `neg_five_not_isCube`. -/
@@ -153,6 +160,15 @@ character-sum analysis consumes. -/
 theorem isOdd_zeroRepaired_mapToCurve : IsOdd (zeroRepaired mapToCurve) :=
   isOdd_zeroRepaired fun _ hu => mapToCurve_neg hu
 
+/-- **At most 10 nonzero preimages per point** under the deployed
+`mapToCurve`. The isogeny is injective on rational points, so the SSWU fibre
+bound carries over. This is the counting interface for the
+indifferentiability sampler (zcash/ironwood#198). -/
+theorem card_mapToCurve_fibre_le (P : SWPoint curve) :
+    (Finset.univ.filter fun u => u ≠ 0 ∧ mapToCurve u = P).card ≤ 10 :=
+  card_fibre_comp_le iso_map_bijective.injective
+    (fun Q => sswu.card_map_fibre_le isSquare_neg_one Q) P
+
 /-- The zero-repair transport, composed at the deployed mapping: for every
 character, the deployed and repaired character sums differ by exactly
 `ψ (mapToCurve 0) - 1`. Conclusions about the literally-odd
@@ -248,6 +264,12 @@ theorem neg_thirteen_not_isSquare : ¬ IsSquare (-13 : VestaBaseField) := by
   reduce_mod_char
   decide
 
+/-- `-1` is a square in the Vesta base field (`q ≡ 1 (mod 4)`), by Euler's
+criterion with the power evaluated by fast modular exponentiation. -/
+theorem isSquare_neg_one : IsSquare (-1 : VestaBaseField) := by
+  rw [ZMod.euler_criterion PALLAS_SCALAR_CARD (by decide : (-1 : VestaBaseField) ≠ 0)]
+  reduce_mod_char
+
 /-- The precomputed resolvent root for RFC 9380's criterion 3 on iso-Vesta is not
 a cube, by `not_exists_pow_eq_of_pow_ne_one` with the power evaluated by fast
 modular exponentiation, as for `neg_five_not_isCube`. -/
@@ -325,6 +347,15 @@ character-sum analysis consumes. -/
 theorem isOdd_zeroRepaired_mapToCurve : IsOdd (zeroRepaired mapToCurve) :=
   isOdd_zeroRepaired fun _ hu => mapToCurve_neg hu
 
+/-- **At most 10 nonzero preimages per point** under the deployed
+`mapToCurve`. The isogeny is injective on rational points, so the SSWU fibre
+bound carries over. This is the counting interface for the
+indifferentiability sampler (zcash/ironwood#198). -/
+theorem card_mapToCurve_fibre_le (P : SWPoint curve) :
+    (Finset.univ.filter fun u => u ≠ 0 ∧ mapToCurve u = P).card ≤ 10 :=
+  card_fibre_comp_le iso_map_bijective.injective
+    (fun Q => sswu.card_map_fibre_le isSquare_neg_one Q) P
+
 /-- The zero-repair transport, composed at the deployed mapping: for every
 character, the deployed and repaired character sums differ by exactly
 `ψ (mapToCurve 0) - 1`. Conclusions about the literally-odd
diff --git a/CompElliptic/Hashing/TwoTermUniformity.lean b/CompElliptic/Hashing/TwoTermUniformity.lean
index a3c08a8..89854c4 100644
--- a/CompElliptic/Hashing/TwoTermUniformity.lean
+++ b/CompElliptic/Hashing/TwoTermUniformity.lean
@@ -376,4 +376,190 @@ theorem sq_sum_abs_prob_dev_le [Nonempty F] (f : F → G) {C : ℝ}
     _ = ((Fintype.card G : ℝ) - 1) * C^4
           * ((Fintype.card G : ℝ) * (Fintype.card F : ℝ)^2)^2 := by ring
 
+
+/-! ## Exports for the indifferentiability arc
+
+The game-side consumer (zcash/ironwood#198) works in `ℝ≥0∞` and should never
+need a square root. `sum_abs_prob_dev_le` states the L¹ bound against any
+budget `ε` whose square dominates the squared bound, so a concrete `ε` is
+checked by squaring, in exact arithmetic. `card_dev_ge_le` is the
+Chebyshev-style counting form of the L² bound: regularity does not
+lower-bound individual fibres, so the rejection sampler's acceptance
+constant holds only outside a bad set of fibres, whose size this bounds.
+`sum_abs_pairCount_sub_le` prices replacing the zero-repaired mapping by the
+deployed one: the two mappings differ at the single input `0`, so their
+two-term pair counts differ only on pairs containing it. -/
+
+/-- The L¹ probability deviation, unsquared, against an arbitrary budget: if
+`ε²` dominates the squared bound then the deviation is at most `ε`. -/
+theorem sum_abs_prob_dev_le [Nonempty F] (f : F → G) {C : ℝ}
+    (h : WeilBounded f C) {ε : ℝ} (hε : 0 ≤ ε)
+    (hbound : ((Fintype.card G : ℝ) - 1) * C^4 / (Fintype.card F : ℝ)^2
+      ≤ ε^2) :
+    ∑ Q, |(pairCount f Q : ℝ) / (Fintype.card F : ℝ)^2
+        - 1 / (Fintype.card G : ℝ)| ≤ ε := by
+  have hx : 0 ≤ ∑ Q, |(pairCount f Q : ℝ) / (Fintype.card F : ℝ)^2
+      - 1 / (Fintype.card G : ℝ)| :=
+    Finset.sum_nonneg fun Q _ => abs_nonneg _
+  have hsq := (sq_sum_abs_prob_dev_le f h).trans hbound
+  nlinarith [hsq, hx, hε]
+
+/-- **Chebyshev-style bad-set counting**: the number of outputs whose pair
+count deviates from its uniform value by at least `τ`, multiplied by `τ²`,
+is at most the summed squared deviation. -/
+theorem card_dev_ge_le (f : F → G) {C : ℝ} (h : WeilBounded f C) {τ : ℝ}
+    (hτ : 0 ≤ τ) :
+    ((univ.filter fun Q => τ ≤ |(Fintype.card G : ℝ) * pairCount f Q
+        - (Fintype.card F : ℝ)^2|).card : ℝ) * τ^2
+      ≤ (Fintype.card G : ℝ) * ((Fintype.card G : ℝ) - 1)
+          * (C^2 * Fintype.card F)^2 := by
+  classical
+  refine le_trans ?_ (sum_sq_dev_le f h)
+  calc ((univ.filter fun Q => τ ≤ |(Fintype.card G : ℝ) * pairCount f Q
+          - (Fintype.card F : ℝ)^2|).card : ℝ) * τ^2
+      = ∑ _Q ∈ univ.filter (fun Q => τ ≤ |(Fintype.card G : ℝ) * pairCount f Q
+          - (Fintype.card F : ℝ)^2|), τ^2 := by
+        rw [Finset.sum_const, nsmul_eq_mul]
+    _ ≤ ∑ Q ∈ univ.filter (fun Q => τ ≤ |(Fintype.card G : ℝ) * pairCount f Q
+          - (Fintype.card F : ℝ)^2|),
+          ((Fintype.card G : ℝ) * pairCount f Q
+            - (Fintype.card F : ℝ)^2)^2 := by
+        refine Finset.sum_le_sum fun Q hQ => ?_
+        have hdev := (Finset.mem_filter.mp hQ).2
+        calc τ^2 ≤ |(Fintype.card G : ℝ) * pairCount f Q
+              - (Fintype.card F : ℝ)^2|^2 := pow_le_pow_left₀ hτ hdev 2
+          _ = _ := sq_abs _
+    _ ≤ ∑ Q, ((Fintype.card G : ℝ) * pairCount f Q
+          - (Fintype.card F : ℝ)^2)^2 :=
+        Finset.sum_le_sum_of_subset_of_nonneg (Finset.filter_subset _ _)
+          fun Q _ _ => sq_nonneg _
+
+/-- **The zero-repair transport for pair counts**: two mappings agreeing away
+from a single input have two-term pair counts within `4·#F - 2` of each other
+in L¹, because only the pairs containing that input can differ. -/
+theorem sum_abs_pairCount_sub_le [Nonempty F] (f g : F → G) (u₀ : F)
+    (h : ∀ u, u ≠ u₀ → f u = g u) :
+    ∑ Q, |(pairCount f Q : ℝ) - (pairCount g Q : ℝ)|
+      ≤ 4 * Fintype.card F - 2 := by
+  classical
+  set T : Finset (F × F) := univ.filter (fun p => p.1 = u₀ ∨ p.2 = u₀)
+    with hT
+  -- Pairs away from `T` have equal sums under `f` and `g`.
+  have hagree : ∀ p : F × F, p ∉ T → f p.1 + f p.2 = g p.1 + g p.2 := by
+    intro p hp
+    simp only [hT, mem_filter, mem_univ, true_and, not_or] at hp
+    rw [h p.1 hp.1, h p.2 hp.2]
+  -- Each pair count splits at `T`, and the parts away from `T` agree.
+  have hsplit : ∀ (m : F → G) (Q : G), (pairCount m Q : ℕ)
+      = ((univ.filter fun p : F × F => m p.1 + m p.2 = Q) \ T).card
+        + (T.filter fun p => m p.1 + m p.2 = Q).card := by
+    intro m Q
+    have hinter : (univ.filter fun p : F × F => m p.1 + m p.2 = Q) ∩ T
+        = T.filter fun p => m p.1 + m p.2 = Q := by
+      ext p
+      simp only [Finset.mem_inter, mem_filter, mem_univ, true_and]
+      exact ⟨fun ⟨a, b⟩ => ⟨b, a⟩, fun ⟨a, b⟩ => ⟨b, a⟩⟩
+    rw [pairCount, ← hinter, add_comm]
+    exact (Finset.card_inter_add_card_sdiff _ _).symm
+  have hkey : ∀ Q : G, |(pairCount f Q : ℝ) - (pairCount g Q : ℝ)|
+      ≤ ((T.filter fun p => f p.1 + f p.2 = Q).card : ℝ)
+        + ((T.filter fun p => g p.1 + g p.2 = Q).card : ℝ) := by
+    intro Q
+    have hsdiff : ((univ.filter fun p : F × F => f p.1 + f p.2 = Q) \ T)
+        = ((univ.filter fun p : F × F => g p.1 + g p.2 = Q) \ T) := by
+      ext p
+      simp only [Finset.mem_sdiff, mem_filter, mem_univ, true_and]
+      exact ⟨fun ⟨hpQ, hpT⟩ => ⟨by rw [← hagree p hpT]; exact hpQ, hpT⟩,
+        fun ⟨hpQ, hpT⟩ => ⟨by rw [hagree p hpT]; exact hpQ, hpT⟩⟩
+    rw [hsplit f Q, hsplit g Q, hsdiff]
+    push_cast
+    have hx : (0 : ℝ) ≤ (T.filter fun p => f p.1 + f p.2 = Q).card :=
+      Nat.cast_nonneg _
+    have hy : (0 : ℝ) ≤ (T.filter fun p => g p.1 + g p.2 = Q).card :=
+      Nat.cast_nonneg _
+    rw [abs_le]
+    constructor <;> [linarith; linarith]
+  -- Sum the per-output bounds; each side totals `T.card` fibrewise.
+  have hfib : ∀ m : F → G, ∑ Q : G,
+      ((T.filter fun p => m p.1 + m p.2 = Q).card : ℝ) = (T.card : ℝ) := by
+    intro m
+    exact_mod_cast (Finset.card_eq_sum_card_fiberwise
+      (f := fun p : F × F => m p.1 + m p.2) (s := T) (t := univ)
+      fun p _ => mem_univ _).symm
+  -- `T` is two axis copies of `F` overlapping in one pair.
+  have hTcard : T.card = 2 * Fintype.card F - 1 := by
+    have h1 : (univ.filter fun p : F × F => p.1 = u₀) = {u₀} ×ˢ univ := by
+      ext p
+      simp only [mem_filter, mem_univ, true_and, Finset.mem_product,
+        Finset.mem_singleton, and_true]
+    have h2 : (univ.filter fun p : F × F => p.2 = u₀) = univ ×ˢ {u₀} := by
+      ext p
+      simp only [mem_filter, mem_univ, true_and, Finset.mem_product,
+        Finset.mem_singleton, true_and]
+    have hint : (univ.filter fun p : F × F => p.1 = u₀)
+        ∩ (univ.filter fun p : F × F => p.2 = u₀) = {(u₀, u₀)} := by
+      ext p
+      simp [Finset.mem_inter, Prod.ext_iff]
+    have hcards := Finset.card_union_add_card_inter
+      (univ.filter fun p : F × F => p.1 = u₀)
+      (univ.filter fun p : F × F => p.2 = u₀)
+    rw [hint, h1, h2] at hcards
+    simp only [Finset.card_product, Finset.card_singleton, Finset.card_univ,
+      one_mul, mul_one] at hcards
+    rw [hT, Finset.filter_or, h1, h2]
+    omega
+  have hF1 : 1 ≤ 2 * Fintype.card F := by
+    have := Fintype.card_pos (α := F)
+    omega
+  calc ∑ Q, |(pairCount f Q : ℝ) - (pairCount g Q : ℝ)|
+      ≤ ∑ Q : G, (((T.filter fun p => f p.1 + f p.2 = Q).card : ℝ)
+          + ((T.filter fun p => g p.1 + g p.2 = Q).card : ℝ)) :=
+        Finset.sum_le_sum fun Q _ => hkey Q
+    _ = (T.card : ℝ) + (T.card : ℝ) := by
+        rw [Finset.sum_add_distrib, hfib f, hfib g]
+    _ = 4 * Fintype.card F - 2 := by
+        rw [hTcard]
+        push_cast [Nat.cast_sub hF1]
+        ring
+
+/-- **The regularity distance of the deployed mapping**, through the transport:
+a mapping that agrees away from a single input with a Weil-bounded one has
+regularity distance at most the Weil-bounded mapping's budget `ε` plus the
+transported pair-count difference divided through by `(#F)²`. The triangle
+inequality splits each output's deviation into the Weil-bounded mapping's
+deviation plus the pair-count difference, so `sum_abs_prob_dev_le` and
+`sum_abs_pairCount_sub_le` bound the two sums. -/
+theorem sum_abs_prob_dev_transport_le [Nonempty F] (f g : F → G) (u₀ : F)
+    (hfg : ∀ u, u ≠ u₀ → f u = g u) {C : ℝ} (h : WeilBounded g C) {ε : ℝ}
+    (hε : 0 ≤ ε)
+    (hbound : ((Fintype.card G : ℝ) - 1) * C^4 / (Fintype.card F : ℝ)^2
+      ≤ ε^2) :
+    ∑ Q, |(pairCount f Q : ℝ) / (Fintype.card F : ℝ)^2
+        - 1 / (Fintype.card G : ℝ)|
+      ≤ ε + (4 * Fintype.card F - 2) / (Fintype.card F : ℝ)^2 := by
+  have hF : (0 : ℝ) < (Fintype.card F : ℝ)^2 := by positivity
+  have htri : ∀ Q : G, |(pairCount f Q : ℝ) / (Fintype.card F : ℝ)^2
+      - 1 / (Fintype.card G : ℝ)|
+      ≤ |(pairCount g Q : ℝ) / (Fintype.card F : ℝ)^2
+          - 1 / (Fintype.card G : ℝ)|
+        + |(pairCount f Q : ℝ) - (pairCount g Q : ℝ)|
+          / (Fintype.card F : ℝ)^2 := by
+    intro Q
+    have hsplit : (pairCount f Q : ℝ) / (Fintype.card F : ℝ)^2
+        - 1 / (Fintype.card G : ℝ)
+        = ((pairCount g Q : ℝ) / (Fintype.card F : ℝ)^2
+            - 1 / (Fintype.card G : ℝ))
+          + ((pairCount f Q : ℝ) - (pairCount g Q : ℝ))
+            / (Fintype.card F : ℝ)^2 := by
+      field_simp
+      ring
+    rw [hsplit]
+    refine le_trans (abs_add_le _ _) (add_le_add le_rfl ?_)
+    rw [abs_div, abs_of_pos hF]
+  refine le_trans (Finset.sum_le_sum fun Q _ => htri Q) ?_
+  rw [Finset.sum_add_distrib, ← Finset.sum_div]
+  refine add_le_add (sum_abs_prob_dev_le g h hε hbound) ?_
+  gcongr
+  exact sum_abs_pairCount_sub_le f g u₀ hfg
+
 end CompElliptic.Hashing
diff --git a/CompElliptic/Isogenies/Homomorphism.lean b/CompElliptic/Isogenies/Homomorphism.lean
index ff68d15..c62dc4d 100644
--- a/CompElliptic/Isogenies/Homomorphism.lean
+++ b/CompElliptic/Isogenies/Homomorphism.lean
@@ -457,20 +457,6 @@ theorem map_neg (P : SWPoint I.domain) : I.map (-P) = -I.map P := by
   · have hP0 : (P.x, P.y) = ((0 : F), (0 : F)) := P.onCurve.resolve_left hP
     rw [SWPoint.ext_pair (E := I.domain) (Q := 0) hP0, neg_zero, I.map_zero, neg_zero]
 
-omit [DecidableEq F] in
-/-- Two on-curve points with the same abscissa are equal or negatives. -/
-private theorem eq_or_eq_neg_of_x_eq {E : SWCurve F} {R S : SWPoint E}
-    (hR : OnCurve E.A E.B (R.x, R.y)) (hS : OnCurve E.A E.B (S.x, S.y))
-    (hx : R.x = S.x) : R = S ∨ R = -S := by
-  have h1 : R.y^2 = R.x^3 + E.A * R.x + E.B := hR
-  have h2 : S.y^2 = S.x^3 + E.A * S.x + E.B := hS
-  rw [hx] at h1
-  have h0 : (R.y - S.y) * (R.y + S.y) = 0 := by linear_combination h1 - h2
-  rcases mul_eq_zero.mp h0 with h | h
-  · exact Or.inl (SWPoint.ext_pair (Prod.ext_iff.mpr ⟨hx, sub_eq_zero.mp h⟩))
-  · exact Or.inr (SWPoint.ext_pair (Prod.ext_iff.mpr
-      ⟨by rw [SWPoint.neg_x]; exact hx, by rw [SWPoint.neg_y]; linear_combination h⟩))
-
 /-- The image of a sum is the sum of the images, up to sign. -/
 theorem map_add_pm (h2 : (2 : F) ≠ 0)
     (hd : ∀ X : F, ¬ OnCurve I.domain.A I.domain.B (X, 0))
@@ -484,7 +470,13 @@ theorem map_add_pm (h2 : (2 : F) ≠ 0)
           ((I.map (P + Q)).x, (I.map (P + Q)).y) := by
         rw [map, dif_pos hs]
         exact I.onCurve_mapXY hs
-      exact eq_or_eq_neg_of_x_eq hLon hi (I.map_add_x h2 hd hc P Q)
+      have hLne : I.map (P + Q) ≠ 0 := fun h0 => by
+        rw [h0] at hLon
+        exact origin_not_on_curve I.codomain hLon
+      have hine : I.map P + I.map Q ≠ 0 := fun h0 => by
+        rw [h0] at hi
+        exact origin_not_on_curve I.codomain hi
+      exact SWPoint.eq_pm_of_x_eq hLne hine (I.map_add_x h2 hd hc P Q)
     · exfalso
       have hi0 : ((I.map P + I.map Q).x, (I.map P + I.map Q).y) = ((0 : F), (0 : F)) :=
         (I.map P + I.map Q).onCurve.resolve_left hi
@@ -546,8 +538,8 @@ operation: it is cryptographically hazardous unless composed with
 modelled as a random oracle by itself. Maps two field elements, intended to
 be outputs of `hash_to_field`, to the isogeny's domain curve, adds there, and
 applies the isogeny once (spec §5.4.9.8). -/
-def mapHashOutputsToCurve (m : F → SWPoint I.domain) (u₀ u₁ : F) : SWPoint I.codomain :=
-  I.map (m u₀ + m u₁)
+def mapHashOutputsToCurve (f : F → SWPoint I.domain) (u₀ u₁ : F) : SWPoint I.codomain :=
+  I.map (f u₀ + f u₁)
 
 /-- `mapHashOutputsToCurve` agrees with applying the isogeny to each point and
 adding on the codomain. RFC 9380 §6.6.3 notes exactly this optimization —add on
@@ -558,8 +550,8 @@ spec and `hashtocurve.sage` use the one-evaluation order, while
 theorem mapHashOutputsToCurve_eq (h2 : (2 : F) ≠ 0)
     (hd : ∀ X : F, ¬ OnCurve I.domain.A I.domain.B (X, 0))
     (hc : ∀ X : F, ¬ OnCurve I.codomain.A I.codomain.B (X, 0))
-    (m : F → SWPoint I.domain) (u₀ u₁ : F) :
-    I.mapHashOutputsToCurve m u₀ u₁ = I.map (m u₀) + I.map (m u₁) :=
-  I.map_add h2 hd hc (m u₀) (m u₁)
+    (f : F → SWPoint I.domain) (u₀ u₁ : F) :
+    I.mapHashOutputsToCurve f u₀ u₁ = I.map (f u₀) + I.map (f u₁) :=
+  I.map_add h2 hd hc (f u₀) (f u₁)
 
 end CompElliptic.Isogenies.ThreeIsogeny
diff --git a/CompElliptic/TrustBoundary.lean b/CompElliptic/TrustBoundary.lean
index 417c3a7..fc6cb6d 100644
--- a/CompElliptic/TrustBoundary.lean
+++ b/CompElliptic/TrustBoundary.lean
@@ -112,6 +112,14 @@ assert_axioms CompElliptic.Curves.Pasta.Pallas.norm_charSum_mapToCurve_sub_zeroR
   CompElliptic.Fields.Pasta.pallasBase)
 assert_axioms CompElliptic.Curves.Pasta.Vesta.norm_charSum_mapToCurve_sub_zeroRepaired +native(
   CompElliptic.Fields.Pasta.vestaBase)
+assert_axioms CompElliptic.Curves.Pasta.Pallas.card_mapToCurve_fibre_le +native(
+  CompElliptic.Fields.Pasta.pallasBase,
+  CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt,
+  CompElliptic.Curves.Pasta.Pallas.q_nsmul_isoGpt)
+assert_axioms CompElliptic.Curves.Pasta.Vesta.card_mapToCurve_fibre_le +native(
+  CompElliptic.Fields.Pasta.vestaBase,
+  CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt,
+  CompElliptic.Curves.Pasta.Vesta.p_nsmul_isoGpt)
 assert_axioms CompElliptic.Curves.Pasta.Pallas.mapHashOutputsToCurve_eq +native(
   CompElliptic.Fields.Pasta.pallasBase)
 assert_axioms CompElliptic.Curves.Pasta.Vesta.mapHashOutputsToCurve_eq +native(
diff --git a/scripts/gen_pasta.py b/scripts/gen_pasta.py
index 1b7052f..e5ccd02 100644
--- a/scripts/gen_pasta.py
+++ b/scripts/gen_pasta.py
@@ -50,6 +50,11 @@
 /-- Vesta scalar field = Pallas base field. -/
 abbrev VestaScalarField := PallasBaseField
 
+/-- The Pallas base field (= the Vesta scalar field), under its `pasta_curves` letter. -/
+abbrev Fp := PallasBaseField
+/-- The Pallas scalar field (= the Vesta base field), under its `pasta_curves` letter. -/
+abbrev Fq := PallasScalarField
+
 /-- Tonelli–Shanks data for the Pallas base field `𝔽ₚ`: `p-1 = 2^32 · T`, with `rootOfUnity = 5ᵀ`
 (`pallas.py`). -/
 def pallasBase : TonelliShanks PallasBaseField where