def shortWeierstrass {R : Type u_1} [CommRing R] (a b : R) : WeierstrassCurve R

The short Weierstrass curve y² = x³ + a x + b over a commutative ring R, represented as a WeierstrassCurve with a₁ = a₂ = a₃ = 0, a₄ = a and a₆ = b.

def ecmDiscriminant {R : Type u_1} [CommRing R] (a b : R) : R

The discriminant quantity 4 a³ + 27 b² of the short Weierstrass curve y² = x³ + a x + b, used by ECM (Algorithm 10.11) to detect a nontrivial gcd with N.

theorem shortWeierstrass_Δ {R : Type u_1} [CommRing R] (a b : R) : (shortWeierstrass a b).Δ = -16 * ecmDiscriminant a b

The Δ invariant of the short Weierstrass curve y² = x³ + a x + b equals -16 (4 a³ + 27 b²).

structure ECMConfig : Type

Configuration data for ECM (Algorithm 10.11): the integer N to be factored (with 1 < N), a smoothness bound B for primes used in the scalar, and a prime bound M.

• N : ℕ
• B : ℕ
• M : ℕ
• hN : 1 < self.N

structure ECMCurveParams : Type

The randomly chosen curve parameters used by ECM: a coefficient a together with the initial point (x₀, y₀) on the resulting short Weierstrass curve.

• a : ℤ
• x₀ : ℤ
• y₀ : ℤ

def ECMCurveParams.b (params : ECMCurveParams) : ℤ

The coefficient b = y₀² - x₀³ - a x₀ derived from (a, x₀, y₀) so that the short Weierstrass curve y² = x³ + a x + b passes through (x₀, y₀).

def ECMCurveParams.curve (params : ECMCurveParams) : WeierstrassCurve ℤ

The short Weierstrass curve over ℤ determined by params.

def ECMCurveParams.disc (params : ECMCurveParams) : ℤ

The discriminant 4 a³ + 27 b² of the ECM curve defined by params.

theorem ECMCurveParams.point_on_curve (params : ECMCurveParams) : WeierstrassCurve.Affine.Equation params.curve params.x₀ params.y₀

By construction, the chosen point (x₀, y₀) satisfies the affine Weierstrass equation of params.curve.

def ECMCurveParams.curveModP (params : ECMCurveParams) (p : ℕ) : WeierstrassCurve.Affine (ZMod p)

Reduce the ECM curve modulo a prime p, viewing it as an affine curve over ZMod p.

def ecmSmoothExponent (ℓ M : ℕ) : ℕ

The exponent e such that ℓ^{e-1} ≤ (√M + 1)² < ℓ^e, as used by ECM to ensure every smooth order ≤ (√M + 1)² divides the scaled scalar.

theorem ecmSmoothExponent_bound_le (ℓ M : ℕ) (_hℓ : 1 < ℓ) : ℓ ^ (ecmSmoothExponent ℓ M - 1) ≤ (M.sqrt + 1) ^ 2

Lower-bound side of the defining property: ℓ^{e-1} ≤ (√M + 1)² for e = ecmSmoothExponent ℓ M.

theorem ecmSmoothExponent_bound_lt (ℓ M : ℕ) (hℓ : 1 < ℓ) : (M.sqrt + 1) ^ 2 < ℓ ^ ecmSmoothExponent ℓ M

Strict upper-bound side: (√M + 1)² < ℓ^e for e = ecmSmoothExponent ℓ M.

def ecmSmoothScalar (B M : ℕ) : ℕ

The ECM scalar multiplier: the product ∏_{ℓ < B prime} ℓ^{ecmSmoothExponent ℓ M}, designed so that every B-smooth integer ≤ (√M + 1)² divides it.

def ecmPartialScalar (ℓ₁ M : ℕ) : ℕ

Partial ECM scalar accumulated up to and including the prime ℓ₁: the product ∏_{ℓ ≤ ℓ₁ prime} ℓ^{ecmSmoothExponent ℓ M}.

theorem ecmSmoothScalar_pos (B M : ℕ) : 0 < ecmSmoothScalar B M

The ECM scalar ecmSmoothScalar B M is strictly positive.

theorem ecmPartialScalar_pos (ℓ₁ M : ℕ) : 0 < ecmPartialScalar ℓ₁ M

The partial ECM scalar ecmPartialScalar ℓ₁ M is strictly positive.

theorem ecmSmoothScalar_smooth (B M : ℕ) : ecmSmoothScalar B M ∈ B.smoothNumbers

The ECM scalar ecmSmoothScalar B M is itself B-smooth: all of its prime factors are strictly less than B.

