theorem prime_101 : Nat.Prime 101

101 is prime, the modulus used in Example 9.1 where G = 𝔽₁₀₁ˣ.

theorem ex_9_1_pow : 3 ^ 24 = 37

Example 9.1: in 𝔽₁₀₁ˣ, 3^24 ≡ 37 (mod 101), witnessing log₃ 37 = 24.

theorem card_units_101 : Fintype.card (ZMod 101)ˣ = 100

The multiplicative group (ZMod 101)ˣ has order 100 = φ(101).

theorem order_factorization : 100 = 2 ^ 2 * 5 ^ 2

Prime factorization 100 = 2² · 5², used in analyzing the order of 𝔽₁₀₁ˣ.

theorem ex_9_2_mul : 46 * 3 = 37

Example 9.2: in 𝔽₁₀₁⁺, 46 · 3 ≡ 37 (mod 101), witnessing log₃ 37 = 46.

theorem card_ZMod_101 : Fintype.card (ZMod 101) = 101

The additive group ZMod 101 has cardinality 101.

theorem prime_order_101 : Nat.Prime 101

101 is prime, so ZMod 101 is a field and 3 is invertible there.

theorem inv_3_mod_101 : 3⁻¹ = 34

The inverse of 3 in ZMod 101 is 34.

theorem ex_9_2_via_inv : 34 * 37 = 46

Computation: log₃ 37 = 34 · 37 = 46 in ZMod 101, matching Example 9.2 via inversion.

noncomputable def birthdayProb (N n : ℕ) : ℝ

Probability that the first n steps of a random walk on a set of size N all land on distinct vertices (the birthday-product ∏_{i<n} (1 - (i+1)/N)).

noncomputable def expectedRho (N : ℕ) : ℝ

Expected value of the rho-length for a random walk on a set of size N, expressed as ∑_{n<N} birthdayProb N n. Theorem 9.3 shows this is asymptotic to √(πN/2).

@[simp]

theorem birthdayProb_zero (N : ℕ) : birthdayProb N 0 = 1

Base case: the empty product is 1, so birthdayProb N 0 = 1.

theorem birthdayProb_succ (N n : ℕ) : birthdayProb N (n + 1) = birthdayProb N n * (1 - ↑(n + 1) / ↑N)

Recursive relation: appending the (n+1)-th step multiplies by 1 - (n+1)/N.

theorem factor_pos {N i : ℕ} (hN : 0 < N) (hi : i + 1 < N) : 0 < 1 - ↑(i + 1) / ↑N

Each factor 1 - (i+1)/N is strictly positive when i + 1 < N.

theorem birthdayProb_pos {N n : ℕ} (hN : 0 < N) (hn : n < N) : 0 < birthdayProb N n

birthdayProb N n is strictly positive whenever n < N.

theorem birthdayProb_le_one {N n : ℕ} (hN : 0 < N) (hn : n < N) : birthdayProb N n ≤ 1

birthdayProb N n ≤ 1 whenever n < N (as a product of factors in [0, 1)).

theorem log_factor_le {N i : ℕ} (hN : 0 < N) (hi : i + 1 < N) : Real.log (1 - ↑(i + 1) / ↑N) ≤ -↑(i + 1) / ↑N

Concavity bound: log(1 - x) ≤ -x for the factor x = (i+1)/N.

theorem sum_range_succ_cast (n : ℕ) : ∑ i ∈ Finset.range n, ↑(i + 1) = ↑n * (↑n + 1) / 2

Closed-form for the shifted arithmetic sum: ∑_{i<n} (i+1) = n(n+1)/2.

theorem birthdayProb_le_exp {N n : ℕ} (hN : 0 < N) (hn : n < N) : birthdayProb N n ≤ Real.exp (-(↑n * (↑n + 1) / (2 * ↑N)))

Exponential upper bound on birthdayProb N n, obtained by summing log(1 - x) ≤ -x.

theorem birthdayProb_le_exp_sq {N n : ℕ} (hN : 0 < N) (hn : n < N) : birthdayProb N n ≤ Real.exp (-(↑n ^ 2 / (2 * ↑N)))

Quadratic exponential bound: birthdayProb N n ≤ exp(-n²/(2N)), the more convenient form used in the Gaussian comparison.

theorem gaussian_integral_half_line (N : ℝ) (hN : 0 < N) : ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-(1 / (2 * N)) * x ^ 2) = √(Real.pi * N / 2)

Gaussian half-line integral: ∫₀^∞ exp(-x²/(2N)) dx = √(πN/2).

