Hi Metakunt!
This looks quite good - my remarks:
- you'll probably need to add additional properties of the field `K` for
the claims (i), (ii) or (iii)
- I think B should be ( Base ` R ) instead (that's the set of
polynomials considered)
- for the exponentiation operation D, you could use the class variable
`.^` , it might make things a bit clearer,
- do you really need negative exponents? Would Q C_ NN0 instead of Q C_
ZZ suffice ?
- I would probably have formalized this in a more direct way: for
example take a concrete `G : ZZ --> NN0`, and directly assume its
properties:
|- ph -> G : ZZ --> NN0
|- ph -> ( G supp 0 ) e. Fin ( you don't need ( G supp 0 ) C_ ZZ ,
you can deduce it from its domain )
- same for I and x: I would have taken a F instead of ( 2nd ` x ) and an
E instead of ( 1st ` x ) (assuming we free the letters!):
|- ph -> F e. B <or some other smaller set depending on (i), (ii),
(iii) >
|- ph -> E e. NN <or some other smaller set depending on (i), (ii),
(iii) >
- same for r, let's take a concrete \mu (say, Y) :
|- ph -> Y e. ( Base ` K )
|- ph -> ( S D Y ) = ( 1r ` K ) (taking S for r)
- you also need conditions on S, like 2 <_ S, ( S gcd N ) = 1, etc.,
which I don't see in your statement. Maybe you could swap my S and R to
keep the same letters as in the paper!
Then your final statement becomes:
qed:: |- ph -> ( E .^ ( ( O ` F ) ` Y ) ) = ( ( ( O ` F ) ` ( E D Y ) ) )
(maybe it would be even more readable if we declare an alias for ( O ` F
),but we already have eaten through many letters of the alphabet here!)
The fact that you have taken e.g. any F e. B makes it equivalent to
proving A. f e. B ..., and I think this formulation is clearer. It's
also similar to the literature's "let F be a polynomial..."
If you need to have a relation .~ like in the paper, you can also write:
.~ = { <. e , f >. | ( ( e e. NN /\ f e. B ) /\ ( e .^ ( ( O ` f ) ` Y )
) = ( ( ( O ` f ) ` ( e D Y ) ) ) ) }
Then you can use .~ in your proof, and your final statement becomes:
qed:: |- ph -> E .~ F
In that case, a first useful lemma will be to explicit the relation:
qed:: |- ph -> ( E .~ F <-> ( E .^ ( ( O ` F ) ` Y ) ) = ( ( ( O ` F ) `
( E D Y ) ) ) )
Which is even clearer.
(I've dropped a few parentheses around the ( ph -> ... ) !)
So, to sum it all up, your conditions would become approximately:
1:: |- .~ = { <. e , y >. | ( ( e e. NN /\ f e. B ) /\ ( e .^ ( ( O ` f
) ` Y ) ) = ( ( ( O ` f ) ` ( e D Y ) ) ) ) }
2:: |- S = ( Poly1 ` K )
3:: |- B = ( Base ` S )
4:: |- X = ( var1 ` S )
5:: |- W = ( mulGrp ` S )
6:: |- V = ( mulGrp ` K )
7:: |- .^ = ( .g ` V )
8:: |- C = ( algSc ` W )
9:: |- D = ( .g ` W )
10:: |- P = ( chr ` K )
11:: |- O = ( eval1 ` K )
12:: |- .- = ( -g ` S )
12:: |- ( ph -> K e. Field )
13:: |- ( ph -> P e. Prime )
14:: |- ( ph -> R e. ( ZZ>_ ` 2 ) )
15:: |- ( ph -> ( N gcd R ) = 1 )
16:: |- ( ph -> P || N )
<more conditions on N, I assume ?>
First lemma:
18:: |- ( ph -> F e. B )
19:: |- ( ph -> E e. NN )
qed:: |- ( ph -> ( E .~ F <-> ( E .^ ( ( O ` F ) ` Y ) ) = ( ( ( O ` F )
` ( E D Y ) ) ) )
Statements for (i), (ii), (iii):
<additional conditions on F and E>
qed:: |- ( ph -> E .~ F )
Maybe for (ii) something like:
20:: |- ( ph -> M e. NN )
21:: |- ( ph -> G : ( 0 ..^ M ) --> NN0 )
22:: |- ( ph -> F = ( V gsum ( x e. ( 0 ..^ M ) |-> ( X .- ( C ` ( (
ZRHom ` K ) ` ( G ` x ) ) ) )
23:: |- ( ph -> I e. NN0 )
24:: |- ( ph -> J e. NN0 )
25:: |- ( ph -> E = ( ( N / P ) ^ I ) .x. ( P ^ J ) )
qed:: |- ( ph -> E .~ F )
I hope this is clear!
BR,
_
Thierry
On 10/04/2025 21:50, 'Meta Kunt' via Metamath wrote:
Would you check if the following matches the definition of Claim 1 in 6.1?
I've tried, painstakingly, to match the definitions. A typo now would
be horrific.
Reference: https://www3.nd.edu/~andyp/notes/AKS.pdf
1:: |- ( ph -> K e. Field )
2:: |- R = ( Poly1 ` K )
3:: |- B = ( Base ` K )
4:: |- X = ( var1 ` K )
5:: |- W = ( mulGrp ` R )
6:: |- M = ( mulGrp ` K )
7:: |- D = ( .g ` M )
8:: |- C = ( algSc ` W )
9:: |- E = ( .g ` W )
10:: |- P = ( chr ` K )
11:: |- ( ph -> ( Q C_ ZZ /\ Q e. Fin ) )
12:: |- F = { g | ( g : ZZ --> NN0 /\ ( g supp 0 ) = Q ) }
13:: |- ( ph -> P e. Prime )
14:: |- I = { x e. ( NN X. B ) | A. r e. S th }
15:: |- O = ( eval1 ` K )
16:: |- .- = ( -g ` R )
17:: |- T = ( f e. F |-> ( W gsum ( z e. ZZ |-> ( ( f ` z ) E ( X .- (
C ` ( ( ZRHom ` K ) ` z ) ) ) ) ) ) )
18:: |- ( th <-> ( ( 1st ` x ) D ( ( O ` ( 2nd ` x ) ) ` r ) ) = ( (
O ` ( 2nd ` x ) ) ` ( ( 1st ` x ) D r ) ) )
The explanation for the following lines.
1: K is a field, in our case it will be an algebraic closure of Fp, I
think we'll need the Euclidean ring.
2: R=K[X], the polynomial ring in one variable
3: B are the elements of K[X]
4: The monomial X of K[X]
5: W is the multiplicative monoid of K[X] with the multiplication as
operation (+g)
6: M, but with the Field K.
7: Group exponentiation of K. in CC ( 3 D 2 ) = ( 2 ^ 3 ) = 9
8: The scalars of K[X], which is "left scalar multiplication with K"
9: Same, but with the polynomial ring K[X], for example in Z[X] ( 2 E
( X + 1 ) ) = ( X^2+2X+1) (informally)
10,13: K with prime characteristic.
11: A finite subset of ZZ, in corresponds to the following integers 0
≤ ai ≤ ⌊pϕ(r) log n⌋ (11 INFO)
12: This is a bit more complicated, this is data necessary to define
P. Here is an example: assume f that is in F with f(2)=3. Then the
polynomial under T would be ( x-2)^3, where the 2 is in K. This
"transfers" information of the monic linear factors to the product of
polynomials in K[X]
14: Definition of the introspective property. In the literature we
have (e,f), we want to say that (e,f) is introspective when for all
r-th primitive roots S, which by abuse of notation we also call r (in
the literature this is \mu) the property 18 holds.
15: Polynomial evaluation of K[X]
16: Polynomial subtraction of K[X]
17: Define the elements of the literature script P as a product of
finitely many linear factors, where the offsets are bounded by [11 INFO]
18: (μ)e ≡ f (μe) in Fp in the literature.
Did I make any mistakes? Hint: I want to show that for every e \in
Literature script E and every f \in Literature script P that e and f
are introspective.
Claim 1(i) shows it for the monomials f=(x-a) and e=n/p, and e=p
Claim 1(ii) shows it for the product of f. In our case this
corresponds to the pointwise sum of elements of F.
Claim 1(iii) shows it for the products of e. Here we need the
properties of primitive roots and the fact that all elements of e are
coprime to r. That's why \mu^e is also a primitive root, see the
definition of 14 and recall that in this definition S stands for
primitive roots.
If everything is fine I would like to formalise the statements and
collect some more feedback before I start to formalising Claim 1. In
our Case, transcribed it would be ( ph -> A. e e. ( (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0
↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) `` ( NN0 X. NN0 )) A. f e. ( T `` F ) -> e I f )
Feedback would be immensely helpful, as I need to put several
definitions in place, in particular I will need PerfectRings,
PrimitiveRoots, maybe even roots of unity. I don't know yet what API I
will need to formalise before I can tackle this statement.
------------------------------------------------------------------------
Your E-Mail. Your Cloud. Your Office. *eclipso Mail Europe
<https://www.eclipso.eu>*.
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send
an email to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/529b6b8d724cff6c3a66478989cc8f0a%40mail.eclipso.de
<https://groups.google.com/d/msgid/metamath/529b6b8d724cff6c3a66478989cc8f0a%40mail.eclipso.de?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/72a34a3b-9a37-4279-ad9e-5fce6e029333%40gmx.net.
