diff --git a/blueprint/lean_decls b/blueprint/lean_decls
index af7744f..0d9cbb7 100644
--- a/blueprint/lean_decls
+++ b/blueprint/lean_decls
@@ -17,4 +17,5 @@ comm_dist_le
is_archimedean_wrt
is_archimedean
anomalous_pair
-non_archimedean_anomalous_pair
\ No newline at end of file
+non_archimedean_anomalous_pair
+not_anomalous_comm_and_arch
\ No newline at end of file
diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex
index cf92c55..4a0c699 100644
--- a/blueprint/src/content.tex
+++ b/blueprint/src/content.tex
@@ -190,55 +190,56 @@ \section{Content}
The other cases follow similarly.
\end{proof}
-\begin{theorem}
+\begin{theorem}\label{non_anomalous_comm_and_arch}\lean{not_anomalous_comm_and_arch}\leanok
+\uses{def:anomalous_pair, def:arch}
A linear ordered cancel semigroup without anomalous pairs is an Archimedean commutative semigroup.
\end{theorem}
\begin{proof}
Let $a$ and $b$ be elements of an ordered semigroup $S$.
-If either $a$ or $b$ is zero, then they commute.
+If either $a$ or $b$ is one, then they commute.
We begin with the case that $a$ and $b$ are positive.
-If $a + b < b + a$, then for all $n\in \mathbb{N}^+$, we have that
+If $a * b < b * a$, then for all $n\in \mathbb{N}^+$, we have that
\begin{align}
-(n+1)(a+b) &= a + n(b+a) + b \\
-&> n(b+a) + b \\
-&> n(b+a) \\
-&> n(a+b)
+(a*b)^{n+1} &= a * (b*a)^n * b \\
+&> (b*a)^n * b \\
+&> (b*a)^n \\
+&> (a*b)^n
\end{align}
-And so $a+b$ and $b+a$ form an anomalous pair.
+And so $a*b$ and $b*a$ form an anomalous pair.
-The same for the case that $b + a < a + b$.
-Therefore, we must have that $a+b = b+a$.
+The same for the case that $b * a < a * b$.
+Therefore, we must have that $a*b = b*a$.
The case where $a$ and $b$ are negative follows similarly.
We now look at the case where $a$ is negative and $b$ is positive.
-If the element $0$ exists and $a+b = 0$, then $a + b + a = a$ and so $b+a = 0$.
+If the element $1$ exists and $a*b = 1$, then $a * b * a = a$ and so $b*a = 1$.
Therefore, $a$ and $b$ commute.
-If $a + b$ is positive, then
+If $a * b$ is positive, then
\begin{align}
-(a+b) + (a+b) &> a + b \\
-(b + a) + b &> b \\
-b + a &> 0
+(a*b) * (a*b) &> a * b \\
+(b * a) * b &> b \\
+b * a &> 0
\end{align}
We already showed that positive elements commute and so
-\[ (b+a) + b = b + (b + a)\]
+\[ (b*a) * b = b * (b * a)\]
-Now we look at the case where $a+b < b+a$.
+Now we look at the case where $a*b < b*a$.
Then we have that
\begin{align}
-2(a + b) &= a + ((b+a) + b) \\
-&= a + (b + (b + a)) \\
-&= (a + b) + (b + a) \\
-&> (a + b) + (a + b) \\
-&= 2(a + b)
+(a * b)^2 &= a * ((b*a) * b) \\
+&= a * (b * (b * a)) \\
+&= (a * b) * (b * a) \\
+&> (a * b) * (a * b) \\
+&= (a * b)^2
\end{align}
Which is a contradiction.
-We get a similar contradiction in the case that $b+a < a+b$.
-Therefore, $a+b = b+a$.
+We get a similar contradiction in the case that $b*a < a*b$.
+Therefore, $a*b = b*a$.
-The case where $a+b$ is negative follows similarly.
+The case where $a*b$ is negative follows similarly.
The case where $b$ is negative and $a$ is positive is symmetric.
\end{proof}
\ No newline at end of file
diff --git a/blueprint/src/web.paux b/blueprint/src/web.paux
index ad6be9c..cd43293 100644
Binary files a/blueprint/src/web.paux and b/blueprint/src/web.paux differ
diff --git a/blueprint/web/dep_graph_document.html b/blueprint/web/dep_graph_document.html
index 705f570..fde5c03 100644
--- a/blueprint/web/dep_graph_document.html
+++ b/blueprint/web/dep_graph_document.html
@@ -61,36 +61,6 @@
Dependencies
-
-
-
-
-
-
-
- Theorem
-
- 4
-
A linear ordered cancel semigroup without anomalous pairs is an Archimedean commutative semigroup.
A linear ordered cancel semigroup without anomalous pairs is an Archimedean commutative semigroup.
+
A linear ordered cancel semigroup without anomalous pairs is an Archimedean commutative semigroup.
-
+
Proof
@@ -1130,29 +1171,29 @@
Lean declarations
▶
-
Let \(a\) and \(b\) be elements of an ordered semigroup \(S\). If either \(a\) or \(b\) is zero, then they commute.
-
We begin with the case that \(a\) and \(b\) are positive. If \(a + b {\lt} b + a\), then for all \(n\in \mathbb {N}^+\), we have that
-
- \begin{align} (n+1)(a+b) & = a + n(b+a) + b \\ & {\gt} n(b+a) + b \\ & {\gt} n(b+a) \\ & {\gt} n(a+b) \end{align}
+
Let \(a\) and \(b\) be elements of an ordered semigroup \(S\). If either \(a\) or \(b\) is one, then they commute.
+
We begin with the case that \(a\) and \(b\) are positive. If \(a * b {\lt} b * a\), then for all \(n\in \mathbb {N}^+\), we have that
+
+ \begin{align} (a*b)^{n+1} & = a * (b*a)^n * b \\ & {\gt} (b*a)^n * b \\ & {\gt} (b*a)^n \\ & {\gt} (a*b)^n \end{align}
-
And so \(a+b\) and \(b+a\) form an anomalous pair.
-
The same for the case that \(b + a {\lt} a + b\). Therefore, we must have that \(a+b = b+a\).
+
And so \(a*b\) and \(b*a\) form an anomalous pair.
+
The same for the case that \(b * a {\lt} a * b\). Therefore, we must have that \(a*b = b*a\).
The case where \(a\) and \(b\) are negative follows similarly.
-
We now look at the case where \(a\) is negative and \(b\) is positive. If the element \(0\) exists and \(a+b = 0\), then \(a + b + a = a\) and so \(b+a = 0\). Therefore, \(a\) and \(b\) commute.
-
If \(a + b\) is positive, then
-
- \begin{align} (a+b) + (a+b) & {\gt} a + b \\ (b + a) + b & {\gt} b \\ b + a & {\gt} 0 \end{align}
+
We now look at the case where \(a\) is negative and \(b\) is positive. If the element \(1\) exists and \(a*b = 1\), then \(a * b * a = a\) and so \(b*a = 1\). Therefore, \(a\) and \(b\) commute.
+
If \(a * b\) is positive, then
+
+ \begin{align} (a*b) * (a*b) & {\gt} a * b \\ (b * a) * b & {\gt} b \\ b * a & {\gt} 0 \end{align}
We already showed that positive elements commute and so
-
- \[ (b+a) + b = b + (b + a) \]
+
+ \[ (b*a) * b = b * (b * a) \]
-
Now we look at the case where \(a+b {\lt} b+a\). Then we have that
-
- \begin{align} 2(a + b) & = a + ((b+a) + b) \\ & = a + (b + (b + a)) \\ & = (a + b) + (b + a) \\ & {\gt} (a + b) + (a + b) \\ & = 2(a + b) \end{align}
+
Now we look at the case where \(a*b {\lt} b*a\). Then we have that
+
+ \begin{align} (a * b)^2 & = a * ((b*a) * b) \\ & = a * (b * (b * a)) \\ & = (a * b) * (b * a) \\ & {\gt} (a * b) * (a * b) \\ & = (a * b)^2 \end{align}
-
Which is a contradiction. We get a similar contradiction in the case that \(b+a {\lt} a+b\). Therefore, \(a+b = b+a\).
-
The case where \(a+b\) is negative follows similarly. The case where \(b\) is negative and \(a\) is positive is symmetric.
+
Which is a contradiction. We get a similar contradiction in the case that \(b*a {\lt} a*b\). Therefore, \(a*b = b*a\).
+
The case where \(a*b\) is negative follows similarly. The case where \(b\) is negative and \(a\) is positive is symmetric.