def Hex.ECPP.shortCurve (p a b : ℕ) : WeierstrassCurve (ZMod p)

The short Weierstrass curve supplied by an ECPP step, reduced modulo p.

Equations

• Hex.ECPP.shortCurve p a b = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := ↑a, a₆ := ↑b }

instance Hex.ECPP.shortCurveIsShortNF (p a b : ℕ) : (shortCurve p a b).IsShortNF

The checker's short curve has zero coefficients a₁, a₂ and a₃.

theorem Hex.ECPP.prime_divisor_gt_three {p n : ℕ} (prime : _root_.Nat.Prime p) (hp : p ∣ n) (hmod : n % 6 = 1 ∨ n % 6 = 5) : 3 < p

The checker coprimality guard excludes characteristics two and three.

theorem Hex.ECPP.cast_mod {p n : ℕ} (hp : p ∣ n) (t : ℕ) : ↑(t % n) = ↑t

Reduction modulo a multiple of p preserves the residue in ZMod p.

theorem Hex.ECPP.cast_modSub {p n : ℕ} (hp : p ∣ n) (hn : 0 < n) (a b : ℕ) : ↑(modSub n a b) = ↑a - ↑b

The checker's natural modular subtraction is field subtraction after reduction at any prime divisor.

theorem Hex.ECPP.inverse_witness {p n d u : ℕ} [Fact (_root_.Nat.Prime p)] (hp : p ∣ n) (h : d * u % n = 1) : ↑u = (↑d)⁻¹

A consumed inverse witness is an actual inverse in every prime residue field.

theorem Hex.ECPP.addWithInverse_reduced {p n x₁ y₁ x₂ d v : ℕ} [Fact (_root_.Nat.Prime p)] {ws rest : List ℕ} {R : Point} (hp : p ∣ n) (hn : 0 < n) (h : addWithInverse n x₁ y₁ x₂ d v ws = some (R, rest)) : ∃ (X : ℕ) (Y : ℕ), R = Point.affine X Y ∧ ↑X = (↑v / ↑d) ^ 2 - ↑x₁ - ↑x₂ ∧ ↑Y = ↑v / ↑d * (↑x₁ - ↑X) - ↑y₁

The coordinates produced by a checked division branch are the field secant or tangent formulas over every prime divisor.

theorem Hex.ECPP.onCurve_reduced {p n a b x y : ℕ} (hp : p ∣ n) (h : onCurve n a b x y = true) : (shortCurve p a b).toAffine.Equation ↑x ↑y

A checked raw point lies on the reduced short curve.

theorem Hex.ECPP.shortCurve_elliptic {p n a b inv : ℕ} (prime : _root_.Nat.Prime p) (hp3 : 3 < p) (hp : p ∣ n) (h : (4 * a * a * a + 27 * b * b) * inv % n = 1) : WeierstrassCurve.IsElliptic (shortCurve p a b).toAffine

The checked discriminant inverse makes the reduced short curve nonsingular.

def Hex.ECPP.Point.Rep (p a b : ℕ) (raw : Point) (P : (shortCurve p a b).toAffine.Point) : Prop

A raw point represents an actual nonsingular affine point after reducing its coordinates into a prime field.

Equations

• Hex.ECPP.Point.Rep p a b Hex.ECPP.Point.infinity P = (P = 0)
• Hex.ECPP.Point.Rep p a b (Hex.ECPP.Point.affine x y) P = ∃ (h : (Hex.ECPP.shortCurve p a b).toAffine.Nonsingular ↑x ↑y), P = WeierstrassCurve.Affine.Point.some (↑x) (↑y) h

theorem Hex.ECPP.startingPoint_rep {p n a b x y inv : ℕ} (prime : _root_.Nat.Prime p) (hp3 : 3 < p) (hp : p ∣ n) (hdisc : (4 * a * a * a + 27 * b * b) * inv % n = 1) (hcurve : onCurve n a b x y = true) : ∃ (P : (shortCurve p a b).toAffine.Point), Point.Rep p a b (Point.affine x y) P ∧ P ≠ 0

The checked starting point represents a nonidentity group element over every prime divisor of the candidate.

