Axioms for the theory of proveit.numbers.modular

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import a, b, q
from proveit.logic import Equals, Exists, Forall
from proveit.numbers import Add, greater_eq, Less, Min, Mod, ModAbs, Mult, Neg
from proveit.numbers import zero, Integer, NaturalPos, Real, RealPos

%begin axioms

Defining axioms for theory 'proveit.numbers.modular'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

For positive real-valued modulus $b$, $\text{mod}(a, b)$ is the non-negative remainder $r$ when $a$ is divided by $b$ in the usual way, giving $0 \le r < b$. This means that there exists a unique integer $q$ such that $a = qb + r$.

# a mod b ≥ 0
mod_greater_eq_zero = Forall(
    (a, b),
    greater_eq(Mod(a, b), zero),
    domains=[Real, RealPos])

mod_greater_eq_zero:

# a mod b < b
mod_less_modulus = Forall(
    (a, b),
    Less(Mod(a, b), b),
    domains=[Real, RealPos])

mod_less_modulus:

# a mod b is the remainder after taking out integer multiples of modulus b
mod_is_remainder = Forall(
    (a, b),
    Exists(q, Equals(a, Add(Mult(q,b),Mod(a,b))), domain=Integer),
    domains=[Real, RealPos])

mod_is_remainder:

ModAbs captures the concept of the arc-distance between points on a circle. If $b$ is the circumference of the circle and $a$ maps to a point on the circle by traversing an arc-distance of $a$ from the origin then $|a|_{\textrm{mod}~b}$ is the arc-distance of that point from the origin (the shortest distance to traverse between the two points in either direction).

mod_abs_def = Forall(
    (a, b),
    Equals(ModAbs(a, b), Min(Mod(a, b), Mod(Neg(a), b))),
    domains=[Real, RealPos])

mod_abs_def:

%end axioms

These axioms may now be imported from the theory package: proveit.numbers.modular