theorem gaussian_sum_asymptotic : Asymptotics.IsEquivalent Filter.atTop (fun (N : ℕ) => ∑ n ∈ Finset.range N, Real.exp (-(↑n ^ 2 / (2 * ↑N)))) fun (N : ℕ) => √(Real.pi * ↑N / 2)

The Riemann sum ∑_{n<N} exp(-n²/(2N)) is asymptotic to the Gaussian integral √(πN/2). This is the analytic engine behind Theorem 9.3.

theorem expectedRho_le_gaussianSum {N : ℕ} (hN : 0 < N) : expectedRho N ≤ ∑ n ∈ Finset.range N, Real.exp (-(↑n ^ 2 / (2 * ↑N)))

expectedRho N is bounded above by the Gaussian Riemann sum, term-by-term.

theorem log_one_sub_ge {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x < 1) : -x - x ^ 2 / (1 - x) ≤ Real.log (1 - x)

Lower bound on log(1 - x): log(1 - x) ≥ -x - x²/(1 - x) for 0 ≤ x < 1.

theorem log_one_sub_ge' {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1 / 2) : -x - 2 * x ^ 2 ≤ Real.log (1 - x)

For x ≤ 1/2, log(1 - x) ≥ -x - 2x², a clean version of the lower bound.

theorem expectedRho_equiv_gaussian_sum : Asymptotics.IsEquivalent Filter.atTop (fun (N : ℕ) => expectedRho N) fun (N : ℕ) => ∑ n ∈ Finset.range N, Real.exp (-(↑n ^ 2 / (2 * ↑N)))

The expected rho-length expectedRho N is asymptotically equivalent to the Gaussian sum ∑_{n<N} exp(-n²/(2N)) (via matching upper and lower bounds on each birthdayProb).

theorem expected_rho_asymptotic : Asymptotics.IsEquivalent Filter.atTop (fun (N : ℕ) => expectedRho N) fun (N : ℕ) => √(Real.pi * ↑N / 2)

Theorem 9.3 (Sutherland): the expected rho-length for a random walk on a set of size N satisfies E[ρ] ~ √(πN/2) as N → ∞.

structure PollardRhoTriple (N : ℕ) (G : Type u_2) : Type u_2

A triple (a, b, γ) tracked by the Pollard-ρ walk for the DLP: scalars a, b ∈ ℤ/Nℤ together with the corresponding group element γ = a·α + b·β.

• a : ZMod N
• b : ZMod N
• γ : G

theorem PollardRhoTriple.ext {N : ℕ} {G : Type u_2} {x y : PollardRhoTriple N G} (a : x.a = y.a) (b : x.b = y.b) (γ : x.γ = y.γ) : x = y

theorem PollardRhoTriple.ext_iff {N : ℕ} {G : Type u_2} {x y : PollardRhoTriple N G} : x = y ↔ x.a = y.a ∧ x.b = y.b ∧ x.γ = y.γ

structure PollardRhoConfig (G : Type u_2) [AddCommGroup G] (N : ℕ) [NeZero N] : Type u_2

Configuration for Pollard's rho algorithm (Algorithm 9.5): the generator α, the target β = log_α^{-1} β, the number r of partition classes (with 0 < r), the per-class scalar offsets c, d and group offsets δ, and a partition map h : G → Fin r.

• α : G
• β : G
• r : ℕ
• hr : 0 < self.r
• c : Fin self.r → ZMod N
• d : Fin self.r → ZMod N
• δ : Fin self.r → G
• h : G → Fin self.r

def PollardRhoTriple.IsValid {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] [Module (ZMod N) G] (cfg : PollardRhoConfig G N) (t : PollardRhoTriple N G) : Prop

A triple is valid for cfg when γ = a • α + b • β, i.e. it tracks the correct linear combination.

def PollardRhoConfig.PartitionValid {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] [Module (ZMod N) G] (cfg : PollardRhoConfig G N) : Prop

A partition is valid when each class offset δ i equals c i • α + d i • β, so applying a partition step preserves the invariant γ = a • α + b • β.

def pollardRhoStep {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] (cfg : PollardRhoConfig G N) (t : PollardRhoTriple N G) : PollardRhoTriple N G

One step of the Pollard-ρ iteration: identify the class i = h(γ) and add (c i, d i, δ i) to the triple.

