def IsSmooth (B n : ℕ) : Prop

A natural number n is B-smooth if all of its prime factors are at most B, i.e. n ∈ Nat.smoothNumbers (B + 1). Smoothness is the key notion underlying subexponential factoring algorithms.

@[implicit_reducible]

instance instDecidableIsSmooth (B n : ℕ) : Decidable (IsSmooth B n)

B-smoothness is decidable: it reduces to deciding membership of n in the finite-indexed set Nat.smoothNumbers (B + 1).

theorem isSmooth_iff {B n : ℕ} : IsSmooth B n ↔ n ≠ 0 ∧ ∀ p ∈ n.primeFactorsList, p ≤ B

Unfolded characterization of smoothness: IsSmooth B n iff n ≠ 0 and every prime factor of n is at most B.

noncomputable def smoothCount (x y : ℝ) : ℕ

The count Ψ(x, y): the number of ⌊y⌋-smooth positive integers up to ⌊x⌋.

def cepFilter (ε : ℝ) : Filter (ℝ × ℝ)

The Canfield–Erdős–Pomerance filter on (u, x): pairs going to infinity constrained by u < (1 - ε) · log x / log log x. Used to state the CEP asymptotic.

theorem canfield_erdos_pomerance (ε : ℝ) (hε_pos : 0 < ε) (hε_lt : ε < 1) : (fun (p : ℝ × ℝ) => Real.log (↑(smoothCount p.2 (p.2 ^ (1 / p.1))) / p.2) + p.1 * Real.log p.1) =o[cepFilter ε] fun (p : ℝ × ℝ) => p.1 * Real.log p.1

Canfield–Erdős–Pomerance theorem: in the range u < (1 - ε) log x / log log x, log(Ψ(x, x^{1/u}) / x) + u log u = o(u log u), i.e. the density of smooth numbers is governed by Dickman's function.

def factorBase (B : ℕ) : Finset ℕ

The factor base of bound B: the finset of primes q ≤ B.

theorem mem_factorBase_iff {q B : ℕ} : q ∈ factorBase B ↔ q ≤ B ∧ Nat.Prime q

Membership in the factor base: q ∈ factorBase B iff q ≤ B and q is prime.

noncomputable def dlog {G : Type u_1} [CommGroup G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) (β : G) : ZMod n

The discrete logarithm of β ∈ G to base g (where g generates the cyclic group of order n), valued in ZMod n. Built by transporting through the isomorphism G ≃ Multiplicative (ZMod n) induced by the generator.

theorem dlog_mul {G : Type u_1} [CommGroup G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) (x y : G) : dlog hg hn (x * y) = dlog hg hn x + dlog hg hn y

The discrete log is a homomorphism on products: dlog(xy) = dlog x + dlog y.

theorem dlog_inv {G : Type u_1} [CommGroup G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) (x : G) : dlog hg hn x⁻¹ = -dlog hg hn x

The discrete log sends inverses to negatives: dlog(x⁻¹) = -dlog x.

theorem dlog_zpow_g {G : Type u_1} [CommGroup G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) (i : ℤ) : dlog hg hn (g ^ i) = ↑i

The discrete log of g^i is i modulo n.

theorem dlog_zpow {G : Type u_1} [CommGroup G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) (x : G) (k : ℤ) : dlog hg hn (x ^ k) = ↑k * dlog hg hn x

The discrete log is ℤ-linear on integer powers: dlog(x^k) = k · dlog x.

theorem dlog_prod {G : Type u_1} [CommGroup G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) (S : Finset ℕ) (f : ℕ → G) : dlog hg hn (∏ q ∈ S, f q) = ∑ q ∈ S, dlog hg hn (f q)

Additivity of discrete log over a finite product: dlog(∏_{q ∈ S} f q) = ∑_{q ∈ S} dlog (f q).

theorem dlog_generator {G : Type u_1} [CommGroup G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) : dlog hg hn g = 1

The discrete log of the generator is 1 ∈ ZMod n.

theorem dlog_one {G : Type u_1} [CommGroup G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) : dlog hg hn 1 = 0

The discrete log of the identity is 0 ∈ ZMod n.

theorem index_calculus_relation {G : Type u_1} [CommGroup G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) (S : Finset ℕ) (f : ℕ → G) (exps : ℕ → ℤ) (b : G) (e : ℤ) (hfact : g ^ e * b⁻¹ = ∏ q ∈ S, f q ^ exps q) : ∑ q ∈ S, ↑(exps q) * dlog hg hn (f q) + dlog hg hn b = ↑e

