Důkaz asociativity sčítání bodů na eliptické křivce

Číslování lemmat i značení odpovídá textu práce
(s jednou výjimkou: pro směrnice přímek z výpočtu s, t, u, v použijeme označení (Subscript[m, 1]),(Subscript[m, 2]),(Subscript[m, 3]),(Subscript[m, 4])).

Lemma 3

(* vyčištění proměnných *)
ClearAll["Global`*"]

(* výpočet s, t, u, v *)

m1=(y2-y1)/(x2-x1);
x4=m1^2-x1-x2;
y4=m1(x1-x4)-y1;
m2=(y3-y4)/(x3-x4);
s=m2^2-x4-x3;
t=m2(x4-s)-y4;

m3=(y3-y2)/(x3-x2);
x5=m3^2-x2-x3;
y5=m3(x2-x5)-y2;
m4=(y5-y1)/(x5-x1);
u=m4^2-x1-x5;
v=m4(x1-u)-y1;

Print[s]

Print[t]

Print[u]

Print[v]

(* s, t ve tvaru zlomku; pro přehlednost vytiskneme pouze jmenovatele *)

jmenovatelS= Denominator[Together[s]];
Print[jmenovatelS]

jmenovatelT= Denominator[Together[t]];
Print[jmenovatelT]

jmenovatelU= Denominator[Together[u]];
Print[jmenovatelU]

jmenovatelV= Denominator[Together[v]];
Print[jmenovatelV]

(* upravíme jmenovatele do přijatelnějšího tvaru *)

Print[FullSimplify[jmenovatelS]]

Print[FullSimplify[jmenovatelT]]

Print[FullSimplify[jmenovatelU]]

Print[FullSimplify[jmenovatelV]]

(* na základě výstupů výše definujeme p, q *)
p=-(x1-x2)^2(x1+x2+x3)+(y1-y2)^2;
q=(x2-x3)^2(x1+x2+x3)-(y2-y3)^2;

(* výpočet největšího společného dělitele (p^2)(q^2)(s-u), (p^3)(q^3)(t-v) *)
gcd=PolynomialGCD[p^2q^2(s-u), p^3q^3(t-v)];
Print[gcd]

(* upravíme gcd do přijatelnějšího tvaru *)
Print[Factor[x1^3 x2-x1 x2^3-x1^3 x3+x2^3 x3+x1 x3^3-x2 x3^3]+Collect[-x2 y1^2+x3 y1^2+x1 y2^2-x3 y2^2-x1 y3^2+x2 y3^2,{y1,y2,y3}] ]

(* na základě výstupu výše definujeme r *)
r=(x1-x2)(x2-x3)(x1-x3)(x1+x2+x3)+(x3-x2)y1^2+(x1-x3)y2^2+(x2-x1)y3^2;

(* nyní ověříme, že platí r = 0, pokud předpokládáme ((Subscript[y, i])^2)=((Subscript[x, i])^3)+(Subscript[Ax, i])+B, i = 1, 2, 3 *)
rId=Expand[r/.{y1^2->x1^3+A x1+B, y2^2->x2^3+A x2+B,y3^2->x3^3+A x3+B}];
Print[rId]

Lemma 4

(* vyčištění proměnných *)
ClearAll["Global`*"]

(* výpočet s, t, u, v *)

m1=(3x1^2+A)/(2y1);
x4=m1^2-2x1;
y4=m1(x1-x4)-y1;
m2=(y3-y4)/(x3-x4);
s=m2^2-x4-x3;
t=m2(x4-s)-y4;

m3=(y3-y1)/(x3-x1);
x5=m3^2-x1-x3;
y5=m3(x1-x5)-y1;
m4=(y5-y1)/(x5-x1);
u=m4^2-x1-x5;
v=m4(x1-u)-y1;

Print[s]

Print[t]

Print[u]

Print[v]

(* s, t ve tvaru zlomku; pro přehlednost vytiskneme pouze jmenovatele *)

jmenovatelS= Denominator[Together[s]];
Print[jmenovatelS]

jmenovatelT= Denominator[Together[t]];
Print[jmenovatelT]

jmenovatelU= Denominator[Together[u]];
Print[jmenovatelU]

jmenovatelV= Denominator[Together[v]];
Print[jmenovatelV]

(* upravíme jmenovatele do přijatelnějšího tvaru *)

Print[FullSimplify[jmenovatelS]]

Print[FullSimplify[jmenovatelT]]

Print[FullSimplify[jmenovatelU]]

Print[FullSimplify[jmenovatelV]]

(* na základě výstupů výše definujeme p, q *)
p=(A+3 x1^2)^2-4y1^2(2x1+x3);
q=-(x1-x3)^2 (2 x1+x3)+(y1-y3)^2;

(* výpočet největšího společného dělitele (p^2)(q^2)(s-u), (p^3)(q^3)(t-v) *)
gcd=PolynomialGCD[p^2q^2(s-u), p^3q^3(t-v)];
Print[gcd]

(* upravíme gcd do přijatelnějšího tvaru *)
Print[FullSimplify[2(A x1 y1+x1^3 y1-A x3 y1-x3^3 y1-y1^3+y1 y3^2)]]

(* na základě výstupu výše definujeme r *)
r=2y1(x1^3+A (x1-x3)-x3^3-y1^2+y3^2);

(* nyní ověříme, že platí r = 0, pokud předpokládáme ((Subscript[y, i])^2) = ((Subscript[x, i])^3)+(Subscript[Ax, i])+B, i=1, 2, 3 *)
rId=Expand[r/.{y1^2->x1^3+A x1+B, y2^2->x2^3+A x2+B,y3^2->x3^3+A x3+B}];
Print[rId]

Lemma 5

(* vyčištění proměnných *)
ClearAll["Global`*"]

(* výpočet s, t, u, v *)

m1=(3x1^2+A)/(2y1);
x4=m1^2-2x1;
y4=m1(x1-x4)-y1;
m2=(3x4^2+A)/(2y4);
s=m2^2-2x4;
t=m2(x4-s)-y4;

m3=(y4-y1)/(x4-x1);
x5=m3^2-x1-x4;
y5=m3(x1-x5)-y1;
m4=(y5-y1)/(x5-x1);
u=m4^2-x1-x5;
v=m4(x1-u)-y1;

(* přímý výpočet s-u, t-v *)

Print[Simplify[s-u]]

Print[Simplify[t-v]]