theorem pollardRhoStep_preserves_invariant {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] [Module (ZMod N) G] (cfg : PollardRhoConfig G N) (t : PollardRhoTriple N G) (hpart : cfg.PartitionValid) (hinv : PollardRhoTriple.IsValid cfg t) : PollardRhoTriple.IsValid cfg (pollardRhoStep cfg t)

Under PartitionValid, a single pollardRhoStep preserves the invariant γ = a • α + b • β.

theorem pollardRho_collision_relation {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] [Module (ZMod N) G] (cfg : PollardRhoConfig G N) (t₁ t₂ : PollardRhoTriple N G) (h₁ : PollardRhoTriple.IsValid cfg t₁) (h₂ : PollardRhoTriple.IsValid cfg t₂) (hcoll : t₁.γ = t₂.γ) : (t₁.a - t₂.a) • cfg.α = (t₂.b - t₁.b) • cfg.β

Collision relation: if two valid triples have the same group element γ, then (a₁ - a₂) • α = (b₂ - b₁) • β. This is the linear identity that the discrete log is extracted from.

theorem pollardRho_dlog_extraction {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] [Module (ZMod N) G] (cfg : PollardRhoConfig G N) (t₁ t₂ : PollardRhoTriple N G) (h₁ : PollardRhoTriple.IsValid cfg t₁) (h₂ : PollardRhoTriple.IsValid cfg t₂) (hcoll : t₁.γ = t₂.γ) (hinv : IsUnit (t₂.b - t₁.b)) : cfg.β = ((t₂.b - t₁.b)⁻¹ * (t₁.a - t₂.a)) • cfg.α

DLP extraction (Algorithm 9.5, step 4): if b₂ - b₁ is invertible in ℤ/Nℤ, solve the collision relation for β = ((b₂ - b₁)⁻¹ (a₁ - a₂)) • α, recovering log_α β.

def pollardRhoIter {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] (cfg : PollardRhoConfig G N) (t₀ : PollardRhoTriple N G) : ℕ → PollardRhoTriple N G

Iterate pollardRhoStep starting from t₀ for n steps.

theorem pollardRhoIter_preserves_invariant {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] [Module (ZMod N) G] (cfg : PollardRhoConfig G N) (t₀ : PollardRhoTriple N G) (hpart : cfg.PartitionValid) (h₀ : PollardRhoTriple.IsValid cfg t₀) (n : ℕ) : PollardRhoTriple.IsValid cfg (pollardRhoIter cfg t₀ n)

Iterating preserves the invariant γ = a • α + b • β under PartitionValid.

theorem pollardRhoIter_gamma_independent {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] (cfg : PollardRhoConfig G N) (t₁ t₂ : PollardRhoTriple N G) (hγ : t₁.γ = t₂.γ) (n : ℕ) : (pollardRhoIter cfg t₁ n).γ = (pollardRhoIter cfg t₂ n).γ

The γ-component of pollardRhoIter depends only on the initial γ, not on the initial scalar coordinates (a, b).

def evalAffine {p : ℕ} (ab : ZMod p × ZMod p) (t : ZMod p) : ZMod p

Evaluate the affine function t ↦ a t + b over ZMod p at t, where ab = (a, b).

theorem card_roots_affine_le_one {p : ℕ} [hp : Fact (Nat.Prime p)] (ab : ZMod p × ZMod p) (hab : ab ≠ (0, 0)) : {t : ZMod p | evalAffine ab t = 0}.card ≤ 1

A nonzero affine function t ↦ a t + b over a field ZMod p has at most one root.

theorem card_collision_pair_le_one {p : ℕ} [hp : Fact (Nat.Prime p)] (f g : ZMod p × ZMod p) (hfg : f ≠ g) : {t : ZMod p | evalAffine f t = evalAffine g t}.card ≤ 1

Two distinct affine functions f, g over ZMod p agree on at most one value of t.

theorem card_lt_pairs_eq (s : ℕ) : {ij : Fin s × Fin s | ij.1 < ij.2}.card = s * (s - 1) / 2

The number of strictly ordered pairs in Fin s × Fin s is s(s-1)/2.

theorem choose_two_le_sq_div_two (s : ℕ) : ↑(s.choose 2) ≤ ↑s ^ 2 / 2

Real-valued upper bound: binom(s, 2) ≤ s²/2.

noncomputable def collisionSet {p : ℕ} [hp : Fact (Nat.Prime p)] (s : ℕ) (F : Fin s → ZMod p × ZMod p) : Finset (ZMod p)