Index-calculus relation: if g^e · b⁻¹ = ∏ f(q)^{exps q} over a factor base, then in ZMod n (n = |G|) the discrete logs satisfy ∑ exps q · dlog(f q) + dlog b = e. This is the linear equation collected during the index-calculus discrete log algorithm.

structure IndexCalculusRelation (B : ℕ) : Type

A single relation collected during index calculus with smoothness bound B: records the exponent on the generator and the exponent vector over the factor base (supported within factorBase B).

• exponent : ℤ
• factorExponents : ℕ → ℤ
• support_subset (q : ℕ) : self.factorExponents q ≠ 0 → q ∈ factorBase B

structure IndexCalculusConfig : Type

Configuration parameters for index calculus modulo a prime p: the prime p, its primality witness, the smoothness bound B, and the group order N = p - 1.

• p : ℕ
• hp : Nat.Prime self.p
• B : ℕ
• N : ℕ

def IndexCalculusConfig.factorBaseSet (cfg : IndexCalculusConfig) : Finset ℕ

The factor base associated with an index-calculus configuration.

def IndexCalculusConfig.factorBaseSize (cfg : IndexCalculusConfig) : ℕ

Size of the factor base in the configuration.

def IndexCalculusConfig.relationsNeeded (cfg : IndexCalculusConfig) : ℕ

Number of relations needed to solve the linear system in index calculus: factor-base size plus one.

def IndexCalculusRelation.IsValid {B : ℕ} {G : Type u_1} [CommGroup G] (R : IndexCalculusRelation B) (g b : G) (f : ℕ → G) : Prop

Validity of a recorded relation in a group G with generator g and factor-base lift f: the equation g^{exponent} · b⁻¹ = ∏ f(q)^{factorExponents q} holds.

def PollardPM1.smoothExponent (N B : ℕ) : ℕ

Pollard p−1 smooth exponent: the product ∏_{ℓ ≤ B prime} ℓ^{⌈log_ℓ N⌉}, guaranteed to be divisible by every B-smooth integer up to N.

def PollardPM1.IsBSmooth (B n : ℕ) : Prop

Local definition of B-smoothness used in the Pollard p−1 analysis: n ≠ 0 and every prime factor is at most B.

def PollardPM1.largestPrimeFactor (n : ℕ) : ℕ

The largest prime factor of n, taken to be 0 if n has no prime factors.

noncomputable def PollardPM1.pollardPM1 (N B a : ℕ) : Option ℕ

Pollard p−1 factoring step: computes gcd(a^m - 1, N) for the smooth exponent m = smoothExponent N B. Returns a nontrivial factor of N if one is found by either gcd(a, N) or gcd(a^m - 1, N).

def PollardPM1.pollardStep (N ℓ e b : ℕ) : ℕ

One stage of Pollard p−1: raise b to ℓ^e modulo N.

theorem PollardPM1.le_foldl_max_init {l : List ℕ} {init : ℕ} : init ≤ List.foldl max init l

The initial accumulator is bounded by any List.foldl max outcome.

theorem PollardPM1.le_foldl_max_of_mem_list {l : List ℕ} {x : ℕ} (hx : x ∈ l) (init : ℕ) : x ≤ List.foldl max init l

Every element of the list is bounded by the foldl max of the list.

theorem PollardPM1.isBSmooth_largestPrimeFactor {n : ℕ} (hn : n ≠ 0) : IsBSmooth (largestPrimeFactor n) n

For nonzero n, n is automatically largestPrimeFactor n-smooth.

theorem PollardPM1.foldl_max_le_of_init_and_elems {l : List ℕ} {init B : ℕ} (hinit : init ≤ B) (h : ∀ x ∈ l, x ≤ B) : List.foldl max init l ≤ B

If the initial accumulator and all list elements are ≤ B, then so is List.foldl max init l.

theorem PollardPM1.factorization_le_clog {q n N : ℕ} (hq : 1 < q) (hn : n ≠ 0) (hnN : n < N) : n.factorization q ≤ Nat.clog q N

For q > 1 and nonzero n < N, the q-adic valuation of n is at most clog q N. Used to bound prime-power factors of smooth n.

theorem PollardPM1.smoothExponent_pos (N B : ℕ) : 0 < smoothExponent N B

The smooth exponent smoothExponent N B is positive.

theorem PollardPM1.prime_not_dvd_smoothExponent {q N B : ℕ} (hq : Nat.Prime q) (hqB : B < q) : ¬q ∣ smoothExponent N B