theorem Hex.ECPP.secant_slope {p n a b x₁ y₁ x₂ y₂ : ℕ} [Fact (_root_.Nat.Prime p)] (hp : p ∣ n) (hn : 0 < n) (hne : ↑x₁ ≠ ↑x₂) : (shortCurve p a b).toAffine.slope ↑x₁ ↑x₂ ↑y₁ ↑y₂ = ↑(modSub n y₂ y₁) / ↑(modSub n x₂ x₁)

The witness quotient in the distinct-abscissa branch is Mathlib's secant slope.

theorem Hex.ECPP.tangent_slope {p n a b x y u : ℕ} [Fact (_root_.Nat.Prime p)] (hp : p ∣ n) (hu : 2 * y % n * u % n = 1) : (shortCurve p a b).toAffine.slope ↑x ↑x ↑y ↑y = ↑((3 * x * x + a) % n) / ↑(2 * y % n)

The witness quotient in the equal-point branch is Mathlib's tangent slope. The inverse witness excludes a vertical tangent in every field.

theorem Hex.ECPP.formula_rep {p a b x₁ y₁ x₂ y₂ X Y : ℕ} [Fact (_root_.Nat.Prime p)] (h₁ : (shortCurve p a b).toAffine.Nonsingular ↑x₁ ↑y₁) (h₂ : (shortCurve p a b).toAffine.Nonsingular ↑x₂ ↑y₂) (hxy : ¬(↑x₁ = ↑x₂ ∧ ↑y₁ = (shortCurve p a b).toAffine.negY ↑x₂ ↑y₂)) (hx : ↑X = (shortCurve p a b).toAffine.addX (↑x₁) (↑x₂) ((shortCurve p a b).toAffine.slope ↑x₁ ↑x₂ ↑y₁ ↑y₂)) (hy : ↑Y = (shortCurve p a b).toAffine.addY (↑x₁) (↑x₂) (↑y₁) ((shortCurve p a b).toAffine.slope ↑x₁ ↑x₂ ↑y₁ ↑y₂)) : Point.Rep p a b (Point.affine X Y) (WeierstrassCurve.Affine.Point.some (↑x₁) (↑y₁) h₁ + WeierstrassCurve.Affine.Point.some (↑x₂) (↑y₂) h₂)

If raw coordinates equal Mathlib's affine addition formulas, they represent the actual group sum.

theorem Hex.ECPP.secant_rep {p n a b x₁ y₁ x₂ y₂ : ℕ} [Fact (_root_.Nat.Prime p)] {ws rest : List ℕ} {R : Point} (hp : p ∣ n) (hn : 0 < n) (h₁ : (shortCurve p a b).toAffine.Nonsingular ↑x₁ ↑y₁) (h₂ : (shortCurve p a b).toAffine.Nonsingular ↑x₂ ↑y₂) (h : addWithInverse n x₁ y₁ x₂ (modSub n x₂ x₁) (modSub n y₂ y₁) ws = some (R, rest)) : Point.Rep p a b R (WeierstrassCurve.Affine.Point.some (↑x₁) (↑y₁) h₁ + WeierstrassCurve.Affine.Point.some (↑x₂) (↑y₂) h₂)

A checked secant branch is the actual affine group sum in every prime residue field.

theorem Hex.ECPP.tangent_rep {p n a b x y : ℕ} [Fact (_root_.Nat.Prime p)] {ws rest : List ℕ} {R : Point} (hp : p ∣ n) (hn : 0 < n) (hpoint : (shortCurve p a b).toAffine.Nonsingular ↑x ↑y) (h : addWithInverse n x y x (2 * y % n) ((3 * x * x + a) % n) ws = some (R, rest)) : Point.Rep p a b R (WeierstrassCurve.Affine.Point.some (↑x) (↑y) hpoint + WeierstrassCurve.Affine.Point.some (↑x) (↑y) hpoint)

A checked tangent branch is the actual affine group sum in every prime residue field.

theorem Hex.ECPP.add_rep {p n a b : ℕ} [Fact (_root_.Nat.Prime p)] (hp : p ∣ n) (hn : 0 < n) {P Q R : Point} {U V : (shortCurve p a b).toAffine.Point} {ws rest : List ℕ} (hP : Point.Rep p a b P U) (hQ : Point.Rep p a b Q V) (h : add? n a P Q ws = some (R, rest)) : Point.Rep p a b R (U + V)

Every accepted raw addition agrees with Mathlib's group law after reduction to a prime divisor.