Shoup's collision set: the set of t ∈ ZMod p such that two distinct affine encodings F i ≠ F j (with i < j) collide at t. The generic-group adversary can only succeed on these t.

theorem card_collisionSet_le {p : ℕ} [hp : Fact (Nat.Prime p)] (s : ℕ) (F : Fin s → ZMod p × ZMod p) : (collisionSet s F).card ≤ s * (s - 1) / 2

The collision set has cardinality at most s(s-1)/2: at most one collision per ordered pair of distinct affine encodings.

theorem shoup_bound_le {p : ℕ} [hp : Fact (Nat.Prime p)] (s : ℕ) (F : Fin s → ZMod p × ZMod p) : ↑(collisionSet s F).card / ↑(Fintype.card (ZMod p)) ≤ ↑s ^ 2 / (2 * ↑p)

Non-strict Shoup bound: |collisionSet| / p ≤ s²/(2p).

theorem shoup_bound {p : ℕ} [hp : Fact (Nat.Prime p)] (s : ℕ) (hs : 1 ≤ s) (F : Fin s → ZMod p × ZMod p) : ↑(collisionSet s F).card / ↑(Fintype.card (ZMod p)) < ↑s ^ 2 / (2 * ↑p)

Theorem 9.7 (Shoup, strict form): for s ≥ 1, the success probability of any generic algorithm making at most s queries on ZMod p is strictly less than s²/(2p).

theorem corollary_9_8_sq {p : ℕ} [hp : Fact (Nat.Prime p)] (s : ℕ) (F : Fin s → ZMod p × ZMod p) (h_det : collisionSet s F = Finset.univ) : 2 * ↑p ≤ ↑s ^ 2

Squared form of Corollary 9.8: if a deterministic generic DLP algorithm succeeds on every t ∈ ZMod p (i.e., the collision set is everything) using s group operations, then s² ≥ 2p.

theorem corollary_9_8 {p : ℕ} [hp : Fact (Nat.Prime p)] (s : ℕ) (F : Fin s → ZMod p × ZMod p) (h_det : collisionSet s F = Finset.univ) : √(2 * ↑p) ≤ ↑s

Corollary 9.8 (Sutherland): every deterministic generic DLP algorithm in a cyclic group of prime order p uses at least √(2p) group operations.

theorem corollary_9_8_group {N : ℕ} [hN : Fact (Nat.Prime N)] (G : Type u_1) [Group G] [Fintype G] [IsCyclic G] (hcard : Fintype.card G = N) (s : ℕ) (F : Fin s → ZMod N × ZMod N) (h_det : collisionSet s F = Finset.univ) : √2 * √↑(Fintype.card G) ≤ ↑s

Group-theoretic form of Corollary 9.8: for a finite cyclic group G of prime order N, every deterministic generic DLP algorithm uses at least √2 · √|G| operations.

theorem corollary_9_8_group_sq {N : ℕ} [hN : Fact (Nat.Prime N)] (G : Type u_1) [Group G] [Fintype G] [IsCyclic G] (hcard : Fintype.card G = N) (s : ℕ) (F : Fin s → ZMod N × ZMod N) (h_det : collisionSet s F = Finset.univ) : 2 * ↑(Fintype.card G) ≤ ↑s ^ 2

Squared group-theoretic form of Corollary 9.8: s² ≥ 2 |G|.

theorem corollary_9_9 {p : ℕ} [hp : Fact (Nat.Prime p)] (s : ℕ) (F : Fin s → ZMod p × ZMod p) (r : ℕ) (hr : ↑r < √↑p / Real.log ↑p) (successSet : Finset (ZMod p)) (h_sub : successSet ⊆ collisionSet s F) (h_mc : 1 / 2 ≤ ↑successSet.card / ↑(Fintype.card (ZMod p))) : √↑p ≤ ↑s ∧ √↑p - √↑p / Real.log ↑p < ↑s - ↑r

Corollary 9.9 (Sutherland): every generic Monte Carlo DLP algorithm in a cyclic group of prime order p that uses o(√p / log p) random group elements still requires at least (1 + o(1))√p group operations. The lemma extracts the quantitative inequalities √p ≤ s and √p - √p/log p < s - r.

noncomputable def largestPrimeFactor (N : ℕ) (hN : 1 < N) : ℕ

The largest prime factor of N > 1, used by Shoup's bound to express the generic-group lower bound in terms of the hardest prime-order subgroup.

theorem largestPrimeFactor_prime (N : ℕ) (hN : 1 < N) : Nat.Prime (largestPrimeFactor N hN)

