Scalar multiplication through the transport

Ed25519Math.scalarMul n (ψ P) = ψ (n • P), so Ed25519 scalar multiplication inherits Mathlib's n • P lemmas.

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.psi_smul (n : ℕ) (P : Ed25519Group.W) : Ed25519Group.psi (n • P) = Ed25519Math.scalarMul n (Ed25519Group.psi P)

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.psi_zero' : Ed25519Group.psi 0 = Ed25519Math.zero

ψ 0 = zero.

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.eq_zero_of_psi_eq_zero {P : Ed25519Group.W} (h : Ed25519Group.psi P = Ed25519Math.zero) : P = 0

The only point mapping to the Edwards identity is the identity.

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.natCast_ne_zero' {n : ℕ} (h0 : n ≠ 0) (hlt : n < NIKE.X25519Common.p) : ↑n ≠ 0

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.psi_G : Ed25519Group.psi NIKE.X25519.G = Ed25519Math.basepoint

The Ed25519 basepoint is the image of the X25519 basepoint.

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.ell_smul_G : Ed25519Math.ell • NIKE.X25519.G = 0

ℓ • G = 0 in Curve25519's group: the basepoint has order dividing ℓ.

Multiples of the basepoint

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.smul_mod (n : ℕ) : (n % Ed25519Math.ell) • NIKE.X25519.G = n • NIKE.X25519.G

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.sm_base (n : ℕ) : Ed25519Math.scalarMul n Ed25519Math.basepoint = Ed25519Group.psi (n • NIKE.X25519.G)

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.sm_base_onCurve (n : ℕ) : Ed25519Math.onCurve (Ed25519Math.scalarMul n Ed25519Math.basepoint)

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.sm_sm (a b : ℕ) : Ed25519Math.scalarMul a (Ed25519Math.scalarMul b Ed25519Math.basepoint) = Ed25519Math.scalarMul (a * b) Ed25519Math.basepoint

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.sm_mod (n : ℕ) : Ed25519Math.scalarMul (n % Ed25519Math.ell) Ed25519Math.basepoint = Ed25519Math.scalarMul n Ed25519Math.basepoint

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.add_sm (a b : ℕ) : Ed25519Math.add (Ed25519Math.scalarMul a Ed25519Math.basepoint) (Ed25519Math.scalarMul b Ed25519Math.basepoint) = Ed25519Math.scalarMul (a + b) Ed25519Math.basepoint

theorem Cryptlib.Primitives.Sign.Ed25519Scalar.sm_mod_eq {a b : ℕ} (h : a % Ed25519Math.ell = b % Ed25519Math.ell) : Ed25519Math.scalarMul a Ed25519Math.basepoint = Ed25519Math.scalarMul b Ed25519Math.basepoint