theorem ecmPartialScalar_smooth (ℓ₁ M : ℕ) : ecmPartialScalar ℓ₁ M ∈ (ℓ₁ + 1).smoothNumbers

The partial ECM scalar ecmPartialScalar ℓ₁ M is (ℓ₁ + 1)-smooth: all of its prime factors are at most ℓ₁.

theorem Nat.factorization_le_log_of_pos' {n p : ℕ} (hn : 0 < n) (hp : 1 < p) : n.factorization p ≤ log p n

The p-adic valuation of a positive integer is bounded by log_p n.

theorem prime_pow_dvd_ecmSmoothScalar {B M p : ℕ} (hp : Nat.Prime p) (hpB : p < B) : p ^ ecmSmoothExponent p M ∣ ecmSmoothScalar B M

Each prime power factor p^{ecmSmoothExponent p M} (with p < B prime) divides the ECM scalar ecmSmoothScalar B M.

theorem prime_pow_dvd_ecmPartialScalar {ℓ₁ M p : ℕ} (hp : Nat.Prime p) (hpB : p ≤ ℓ₁) : p ^ ecmSmoothExponent p M ∣ ecmPartialScalar ℓ₁ M

Each prime power factor p^{ecmSmoothExponent p M} (with p ≤ ℓ₁ prime) divides the partial ECM scalar ecmPartialScalar ℓ₁ M.

theorem smooth_dvd_ecmSmoothScalar {n B M : ℕ} (hn : n ≠ 0) (hsmooth : n ∈ B.smoothNumbers) (hbound : n ≤ (M.sqrt + 1) ^ 2) : n ∣ ecmSmoothScalar B M

Key divisibility property: every nonzero B-smooth integer n ≤ (√M + 1)² divides the ECM scalar ecmSmoothScalar B M.

theorem smooth_dvd_ecmPartialScalar {n ℓ₁ M : ℕ} (hn : n ≠ 0) (hsmooth : n ∈ (ℓ₁ + 1).smoothNumbers) (hbound : n ≤ (M.sqrt + 1) ^ 2) : n ∣ ecmPartialScalar ℓ₁ M

Partial analogue: every nonzero (ℓ₁ + 1)-smooth integer n ≤ (√M + 1)² divides the partial ECM scalar ecmPartialScalar ℓ₁ M.

inductive ECMResult (N : ℕ) : Type

The outcome of one trial of ECM (Algorithm 10.11): either a proper nontrivial divisor d of N (with 1 < d < N, d ∣ N), or failure.

• factor {N : ℕ} (d : ℕ) (hd_gt : 1 < d) (hd_lt : d < N) (hd_dvd : d ∣ N) : ECMResult N
• failure {N : ℕ} : ECMResult N

def ECMResult.isSuccess {N : ℕ} : ECMResult N → Prop

ECMResult.isSuccess is True exactly when the result is a factor, False on failure.

theorem ecm_correctness (cfg : ECMConfig) (params : ECMCurveParams) (p₁ p₂ : ℕ) [Fact (Nat.Prime p₁)] [Fact (Nat.Prime p₂)] (_hne : p₁ ≠ p₂) (_hdvd₁ : p₁ ∣ cfg.N) (_hdvd₂ : p₂ ∣ cfg.N) (hp₁M : p₁ ≤ cfg.M) (_hdisc : ¬↑cfg.N ∣ params.disc) (ℓ₁ : ℕ) (_hℓ₁_prime : Nat.Prime ℓ₁) (_hℓ₁_bound : ℓ₁ < cfg.B) (P₁ : (params.curveModP p₁).Point) (P₂ : (params.curveModP p₂).Point) (hsmooth₁ : addOrderOf P₁ ∈ (ℓ₁ + 1).smoothNumbers) (hord₁_bound : addOrderOf P₁ ≤ (p₁.sqrt + 1) ^ 2) (hnotsmooth₂ : addOrderOf P₂ ∉ (ℓ₁ + 1).smoothNumbers) : ecmPartialScalar ℓ₁ cfg.M • P₁ = 0 ∧ ecmPartialScalar ℓ₁ cfg.M • P₂ ≠ 0

Correctness of ECM (Theorem 10.12): assume N has distinct prime divisors p₁, p₂ with p₁ ≤ M, the discriminant is not divisible by N, and reductions P₁ ∈ E(𝔽_{p₁}), P₂ ∈ E(𝔽_{p₂}) are such that |P₁| is ℓ₁-smooth (with |P₁| ≤ (√p₁ + 1)²) but |P₂| is not. Then the partial scalar kills P₁ modulo p₁ while leaving P₂ nonzero modulo p₂, so the gcd step exposes a nontrivial factor of N.