A prime q > B does not divide smoothExponent N B, since the smooth exponent only uses primes ℓ ≤ B.

theorem PollardPM1.dvd_smoothExponent_of_isBSmooth {n N B : ℕ} (hsmooth : IsBSmooth B n) (hnN : n < N) : n ∣ smoothExponent N B

Key divisibility lemma for Pollard p−1: any B-smooth n < N divides smoothExponent N B.

theorem PollardPM1.pow_smoothExponent_eq_one_mod {p N B : ℕ} (hp : Nat.Prime p) (hsmooth : IsBSmooth B (p - 1)) (hnN : p - 1 < N) (u : (ZMod p)ˣ) : ↑u ^ smoothExponent N B = 1

Pollard p−1 correctness: for prime p with (p − 1) being B-smooth and less than N, any unit u ∈ (ZMod p)ˣ satisfies u^{smoothExponent N B} = 1.

theorem PollardPM1.gcd_proper_divisor {n N p q : ℕ} (hpN : p ∣ N) (hqN : q ∣ N) (hp : Nat.Prime p) (hpn : p ∣ n) (hqn : ¬q ∣ n) (hN : 1 < N) : 1 < n.gcd N ∧ n.gcd N < N

If p ∣ N, q ∣ N, p prime, p ∣ n, but q ∤ n, and N > 1, then gcd(n, N) is a proper nontrivial divisor of N. This is the abstract correctness of "gcd reveals a factor" used at the end of Pollard p−1 / ECM.

theorem PollardPM1.smoothExponent_dvd_of_le {N B₁ B₂ : ℕ} (h : B₁ ≤ B₂) : smoothExponent N B₁ ∣ smoothExponent N B₂

Monotonicity of smoothExponent in the smoothness bound: if B₁ ≤ B₂ then smoothExponent N B₁ ∣ smoothExponent N B₂.

theorem PollardPM1.list_foldl_max_mem_or_eq_init (l : List ℕ) (init : ℕ) : List.foldl max init l ∈ l ∨ List.foldl max init l = init

For any list l, l.foldl max init is either an element of l or equals the initial value init.

theorem PollardPM1.largestPrimeFactor_mem_primeFactorsList {n : ℕ} (h : Nat.Prime (largestPrimeFactor n)) : largestPrimeFactor n ∈ n.primeFactorsList

If largestPrimeFactor n is actually prime, then it appears in n's prime-factors list.

theorem PollardPM1.largestPrimeFactor_dvd {n : ℕ} (h : Nat.Prime (largestPrimeFactor n)) (hn : n ≠ 0) : largestPrimeFactor n ∣ n

If largestPrimeFactor n is prime and n ≠ 0, then it actually divides n.

theorem PollardPM1.card_mth_roots_mul_largest_prime_le {q m : ℕ} (hq : Nat.Prime q) (hℓq_prime : Nat.Prime (largestPrimeFactor (q - 1))) (hℓq_not_dvd : ¬largestPrimeFactor (q - 1) ∣ m) : Nat.card ↥(powMonoidHom m).ker * largestPrimeFactor (q - 1) ≤ q - 1

Cardinality bound used in Pollard p−1 second-stage analysis: for prime q with ℓ = largestPrimeFactor (q − 1) prime and ℓ ∤ m, we have |ker(x ↦ x^m : (ZMod q)ˣ)| · ℓ ≤ q − 1.

theorem PollardPM1.largestPrimeFactor_prime_of_pos {n : ℕ} (h : 0 < largestPrimeFactor n) : Nat.Prime (largestPrimeFactor n)

If largestPrimeFactor n > 0, it is actually a prime.

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

Short Weierstrass curve over a commutative ring: y² = x³ + a x + b, realized by setting (a₁, a₂, a₃, a₄, a₆) = (0, 0, 0, a, b).

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

ECM discriminant of the short Weierstrass curve y² = x³ + a x + b: 4 a³ + 27 b². The full Δ differs by a factor -16.

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

The standard Weierstrass discriminant Δ of shortWeierstrass a b equals -16 (4 a³ + 27 b²) = -16 · ecmDiscriminant a b.

structure ECMFactoring.ECMConfig : Type

Configuration data for the elliptic curve method (ECM): the modulus N, the smoothness bound B, the prime-search bound M, and a witness 1 < N.

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

structure ECMFactoring.ECMCurveParams : Type

ECM curve parameters over ℤ: choice of a and a base point (x₀, y₀). The value of b is computed so that (x₀, y₀) lies on the curve.

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