The largest prime factor of N > 1 is itself prime.

theorem largestPrimeFactor_dvd (N : ℕ) (hN : 1 < N) : largestPrimeFactor N hN ∣ N

The largest prime factor divides N.

theorem le_largestPrimeFactor {N q : ℕ} (hN : 1 < N) (hq : q ∈ N.primeFactors) : q ≤ largestPrimeFactor N hN

Any prime factor of N is bounded above by the largest prime factor.

theorem largestPrimeFactor_prime_eq (p : ℕ) (hp : Nat.Prime p) : largestPrimeFactor p ⋯ = p

When p is itself prime, its largest prime factor is p.

theorem largestPrimeFactor_pos (N : ℕ) (hN : 1 < N) : 0 < largestPrimeFactor N hN

The largest prime factor is positive.

theorem largestPrimeFactor_fact (N : ℕ) (hN : 1 < N) : Fact (Nat.Prime (largestPrimeFactor N hN))

Package the primality of the largest prime factor as a Fact, for use with typeclass-driven lemmas like ZMod.card.

theorem dlp_success_le_collision_prob {p : ℕ} [hp : Fact (Nat.Prime p)] (s : ℕ) (F : Fin s → ZMod p × ZMod p) (successSet : Finset (ZMod p)) (h_sub : successSet ⊆ collisionSet s F) : ↑successSet.card / ↑(Fintype.card (ZMod p)) ≤ ↑(collisionSet s F).card / ↑(Fintype.card (ZMod p))

Any DLP success set contained in the collision set has probability bounded by the collision-set probability.

theorem shoup_theorem_9_7_prime {p : ℕ} [hp : Fact (Nat.Prime p)] (s : ℕ) (F : Fin s → ZMod p × ZMod p) (successSet : Finset (ZMod p)) (h_sub : successSet ⊆ collisionSet s F) : ↑successSet.card / ↑(Fintype.card (ZMod p)) ≤ ↑s ^ 2 / (2 * ↑p)

Theorem 9.7 (Shoup) for prime modulus: any DLP success probability for s generic queries is at most s²/(2p).

theorem shoup_theorem_9_7_at_largest_prime_factor (N : ℕ) (hN : 1 < N) (s : ℕ) (F : Fin s → ZMod (largestPrimeFactor N hN) × ZMod (largestPrimeFactor N hN)) (successSet : Finset (ZMod (largestPrimeFactor N hN))) : successSet ⊆ collisionSet s F → ↑successSet.card / ↑(Fintype.card (ZMod (largestPrimeFactor N hN))) ≤ ↑s ^ 2 / (2 * ↑(largestPrimeFactor N hN))

Shoup's bound applied to the largest prime factor of N: the success probability of a DLP attack restricted to the prime-order subgroup of order lp(N) is at most s²/(2·lp(N)).

noncomputable def projToLargestPrime (N : ℕ) (hN : 1 < N) : ZMod N →+* ZMod (largestPrimeFactor N hN)

Canonical ring hom ZMod N → ZMod (largestPrimeFactor N) induced by the divisibility lp(N) ∣ N, used to reduce a generic DLP on ZMod N to the prime-order subgroup.

theorem zmod_castHom_kernel_card {N q : ℕ} [NeZero N] (hq : Fact (Nat.Prime q)) (hdvd : q ∣ N) : {a : ZMod N | (ZMod.castHom hdvd (ZMod q)) a = 0}.card = N / q

For a prime q ∣ N, the kernel of the cast ZMod N → ZMod q has cardinality N / q.

theorem zmod_castHom_fiber_le {N q : ℕ} [NeZero N] (hq : Fact (Nat.Prime q)) (hdvd : q ∣ N) (b : ZMod q) : {a : ZMod N | (ZMod.castHom hdvd (ZMod q)) a = b}.card ≤ N / q

Every fiber of the cast ZMod N → ZMod q has cardinality at most N / q (equal cardinality N / q in fact).

theorem card_le_card_image_mul_div {N q : ℕ} [NeZero N] (hq : Fact (Nat.Prime q)) (hdvd : q ∣ N) (S : Finset (ZMod N)) : S.card ≤ (Finset.image (⇑(ZMod.castHom hdvd (ZMod q))) S).card * (N / q)

For any S ⊆ ZMod N, |S| ≤ |image S| · (N / q) using the uniform fiber bound.

