From 0e32fdb1889850bd1b75759eb95857d6ac94c94a Mon Sep 17 00:00:00 2001
From: metakunt <166170055+metakunt@users.noreply.github.com>
Date: Tue, 27 Aug 2024 14:08:57 +0200
Subject: [PATCH] Part of claim 2 (#11)

* Part of claim 2

* Fix escape
---
 AKS (PRIMES is in P)/claim2p1.md | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 AKS (PRIMES is in P)/claim2p1.md

diff --git a/AKS (PRIMES is in P)/claim2p1.md b/AKS (PRIMES is in P)/claim2p1.md
new file mode 100644
index 0000000..92f2125
--- /dev/null
+++ b/AKS (PRIMES is in P)/claim2p1.md	
@@ -0,0 +1,17 @@
++++
+reference = "Part of Claim 2 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+statement = """
+$e |- ( ph -> P e. Prime ) $.
+$e |- X = ( GFoo ` P ) $.
+$e |- B = ( Base ` X ) $.
+$e |- ( ph -> R e. PrimRoot ) $.
+$e |- ( ph -> CurlyPbar = { y e. B | E. f e. CurlyP y = ( f ` R ) } ) $.
+$e |- ( ph -> T = ( ( X ^ M ) - ( X ^ N ) ) ) $.
+$e |- ( ( ph /\\ x e. CurlyPbar ) -> ( T ` x ) = 0 ) $.
+$p |- ( ph -> ( # ` CurlyPBar ) <_ ( ( deg1 ` R ) ` T ) ) $.
+"""
+dependencies = ["fta1g"]
++++
+If every element of CurlyPBar is a root of T, then the elements of CurlyPBar are bound by the degree of T.
+Also, not as a statement, but the degree of T is greater equal than $N^{\sqrt{\bar \mathcal{R}\bar}}$