def ECMFactoring.ECMCurveParams.b (params : ECMCurveParams) : ℤ

The constant term b of the ECM curve, chosen so that (x₀, y₀) lies on y² = x³ + a x + b.

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

The elliptic curve over ℤ associated to ECM parameters.

def ECMFactoring.ECMCurveParams.disc (params : ECMCurveParams) : ℤ

ECM discriminant of the chosen curve.

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

By construction of b, the prescribed base point (x₀, y₀) satisfies the Weierstrass equation.

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

The ECM curve reduced modulo a prime p, viewed as an affine Weierstrass curve over ZMod p.

def ECMFactoring.ecmSmoothExponent (ℓ M : ℕ) : ℕ

Per-prime exponent used in ECM: ⌊log_ℓ ((√M + 1)²)⌋ + 1, large enough to cover any prime-power up to (√M + 1)² as a factor of the multiplier.

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

Lower bound: ℓ^{ecmSmoothExponent ℓ M − 1} ≤ (√M + 1)², used to show the exponent isn't too large.

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

Upper bound: (√M + 1)² < ℓ^{ecmSmoothExponent ℓ M}, used to show the exponent is large enough.

def ECMFactoring.ecmSmoothScalar (B M : ℕ) : ℕ

ECM smooth scalar k = ∏_{ℓ < B prime} ℓ^{ecmSmoothExponent ℓ M}: every B-smooth integer at most (√M + 1)² divides this scalar.

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

Positivity of the ECM smooth scalar.

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

The ECM smooth scalar is itself a B-smooth number.

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

For positive n and p > 1, the p-adic valuation of n is at most log_p n.

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

For prime p < B, the full prime-power factor p^{ecmSmoothExponent p M} divides the ECM smooth scalar.

theorem ECMFactoring.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 for ECM: any nonzero B-smooth n ≤ (√M + 1)² divides the ECM smooth scalar ecmSmoothScalar B M.

theorem ECMFactoring.ecm_algebraic_step (cfg : ECMConfig) (params : ECMCurveParams) (p₁ p₂ : ℕ) [Fact (Nat.Prime p₁)] [Fact (Nat.Prime p₂)] (hp₁M : p₁ ≤ cfg.M) (P₁ : (params.curveModP p₁).Point) (P₂ : (params.curveModP p₂).Point) (hsmooth₁ : addOrderOf P₁ ∈ cfg.B.smoothNumbers) (hord₁_bound : addOrderOf P₁ ≤ (p₁.sqrt + 1) ^ 2) (hnotsmooth₂ : addOrderOf P₂ ∉ cfg.B.smoothNumbers) : ecmSmoothScalar cfg.B cfg.M • P₁ = 0 ∧ ecmSmoothScalar cfg.B cfg.M • P₂ ≠ 0

ECM algebraic step: in the situation P₁ on the reduction mod p₁, where the order of P₁ is B-smooth and bounded, while the order of P₂ is not B-smooth, multiplying by the ECM smooth scalar kills P₁ but not P₂. This separation is what allows ECM to find a factor.

def MontgomeryTorsion.MontgomeryOnCurve {k : Type u_1} [Field k] (A B x y : k) : Prop

The Montgomery form equation B y² = x³ + A x² + x over a field k.

theorem MontgomeryTorsion.ne_add_two_zero_of_sq_ne_four {k : Type u_1} [Field k] {A : k} (h : A ^ 2 ≠ 4) : A + 2 ≠ 0

Auxiliary: if A² ≠ 4 then A + 2 ≠ 0, since A² - 4 = (A + 2)(A - 2).

theorem MontgomeryTorsion.ne_sub_two_zero_of_sq_ne_four {k : Type u_1} [Field k] {A : k} (h : A ^ 2 ≠ 4) : A - 2 ≠ 0

Auxiliary: if A² ≠ 4 then A - 2 ≠ 0.

theorem MontgomeryTorsion.not_isSquare_disc_of_no_roots {k : Type u_1} [Field k] (h2 : 2 ≠ 0) {A : k} (hno_root : ∀ (r : k), r ^ 2 + A * r + 1 ≠ 0) : ¬IsSquare (A ^ 2 - 4)

If the polynomial r² + A r + 1 = 0 has no root in k (char ≠ 2), then its discriminant A² - 4 is a non-square.

theorem MontgomeryTorsion.isSquare_mul_or_of_not_isSquare_mul {k : Type u_1} [Field k] [Fintype k] [DecidableEq k] {a b c : k} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (h : ¬IsSquare (a * b)) : IsSquare (a * c) ∨ IsSquare (b * c)