theorem shoup_theorem_9_7_general_N (N : ℕ) [NeZero N] (hN : 1 < N) (s : ℕ) (successSet : Finset (ZMod N)) (F : Fin s → ZMod (largestPrimeFactor N hN) × ZMod (largestPrimeFactor N hN)) (hp : Fact (Nat.Prime (largestPrimeFactor N hN))) (h_reduction : Finset.image (⇑(projToLargestPrime N hN)) successSet ⊆ collisionSet s F) : ↑successSet.card / ↑(Fintype.card (ZMod N)) ≤ ↑s ^ 2 / (2 * ↑(largestPrimeFactor N hN))

Theorem 9.7 (Shoup) for general modulus N: reducing to the largest prime factor gives a success-probability bound of s²/(2 · lp(N)) for any generic DLP attack on ZMod N.

theorem sum_sq_range_real (n : ℕ) : ∑ k ∈ Finset.range n, ↑k ^ 2 = ↑n * (↑n - 1) * (2 * ↑n - 1) / 6

Closed form for the sum of squares: ∑_{k<n} k² = n(n-1)(2n-1)/6.

noncomputable def lasVegasExpectedLB (p M : ℕ) : ℝ

Expected-value lower bound used in Corollary 9.10: ∑_{m<M} (1 - m²/(2p)), which bounds the expected number of group operations for a Las Vegas DLP algorithm.

