$k$-Equivalence Relations and Associated Algorithms

Abstract

Lines and circles pose significant scalability challenges in synthetic geometry. A line with $n$ points implies $\left(\genfrac{}{}{0ex}{}{n}{3}\right)$ collinearity atoms, or alternatively, when lines are represented as functions, equality among $\left(\genfrac{}{}{0ex}{}{n}{2}\right)$ different lines. Similarly, a circle with $n$ points implies $\left(\genfrac{}{}{0ex}{}{n}{4}\right)$ cocyclicity atoms or equality among $\left(\genfrac{}{}{0ex}{}{n}{3}\right)$ circumcircles. We introduce a new mathematical concept of $k$-equivalence relations, which generalizes equality ($k=1$) and includes both lines ($k=2$) and circles ($k=3$), and present an efficient proof-producing procedure to compute the closure of a $k$-equivalence relation.