Quadratic-character lemma over a finite field: if a, b, c are all nonzero and a · b is not a square, then at least one of a · c or b · c is a square.

theorem MontgomeryTorsion.exists_By_sq_eq_of_isSquare_mul_inv {k : Type u_1} [Field k] {A B : k} (hB : B ≠ 0) (h : IsSquare (A * B⁻¹)) : ∃ (y : k), B * y ^ 2 = A

If A · B⁻¹ is a square in k and B ≠ 0, then there exists y with B y² = A. Used to produce y-coordinates of torsion points.

theorem MontgomeryTorsion.montgomery_torsion_10_14 {k : Type u_1} [Field k] [Fintype k] [DecidableEq k] (h2 : 2 ≠ 0) {A B : k} (hB : B ≠ 0) (hA : A ^ 2 ≠ 4) : (∃ (r : k) (s : k), r ≠ 0 ∧ s ≠ 0 ∧ r ≠ s ∧ r ^ 2 + A * r + 1 = 0 ∧ s ^ 2 + A * s + 1 = 0) ∨ (∃ (y : k), B * y ^ 2 = A + 2) ∨ ∃ (y : k), B * y ^ 2 = A - 2

Montgomery torsion existence (Theorem 10.14 of Sutherland's notes): over a finite field k of characteristic ≠ 2, a Montgomery curve B y² = x³ + A x² + x (with B ≠ 0, A² ≠ 4) always has either two distinct rational points of order 2 coming from a factorization (x - r)(x - s) of x² + A x + 1, or a rational point of order 4 (a y with B y² = A ± 2).

def MontgomeryTorsion.IsOrder2Point {k : Type u_1} [Field k] (A B x : k) : Prop

A point (x, 0) of order 2 on the Montgomery curve B y² = x³ + A x² + x, characterized by lying on the curve with y = 0 and x ≠ 0.

def MontgomeryTorsion.IsOrder4Point {k : Type u_1} [Field k] (A B x y : k) : Prop

A point (x, y) of order 4 on the Montgomery curve: a curve point with y ≠ 0 and x = ±1.

def MontgomeryTorsion.HasSubgroupOfOrder4 {k : Type u_1} [Field k] (A B : k) : Prop

The Montgomery curve has an order-4 rational subgroup if it has either two distinct order-2 points or an order-4 point.

theorem MontgomeryTorsion.isOrder2Point_of_root {k : Type u_1} [Field k] {A B r : k} (hr : r ^ 2 + A * r + 1 = 0) (hr0 : r ≠ 0) : IsOrder2Point A B r

A nonzero root r of x² + A x + 1 yields an order-2 point (r, 0) on the Montgomery curve.

theorem MontgomeryTorsion.isOrder4Point_at_one {k : Type u_1} [Field k] {A B y : k} (hy : B * y ^ 2 = A + 2) (hyNe : y ≠ 0) : IsOrder4Point A B 1 y

If B y² = A + 2 with y ≠ 0, then (1, y) is an order-4 point.

theorem MontgomeryTorsion.isOrder4Point_at_neg_one {k : Type u_1} [Field k] {A B y : k} (hy : B * y ^ 2 = A - 2) (hyNe : y ≠ 0) : IsOrder4Point A B (-1) y

If B y² = A - 2 with y ≠ 0, then (-1, y) is an order-4 point.

theorem MontgomeryTorsion.y_ne_zero_of_By_sq_eq_add_two {k : Type u_1} [Field k] {A B y : k} (hA : A ^ 2 ≠ 4) (hy : B * y ^ 2 = A + 2) : y ≠ 0

Under A² ≠ 4, an equation B y² = A + 2 forces y ≠ 0 (otherwise A = -2, contradicting A² ≠ 4).

theorem MontgomeryTorsion.y_ne_zero_of_By_sq_eq_sub_two {k : Type u_1} [Field k] {A B y : k} (hA : A ^ 2 ≠ 4) (hy : B * y ^ 2 = A - 2) : y ≠ 0

Under A² ≠ 4, an equation B y² = A - 2 forces y ≠ 0.

def MontgomeryTorsion.ShortWeierstrassOnCurve {k : Type u_1} [Field k] (a b x y : k) : Prop

The short Weierstrass equation y² = x³ + a x + b over k.

theorem MontgomeryTorsion.theorem_10_15_squareness {k : Type u_1} [Field k] (h2 : 2 ≠ 0) {a b x₀ u v : k} (hcurve_P : ShortWeierstrassOnCurve a b u v) (hcurve_2P : ShortWeierstrassOnCurve a b x₀ 0) (hv : v ≠ 0) (hdouble : x₀ = ((3 * u ^ 2 + a) / (2 * v)) ^ 2 - 2 * u) : (u - x₀) ^ 2 = 3 * x₀ ^ 2 + a ∧ 3 * x₀ ^ 2 + a ≠ 0

"Squareness" step in Theorem 10.15 of Sutherland: if (u, v) is a point on the short Weierstrass curve and 2 · (u, v) = (x₀, 0), then (u - x₀)² = 3 x₀² + a and 3 x₀² + a ≠ 0. This is the key squareness that allows converting to Montgomery form.

theorem MontgomeryTorsion.theorem_10_15_isomorphism {k : Type u_1} [Field k] {a b x₀ A B : k} (hcurve_2P : ShortWeierstrassOnCurve a b x₀ 0) (hB_sq : B ^ 2 * (3 * x₀ ^ 2 + a) = 1) (hA : A = 3 * x₀ * B) (x y : k) : ShortWeierstrassOnCurve a b x y → MontgomeryOnCurve A B (B * (x - x₀)) (B * y)

The forward direction of the Theorem 10.15 isomorphism: the substitution (x, y) ↦ (B (x - x₀), B y) sends short Weierstrass points y² = x³ + a x + b to Montgomery-form points B Y² = X³ + A X² + X for A = 3 x₀ B and B² (3 x₀² + a) = 1.

theorem MontgomeryTorsion.theorem_10_15_inverse {k : Type u_1} [Field k] {a b x₀ A B : k} (hcurve_2P : ShortWeierstrassOnCurve a b x₀ 0) (hB_sq : B ^ 2 * (3 * x₀ ^ 2 + a) = 1) (hA : A = 3 * x₀ * B) (X Y : k) : MontgomeryOnCurve A B X Y → ShortWeierstrassOnCurve a b (X / B + x₀) (Y / B)

The inverse direction of the Theorem 10.15 isomorphism: the substitution (X, Y) ↦ (X / B + x₀, Y / B) sends Montgomery-form points back to short Weierstrass points.

theorem MontgomeryTorsion.theorem_10_15_round_trip {k : Type u_1} [Field k] {x₀ B : k} (hB : B ≠ 0) : (∀ (x y : k), B * (x - x₀) / B + x₀ = x ∧ B * y / B = y) ∧ ∀ (X Y : k), B * (X / B + x₀ - x₀) = X ∧ B * (Y / B) = Y

The two substitutions of Theorem 10.15 are inverse to each other on coordinates, in both directions.

theorem MontgomeryTorsion.theorem_10_15 {k : Type u_1} [Field k] (h2 : 2 ≠ 0) {a b x₀ u v : k} (hcurve_P : ShortWeierstrassOnCurve a b u v) (hcurve_2P : ShortWeierstrassOnCurve a b x₀ 0) (hv : v ≠ 0) (hdouble : x₀ = ((3 * u ^ 2 + a) / (2 * v)) ^ 2 - 2 * u) : ((u - x₀) ^ 2 = 3 * x₀ ^ 2 + a ∧ 3 * x₀ ^ 2 + a ≠ 0) ∧ ∀ (B A : k), B ^ 2 * (3 * x₀ ^ 2 + a) = 1 → A = 3 * x₀ * B → (∀ (x y : k), ShortWeierstrassOnCurve a b x y → MontgomeryOnCurve A B (B * (x - x₀)) (B * y)) ∧ (∀ (X Y : k), MontgomeryOnCurve A B X Y → ShortWeierstrassOnCurve a b (X / B + x₀) (Y / B)) ∧ (∀ (x y : k), B * (x - x₀) / B + x₀ = x ∧ B * y / B = y) ∧ ∀ (X Y : k), B * (X / B + x₀ - x₀) = X ∧ B * (Y / B) = Y

Theorem 10.15 of Sutherland (Montgomery model from order-4 point): if E : y² = x³ + a x + b has a point P = (u, v) whose double is the 2-torsion point (x₀, 0), then 3 x₀² + a is a square in k, and E can be put in Montgomery form E'' : B y² = x³ + A x² + x with B = 1/√(3 x₀² + a) and A = 3 x₀ B; the map (x, y) ↦ (B (x - x₀), B y) gives a bijective isomorphism E ≃ E''.