:: Set of Points on Elliptic Curve in Projective Coordinates
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 21, 2010
:: Copyright (c) 2010-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, CARD_1, FUNCT_1, RELAT_1, XBOOLE_0, ARYTM_3, NEWTON,
TARSKI, FINSET_1, CARD_3, FINSEQ_1, SUBSET_1, ARYTM_1, XXREAL_0, FUNCT_2,
PARTFUN1, INT_2, NAT_1, BINOP_1, BINOP_2, REALSET1, ZFMISC_1, INT_3,
SUPINF_2, ALGSTR_0, GROUP_1, MESFUNC1, INT_1, VECTSP_1, STRUCT_0,
GROUP_2, GRAPH_1, FINSEQ_2, EC_PF_1, RLVECT_1, LATTICES, EQREL_1,
RELAT_2, UNIROOTS, PROB_2, MOD_2, RECDEF_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELAT_2,
RELSET_1, PARTFUN1, XTUPLE_0, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1,
FINSET_1, CARD_3, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1,
INT_1, NAT_D, REALSET1, FINSEQ_1, FINSEQ_2, EQREL_1, RVSUM_1, NEWTON,
WSIERP_1, MOD_2, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1,
GROUP_2, GR_CY_1, INT_3, UNIROOTS, PROB_2, BINOM;
constructors NAT_D, REALSET1, GROUP_2, BINOP_1, GR_CY_1, INT_3, WSIERP_1,
UPROOTS, BINOP_2, RELSET_1, FUNCT_7, UNIROOTS, PROB_2, BINOM, MOD_2,
XTUPLE_0, NUMBERS, NEWTON;
registrations XBOOLE_0, STRUCT_0, XREAL_0, ORDINAL1, NAT_1, INT_1, GROUP_2,
FINSET_1, ALGSTR_0, VECTSP_1, INT_3, XXREAL_0, NEWTON, SUBSET_1, CARD_1,
RELAT_2, VALUED_0, EQREL_1, RELSET_1, FINSEQ_2, UNIROOTS, NUMBERS,
MEMBERED, XTUPLE_0, MCART_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: 1.Finite Prime Field $\bf{GF}(p)$
reserve x for set;
reserve i,j for Integer;
reserve n,n1,n2,n3 for Nat;
reserve K,K1,K2,K3 for Field;
definition
let K be Field;
mode Subfield of K -> Field means
:: EC_PF_1:def 1
the carrier of it c= the carrier of K
& the addF of it = (the addF of K) || the carrier of it
& the multF of it = (the multF of K) || the carrier of it
& 1.it = 1.K & 0.it = 0.K;
end;
theorem :: EC_PF_1:1
K is Subfield of K;
theorem :: EC_PF_1:2
for ST be non empty doubleLoopStr
st the carrier of ST is Subset of the carrier of K
& the addF of ST = (the addF of K) || (the carrier of ST)
& the multF of ST = (the multF of K) || (the carrier of ST)
& 1.ST = 1.K & 0.ST = 0.K
& ST is right_complementable commutative almost_left_invertible
non degenerated holds ST is Subfield of K;
registration let K be Field;
cluster strict for Subfield of K;
end;
reserve SK1,SK2 for Subfield of K;
reserve ek,ek1,ek2 for Element of K;
theorem :: EC_PF_1:3
K1 is Subfield of K2 implies for x st x in K1 holds x in K2;
theorem :: EC_PF_1:4
for K1,K2 be strict Field st
K1 is Subfield of K2 & K2 is Subfield of K1 holds K1 = K2;
theorem :: EC_PF_1:5
for K1, K2, K3 be Field st
K1 is Subfield of K2 & K2 is Subfield of K3 holds K1 is Subfield of K3;
theorem :: EC_PF_1:6
SK1 is Subfield of SK2 iff the carrier of SK1 c= the carrier of SK2;
theorem :: EC_PF_1:7
SK1 is Subfield of SK2 iff for x st x in SK1 holds x in SK2;
theorem :: EC_PF_1:8
for SK1,SK2 be strict Subfield of K holds
SK1 = SK2 iff the carrier of SK1 = the carrier of SK2;
theorem :: EC_PF_1:9
for SK1, SK2 be strict Subfield of K holds
(SK1 = SK2 iff for x holds x in SK1 iff x in SK2);
registration
let K be finite Field;
cluster finite for Subfield of K;
end;
definition
let K be finite Field;
redefine func card K -> Element of NAT;
end;
registration
cluster strict finite for Field;
end;
theorem :: EC_PF_1:10
for K be strict finite Field,
SK1 be strict Subfield of K st
card K = card SK1 holds SK1 = K;
definition let IT be Field;
attr IT is prime means
:: EC_PF_1:def 2
K1 is strict Subfield of IT implies K1 = IT;
end;
notation let p be Prime;
synonym GF(p) for INT.Ring(p);
end;
registration let p be Prime;
cluster GF(p) -> finite;
end;
registration let p be Prime;
cluster GF(p) -> prime;
end;
registration
cluster prime for Field;
end;
begin :: 2. Arithmetic in $\bf{GF}(p)$
reserve p for Prime;
reserve a,b,c for Element of GF(p);
reserve F for FinSequence of GF(p);
theorem :: EC_PF_1:11
0 = 0.(GF p);
theorem :: EC_PF_1:12
1 = 1.(GF p);
theorem :: EC_PF_1:13
ex n1 st a = n1 mod p;
theorem :: EC_PF_1:14
i mod p is Element of GF(p);
theorem :: EC_PF_1:15
a = i mod p & b = j mod p implies a+b = (i+j) mod p;
theorem :: EC_PF_1:16
a = i mod p implies -a = (p-i) mod p;
theorem :: EC_PF_1:17
a = i mod p & b = j mod p implies a-b = (i-j) mod p;
theorem :: EC_PF_1:18
a = i mod p & b = j mod p implies a*b = (i*j) mod p;
theorem :: EC_PF_1:19
a = i mod p & i*j mod p = 1 implies a" = j mod p;
theorem :: EC_PF_1:20
a = 0 or b = 0 iff a*b = 0;
theorem :: EC_PF_1:21
a |^ 0 = 1_GF(p) & a |^ 0 = 1;
theorem :: EC_PF_1:22
a |^ 2 = a*a;
theorem :: EC_PF_1:23
a = n1 mod p implies a|^n = n1|^n mod p;
theorem :: EC_PF_1:24
for K being unital associative non empty multMagma, a being
Element of K, n being Nat holds a|^(n+1) = (a|^n) * a;
theorem :: EC_PF_1:25
a <> 0 implies a |^ n <> 0;
theorem :: EC_PF_1:26
for F being Abelian add-associative right_zeroed right_complementable
associative commutative well-unital almost_left_invertible distributive
non empty doubleLoopStr, x,y being Element of F holds x*x=y*y
iff x=y or x=-y;
theorem :: EC_PF_1:27
for p be Prime, x be Element of GF(p) st 2 < p & x+x = 0.(GF p)
holds x = 0.(GF(p));
theorem :: EC_PF_1:28
a <> 0 implies (a") |^n = (a|^n)";
registration let p;
cluster MultGroup GF(p) -> cyclic;
end;
theorem :: EC_PF_1:29
for x be Element of MultGroup GF(p), x1 be Element of GF(p),
n be Nat st x = x1 holds x|^n = x1 |^n;
theorem :: EC_PF_1:30
ex g be Element of GF(p) st
for a be Element of GF(p) st a <> 0.GF(p) holds
ex n be Nat st a = g|^n;
begin :: 3.Relation between Legendre symbol and the number of roots in $\bf{GF}(p)$
definition let p, a;
attr a is quadratic_residue means
:: EC_PF_1:def 3
a <> 0 & ex x being Element of GF(p) st x|^2 = a;
attr a is not_quadratic_residue means
:: EC_PF_1:def 4
a <> 0 & not ex x being Element of GF(p) st x|^2 = a;
end;
theorem :: EC_PF_1:31
a <> 0 implies a|^2 is quadratic_residue;
registration let p be Prime;
cluster 1.(GF p) -> quadratic_residue;
end;
definition let p, a;
func Lege_p(a) -> Integer equals
:: EC_PF_1:def 5
0 if a = 0,
1 if a is quadratic_residue
otherwise -1;
end;
theorem :: EC_PF_1:32
a is not_quadratic_residue iff Lege_p(a) = -1;
theorem :: EC_PF_1:33
a is quadratic_residue iff Lege_p(a) = 1;
theorem :: EC_PF_1:34
a = 0 iff Lege_p(a) = 0;
theorem :: EC_PF_1:35
a <> 0 implies Lege_p(a|^2) = 1;
theorem :: EC_PF_1:36
Lege_p(a*b) = Lege_p(a) * Lege_p(b);
theorem :: EC_PF_1:37
a <> 0 & n mod 2 = 0 implies Lege_p(a|^n) = 1;
theorem :: EC_PF_1:38
n mod 2 = 1 implies Lege_p(a|^n) = Lege_p(a);
theorem :: EC_PF_1:39
2 < p implies card({b : b|^2 = a}) = 1 + Lege_p(a);
begin :: 4.Set of points on an elliptic curve over $\bf{GF}(p)$
definition let K be Field;
func ProjCo(K) -> non empty Subset of
[:the carrier of K, the carrier of K, the carrier of K:] equals
:: EC_PF_1:def 6
[:the carrier of K, the carrier of K, the carrier of K:] \ {[0.K,0.K,0.K]};
end;
theorem :: EC_PF_1:40
ProjCo(GF(p)) = [:the carrier of GF(p),
the carrier of GF(p), the carrier of GF(p):] \ {[0,0,0]};
reserve Px,Py,Pz for Element of GF(p);
definition
let p be Prime;
let a, b be Element of GF(p);
func Disc(a,b,p) -> Element of GF(p) means
:: EC_PF_1:def 7
for g4, g27 be Element of GF(p) st g4 = 4 mod p & g27 = 27 mod p
holds it = g4*a|^3 + g27*b|^2;
end;
definition
let p be Prime;
let a, b be Element of GF(p);
func EC_WEqProjCo(a,b,p) -> Function of
[:the carrier of GF(p), the carrier of GF(p), the carrier of GF(p):],
GF(p) means
:: EC_PF_1:def 8
for P be Element of [:the carrier of GF(p),
the carrier of GF(p), the carrier of GF(p):] holds
it. P = ((P`2_3) |^2)*(P`3_3)-((P`1_3) |^3
+a*(P`1_3)*(P`3_3) |^2+b*(P`3_3) |^3);
end;
theorem :: EC_PF_1:41
for X,Y,Z be Element of GF(p) holds
EC_WEqProjCo(a,b,p).([X,Y,Z]) = Y |^2*Z-(X|^3 +a*X*Z |^2+b*Z |^3);
definition
let p be Prime;
let a, b be Element of GF(p);
func EC_SetProjCo(a,b,p) -> non empty Subset of ProjCo(GF(p)) equals
:: EC_PF_1:def 9
{P where P is Element of ProjCo(GF(p)) : EC_WEqProjCo(a,b,p).P = 0.GF(p) };
end;
theorem :: EC_PF_1:42
[0,1,0] is Element of EC_SetProjCo(a,b,p);
theorem :: EC_PF_1:43
for p be Prime, a, b, X, Y be Element of GF(p) holds
Y|^2 = X|^3 + a*X + b iff [X,Y,1] is Element of EC_SetProjCo(a,b,p);
definition
let p be Prime;
let P,Q be Element of ProjCo(GF(p));
pred P _EQ_ Q means
:: EC_PF_1:def 10
ex a be Element of GF(p) st a <> 0.GF(p)
& P`1_3 = a*(Q`1_3) & P`2_3 = a*(Q`2_3) & P`3_3 = a*(Q`3_3);
reflexivity;
symmetry;
end;
theorem :: EC_PF_1:44
for p be Prime, P,Q,R be Element of ProjCo(GF(p)) holds
( P _EQ_ Q & Q _EQ_ R implies P _EQ_ R);
theorem :: EC_PF_1:45
for p be Prime, a, b be Element of GF(p),
P,Q be Element of [:the carrier of GF(p), the carrier of GF(p),
the carrier of GF(p):], d be Element of GF(p)
st p > 3 & Disc(a,b,p) <> 0.GF(p) &
P in EC_SetProjCo(a,b,p) & d <> 0.GF(p)
& Q`1_3 = d*(P`1_3) & Q`2_3 = d*(P`2_3) & Q`3_3 = d*(P`3_3) holds
Q in EC_SetProjCo(a,b,p);
definition
let p be Prime;
func R_ProjCo p -> Relation of ProjCo(GF(p)) equals
:: EC_PF_1:def 11
{[P,Q] where P,Q is Element of ProjCo(GF(p)) : P _EQ_ Q};
end;
theorem :: EC_PF_1:46
for p be Prime, P,Q be Element of ProjCo(GF(p)) holds
P _EQ_ Q iff [P,Q] in R_ProjCo p;
registration let p be Prime;
cluster R_ProjCo p -> total symmetric transitive;
end;
definition
let p be Prime;
let a, b be Element of GF(p);
func R_EllCur (a,b,p) -> Equivalence_Relation of EC_SetProjCo(a,b,p)
equals
:: EC_PF_1:def 12
(R_ProjCo p) /\ nabla EC_SetProjCo(a,b,p);
end;
theorem :: EC_PF_1:47
for p be Prime, a, b be Element of GF(p),
P,Q be Element of ProjCo(GF(p))
st Disc(a,b,p) <> 0.GF(p) &
P in EC_SetProjCo(a,b,p) & Q in EC_SetProjCo(a,b,p) holds
( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p));
theorem :: EC_PF_1:48
for p be Prime, a, b be Element of GF(p),
P be Element of ProjCo(GF(p))
st p > 3 & Disc(a,b,p) <> 0.GF(p) &
P in EC_SetProjCo(a,b,p) & P`3_3 <> 0 holds
ex Q be Element of ProjCo(GF(p)) st Q in EC_SetProjCo(a,b,p)
& Q _EQ_ P & Q`3_3 = 1;
theorem :: EC_PF_1:49
for p be Prime, a, b be Element of GF(p),
P be Element of ProjCo(GF(p))
st p > 3 & Disc(a,b,p) <> 0.GF(p) &
P in EC_SetProjCo(a,b,p) & P`3_3 = 0 holds
ex Q be Element of ProjCo(GF(p))
st Q in EC_SetProjCo(a,b,p) & Q _EQ_ P & Q`1_3 = 0 & Q`2_3= 1 & Q`3_3= 0;
theorem :: EC_PF_1:50
for p be Prime, a, b be Element of GF(p), x be set st
p > 3 & Disc(a,b,p) <> 0.GF(p)
& x in Class (R_EllCur(a,b,p)) holds
( ex P be Element of ProjCo(GF(p)) st P in EC_SetProjCo(a,b,p) & P=[0,1,0]
& x = Class(R_EllCur(a,b,p),P) ) or
ex P be Element of ProjCo(GF(p)), X,Y be Element of GF(p)
st P in EC_SetProjCo(a,b,p) & P=[X,Y,1]
& x = Class(R_EllCur(a,b,p),P);
theorem :: EC_PF_1:51
for p be Prime, a, b be Element of GF(p) st
p > 3 & Disc(a,b,p) <> 0.GF(p) holds
Class (R_EllCur(a,b,p)) = {Class(R_EllCur(a,b,p),[0,1,0])}
\/ {Class(R_EllCur(a,b,p),P)
where P is Element of ProjCo(GF(p)):
P in EC_SetProjCo(a,b,p) & ex X,Y be Element of GF(p) st P=[X,Y,1]};
theorem :: EC_PF_1:52
for p be Prime,
a, b,d1,Y1,d2,Y2 be Element of GF(p)
st p > 3 & Disc(a,b,p) <> 0.GF(p)
& [d1,Y1,1] in EC_SetProjCo(a,b,p)
& [d2,Y2,1] in EC_SetProjCo(a,b,p) holds
Class(R_EllCur(a,b,p),[d1,Y1,1]) = Class(R_EllCur(a,b,p),[d2,Y2,1])
iff d1=d2 & Y1=Y2;
theorem :: EC_PF_1:53
for p be Prime, a, b be Element of GF(p),
F1,F2 be set st p > 3 & Disc(a,b,p) <> 0.GF(p)
& F1 = {Class(R_EllCur(a,b,p),[0,1,0])} & F2 = {Class(R_EllCur(a,b,p),P)
where P is Element of ProjCo(GF(p)):
P in EC_SetProjCo(a,b,p) &
ex X,Y be Element of GF(p) st P=[X,Y,1]} holds F1 misses F2;
theorem :: EC_PF_1:54
for X be non empty finite set,
R be Equivalence_Relation of X,
S be Class(R)-valued Function, i be set st i in dom S holds
S.i is finite Subset of X;
theorem :: EC_PF_1:55
for X be non empty set,
R be Equivalence_Relation of X,
S be Class(R)-valued Function st S is one-to-one
holds S is disjoint_valued;
theorem :: EC_PF_1:56
for X be non empty set,
R be Equivalence_Relation of X,
S be Class(R)-valued Function st S is onto
holds Union S = X;
theorem :: EC_PF_1:57
for X be non empty finite set,
R be Equivalence_Relation of X,
S be Class(R)-valued Function,
L be FinSequence of NAT
st S is one-to-one onto & dom S = dom L
& (for i be Nat st i in dom S holds L.i = card (S.i))
holds card (X) = Sum L;
theorem :: EC_PF_1:58
for p be Prime, a, b,d be Element of GF(p), F,G be set st
p > 3 & Disc(a,b,p) <> 0.GF(p)
& F = {Y where Y is Element of GF(p) : Y|^2= d|^3 + a*d + b} & F <> {}
& G = {Class(R_EllCur(a,b,p),[d,Y,1])
where Y is Element of GF(p) : [d,Y,1] in EC_SetProjCo(a,b,p) } holds
ex I be Function of F,G st I is onto & I is one-to-one;
theorem :: EC_PF_1:59
for p be Prime, a, b, d be Element of GF(p) st
p > 3 & Disc(a,b,p) <> 0.GF(p) holds
card ({Class(R_EllCur(a,b,p),[d,Y,1]) where Y is Element of GF(p)
: [d,Y,1] in EC_SetProjCo(a,b,p) }) = 1 + Lege_p(d|^3 + a*d + b);
theorem :: EC_PF_1:60
for p be Prime, a, b be Element of GF(p)
st p > 3 & Disc(a,b,p) <> 0.GF(p) holds
ex F be FinSequence of NAT st len F = p
& (for n be Nat st n in Seg p
ex d be Element of GF(p) st d=n-1 & F.n = 1 + Lege_p(d|^3 + a*d + b))
& card {Class(R_EllCur(a,b,p),P)
where P is Element of ProjCo(GF(p)): P in EC_SetProjCo(a,b,p) &
ex X,Y be Element of GF(p) st P=[X,Y,1]} = Sum(F);
theorem :: EC_PF_1:61
for p be Prime, a, b be Element of GF(p)
st p > 3 & Disc(a,b,p) <> 0.GF(p)
ex F be FinSequence of INT st len F = p &
(for n be Nat st n in Seg p ex d be Element of GF(p)
st d=n-1 & F.n = Lege_p(d|^3 + a*d + b)) &
card(Class(R_EllCur(a,b,p))) = 1 + p + Sum(F);