theorem lasVegasExpectedLB_closed_form (p M : ℕ) (hp' : 0 < ↑p) : lasVegasExpectedLB p M = ↑M - ↑M * (↑M - 1) * (2 * ↑M - 1) / (12 * ↑p)

Closed form: lasVegasExpectedLB p M = M - M(M-1)(2M-1)/(12 p).

theorem lasVegas_shoup_lb {p : ℕ} (M : ℕ) (cdf : ℕ → ℝ) (hcdf : ∀ (s : ℕ), cdf s ≤ ↑s ^ 2 / (2 * ↑p)) : lasVegasExpectedLB p M ≤ ∑ m ∈ Finset.range M, (1 - cdf m)

Using Shoup's bound cdf s ≤ s²/(2p) term-by-term gives the lower bound lasVegasExpectedLB p M ≤ ∑ (1 - cdf m).

theorem lasVegasExpectedLB_ge (p M : ℕ) (hp' : 0 < ↑p) (hM : ↑M ^ 2 ≤ 2 * ↑p) (hM1 : 1 ≤ M) : 2 * ↑M / 3 ≤ lasVegasExpectedLB p M

When M² ≤ 2p and M ≥ 1, the expected-LB satisfies lasVegasExpectedLB p M ≥ 2M/3.

theorem floor_sqrt_2p_sq_le (p : ℕ) : ↑⌊√(2 * ↑p)⌋₊ ^ 2 ≤ 2 * ↑p

⌊√(2p)⌋² ≤ 2p, providing the hypothesis M² ≤ 2p for M = ⌊√(2p)⌋.

theorem floor_sqrt_2p_ge_one {p : ℕ} [hp : Fact (Nat.Prime p)] : 1 ≤ ⌊√(2 * ↑p)⌋₊

For p prime, ⌊√(2p)⌋ ≥ 1.

theorem two_sqrt_two_p_eq (p : ℕ) : 2 * √(2 * ↑p) / 3 = 2 * √2 / 3 * √↑p

Rewrite 2√(2p)/3 = (2√2/3)·√p.

theorem corollary_9_10 {p : ℕ} [hp : Fact (Nat.Prime p)] (cdf : ℕ → ℝ) (hcdf : ∀ (s : ℕ), cdf s ≤ ↑s ^ 2 / (2 * ↑p)) : 2 * √2 / 3 * √↑p - 2 / 3 ≤ ∑ m ∈ Finset.range ⌊√(2 * ↑p)⌋₊, (1 - cdf m)

Corollary 9.10 (Sutherland), explicit form: given Shoup's bound cdf s ≤ s²/(2p) on the success probability, the expected number of operations of a Las Vegas DLP algorithm is at least (2√2/3) √p - 2/3, giving the (2√2/3 + o(1))√N lower bound.

theorem tail_sum_le_nat {α : Type u_1} [Fintype α] (f : α → ℕ) (M : ℕ) : ∑ m ∈ Finset.range M, {x : α | m < f x}.card ≤ ∑ x : α, f x

Tail-sum identity: ∑_{m<M} |{x : m < f x}| ≤ ∑_x f x, used to convert a collection of tail counts into a sum of integer-valued data.

theorem sum_falling_range_real (n : ℕ) : ∑ k ∈ Finset.range n, ↑k * (↑k - 1) = ↑n * (↑n - 1) * (↑n - 2) / 3

Closed form for the falling-factorial sum: ∑_{k<n} k(k-1) = n(n-1)(n-2)/3.

theorem corollary_9_10_expected_bound (p : ℕ) [Fact (Nat.Prime p)] (w : ZMod p → ℕ) : (∀ (s : ℕ), {t : ZMod p | w t ≤ s}.card ≤ s * (s - 1) / 2) → 2 * √(2 * ↑p) / 3 ≤ (∑ t : ZMod p, ↑(w t)) / ↑p

Corollary 9.10 (expected-value form): if the work function w : ZMod p → ℕ satisfies Shoup's combinatorial constraint, then the expected number of operations (∑ w t)/p is at least 2√(2p)/3.

def LasVegasShoupConstraint {p : ℕ} [hp : Fact (Nat.Prime p)] (w : ZMod p → ℕ) : Prop

Shoup's combinatorial constraint on a Las Vegas DLP work function w: for every s, at most s(s-1)/2 instances t are solved by w t ≤ s queries.

theorem las_vegas_count_solved_le {p : ℕ} [hp : Fact (Nat.Prime p)] (w : ZMod p → ℕ) (hw : LasVegasShoupConstraint w) : {t : ZMod p | w t ≤ p.sqrt}.card ≤ p / 2

At most p/2 instances are solved within ⌊√p⌋ queries.

theorem las_vegas_count_unsolved_ge {p : ℕ} [hp : Fact (Nat.Prime p)] (w : ZMod p → ℕ) (hw : LasVegasShoupConstraint w) : p / 2 ≤ {t : ZMod p | p.sqrt < w t}.card

Complementary count: at least p/2 instances are unsolved within ⌊√p⌋ queries.

theorem las_vegas_sum_lower_bound_nat {p : ℕ} [hp : Fact (Nat.Prime p)] (w : ZMod p → ℕ) (hw : LasVegasShoupConstraint w) : (p.sqrt + 1) * (p / 2) ≤ ∑ t : ZMod p, w t

Natural-number lower bound: (⌊√p⌋ + 1) · (p/2) ≤ ∑ w t.

theorem real_sqrt_le_nat_sqrt_succ (n : ℕ) : √↑n ≤ ↑n.sqrt + 1

√n ≤ Nat.sqrt n + 1 as real numbers.

theorem corollary_9_11_quantitative {p : ℕ} [hp : Fact (Nat.Prime p)] (w : ZMod p → ℕ) (hw : LasVegasShoupConstraint w) : ↑(p.sqrt + 1) * ↑(p / 2) / ↑p ≤ (∑ t : ZMod p, ↑(w t)) / ↑p

Quantitative form of Corollary 9.11: real-valued lower bound on the expected work (∑ w t)/p in terms of (⌊√p⌋ + 1)(p/2)/p.

theorem corollary_9_11_precise_constant (p : ℕ) [Fact (Nat.Prime p)] (w : ZMod p → ℕ) : LasVegasShoupConstraint w → √(2 * ↑p) / 2 ≤ (∑ t : ZMod p, ↑(w t)) / ↑p

Sharp constant form: the expected work (∑ w t)/p ≥ √(2p)/2.

theorem corollary_9_11 (p : ℕ) [Fact (Nat.Prime p)] (w : ZMod p → ℕ) (hw : LasVegasShoupConstraint w) : √2 / 2 * √↑p ≤ (∑ t : ZMod p, ↑(w t)) / ↑p

Corollary 9.11 (Sutherland): every generic Las Vegas DLP algorithm in a cyclic group of prime order p uses an expected Ω(√p) group operations, with the explicit constant √2/2 · √p.

structure PollardRhoDPConfig (G : Type u_2) [AddCommGroup G] (N : ℕ) [NeZero N] extends PollardRhoConfig G N : Type u_2

Configuration for Pollard-ρ with distinguished points (Algorithm 9.6): extends PollardRhoConfig with a boolean predicate B : G → Bool identifying distinguished group elements that get logged for collision detection.

• α : G
• β : G
• r : ℕ
• hr : 0 < self.r
• c : Fin self.r → ZMod N
• d : Fin self.r → ZMod N
• δ : Fin self.r → G
• h : G → Fin self.r
• B : G → Bool

def PollardRhoTriple.IsDistinguished {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] (dpCfg : PollardRhoDPConfig G N) (t : PollardRhoTriple N G) : Prop

A triple is distinguished when its γ-component is flagged by B.

def PollardRhoDPConfig.IsCollision {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] (dpCfg : PollardRhoDPConfig G N) (t₁ t₂ : PollardRhoTriple N G) : Prop

Two distinguished-point triples are a "DP collision" when both are distinguished and have the same γ (only then does the algorithm record a useful collision).

theorem pollardRhoDP_collision_relation {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] [Module (ZMod N) G] (dpCfg : PollardRhoDPConfig G N) (t₁ t₂ : PollardRhoTriple N G) (h₁ : PollardRhoTriple.IsValid dpCfg.toPollardRhoConfig t₁) (h₂ : PollardRhoTriple.IsValid dpCfg.toPollardRhoConfig t₂) (hcoll : dpCfg.IsCollision t₁ t₂) : (t₁.a - t₂.a) • dpCfg.α = (t₂.b - t₁.b) • dpCfg.β

The collision relation (a₁ - a₂) • α = (b₂ - b₁) • β for the distinguished-points variant, derived from the ordinary Pollard-ρ collision relation.

theorem pollardRhoDP_dlog_extraction {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] [Module (ZMod N) G] (dpCfg : PollardRhoDPConfig G N) (t₁ t₂ : PollardRhoTriple N G) (h₁ : PollardRhoTriple.IsValid dpCfg.toPollardRhoConfig t₁) (h₂ : PollardRhoTriple.IsValid dpCfg.toPollardRhoConfig t₂) (hcoll : dpCfg.IsCollision t₁ t₂) (hinv : IsUnit (t₂.b - t₁.b)) : dpCfg.β = ((t₂.b - t₁.b)⁻¹ * (t₁.a - t₂.a)) • dpCfg.α

DLP extraction for the distinguished-points variant of Pollard-ρ: β = ((b₂ - b₁)⁻¹ (a₁ - a₂)) • α when b₂ - b₁ is invertible in ZMod N.

theorem pollardRhoDP_iter_preserves_invariant {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] [Module (ZMod N) G] (dpCfg : PollardRhoDPConfig G N) (t₀ : PollardRhoTriple N G) (hpart : dpCfg.PartitionValid) (h₀ : PollardRhoTriple.IsValid dpCfg.toPollardRhoConfig t₀) (n : ℕ) : PollardRhoTriple.IsValid dpCfg.toPollardRhoConfig (pollardRhoIter dpCfg.toPollardRhoConfig t₀ n)

Iterating the underlying Pollard-ρ step in the DP setting preserves the validity invariant γ = a • α + b • β.

theorem pollardRhoDP_correctness {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] [Module (ZMod N) G] (dpCfg : PollardRhoDPConfig G N) (t₀ : PollardRhoTriple N G) (hpart : dpCfg.PartitionValid) (h₀ : PollardRhoTriple.IsValid dpCfg.toPollardRhoConfig t₀) (j k : ℕ) (hcoll : dpCfg.IsCollision (pollardRhoIter dpCfg.toPollardRhoConfig t₀ j) (pollardRhoIter dpCfg.toPollardRhoConfig t₀ k)) (hinv : IsUnit ((pollardRhoIter dpCfg.toPollardRhoConfig t₀ k).b - (pollardRhoIter dpCfg.toPollardRhoConfig t₀ j).b)) : dpCfg.β = (((pollardRhoIter dpCfg.toPollardRhoConfig t₀ k).b - (pollardRhoIter dpCfg.toPollardRhoConfig t₀ j).b)⁻¹ * ((pollardRhoIter dpCfg.toPollardRhoConfig t₀ j).a - (pollardRhoIter dpCfg.toPollardRhoConfig t₀ k).a)) • dpCfg.α

End-to-end correctness of Pollard-ρ with distinguished points (Algorithm 9.6): once a DP collision occurs at iteration indices j, k and b_k - b_j is invertible in ZMod N, the algorithm correctly recovers β as a multiple of α, hence log_α β.

theorem pollardRhoDP_all_distinguished {G : Type u_1} [AddCommGroup G] {N : ℕ} [NeZero N] (dpCfg : PollardRhoDPConfig G N) (hB : ∀ (g : G), dpCfg.B g = true) (t : PollardRhoTriple N G) : PollardRhoTriple.IsDistinguished dpCfg t

Degenerate sanity check: if the distinguishing predicate B always returns true, then every triple is distinguished (so Algorithm 9.6 reduces to ordinary Pollard-ρ).