associativity of modular arithmetic

Johan G. F. Belinfante
2005 July 21

SetDirectory["i:"]; << goedel71.21a; << tools.m

summary

The functional formulations of Quaife's Theorems (Q10) and (Q15) may be viewed as statements about homomorphisms from the natural number system to modular number systems.  In this notebook, this is used to derive formal statements about the associativity of modular arithmetic.  The case of modulo 0 is exceptional in many ways, but not with regard to the statements of the theorems in this notebook.

modular addition

Lemma.

Assoc[composite[modulo[x], NATADD], cross[Id, modulo[x]], 
      composite[cross[Id, NATADD], ASSOC]]

composite[modulo[x_], NATADD, cross[Id, composite[modulo[x_], NATADD]], 
        ASSOC] := composite[modulo[x], NATADD, cross[NATADD, Id]]

Lemma.

Assoc[composite[modulo[x], NATADD], cross[modulo[x], Id], 
      cross[NATADD, Id]]

composite[modulo[x_], NATADD, 
        cross[composite[modulo[x_], NATADD], Id]] := 
      composite[modulo[x], NATADD, cross[NATADD, Id]]

The associativity of modular addition.

SubstTest[implies, 
      and[subclass[y, cart[cart[V, V], V]], 
        equal[composite[y, cross[Id, y], ASSOC], 
          composite[y, cross[y, Id]]]], associative[y], 
      y -> composite[modulo[x], NATADD]]

associative[composite[modulo[x_], NATADD]] := True

The restriction of addition modulo x to numbers less than x is also assocative. Quite a few steps are needed to obtain a clean statement of this.

Lemma.

ImageComp[modulo[nat[x]], id[nat[x]], V] // Reverse

image[modulo[nat[x_]], nat[x_]] := nat[x]

Temporary rule.

ImageComp[composite[modulo[nat[x]], NATADD], 
        cross[modulo[nat[x]], modulo[nat[x]]], V] // Reverse

union[
        image[modulo[nat[x_]], 
          image[NATADD, 
            cart[nat[x_], 
              union[intersection[omega, complement[image[V, nat[x_]]]], 
                nat[x_]]]]], 
        intersection[omega, complement[image[V, nat[x_]]]]] := 
      union[intersection[omega, complement[image[V, nat[x]]]], 
        nat[x]]

A standard theorem about restrictions of associative operations to classes closed under the operation now yields:

SubstTest[implies, 
      and[associative[u], subclass[image[u, cart[v, v]], v]], 
      associative[
        composite[u, id[cart[v, v]]]], {u -> 
          composite[modulo[nat[x]], NATADD], 
        v -> range[modulo[nat[x]]]}]

(% /. x -> x_) /. Equal -> SetDelayed

This can be simplified:

SubstTest[implies, equal[y, range[modulo[nat[x]]]], 
      associative[composite[modulo[nat[x]], NATADD, id[cart[y, y]]]], 
      y -> nat[x]]

(% /. x -> x_) /. Equal -> SetDelayed

The equation also holds when nat[x] = 0, so that redundant literal can be removed.

SubstTest[and, implies[p1, p2], 
        or[p1, p2], {p1 -> equal[0, nat[x]], 
          p2 -> associative[
              composite[modulo[nat[x]], NATADD, id[cart[nat[x], nat[x]]]]]}] // 
      Reverse

(% /. x -> x_) /. Equal -> SetDelayed

The nat wrapper can be removed.

SubstTest[implies, equal[y, nat[x]], 
      associative[composite[modulo[y], NATADD, id[cart[y, y]]]], 
      y -> x]

(% /. x -> x_) /. Equal -> SetDelayed

The numberhood literal is also redundant:

SubstTest[implies, equal[0, y], associative[y], 
        y -> composite[modulo[x], NATADD, id[cart[x, x]]]] // 
      MapNotNot

(% /. x -> x_) /. Equal -> SetDelayed

Finally one obtains a simple statement about addition modulo  x  restricted to numbers less than  x.

SubstTest[and, implies[p1, p2], 
        or[p1, p2], {p1 -> member[x, omega], 
          p2 -> associative[composite[modulo[x], NATADD, id[cart[x, x]]]]}] // 
      Reverse

associative[composite[modulo[x_], NATADD, id[cart[x_, x_]]]] := 
      True

modular multiplication

Lemma.

Assoc[composite[modulo[x], NATMUL], cross[Id, modulo[x]], 
      composite[cross[Id, NATMUL], ASSOC]]

composite[modulo[x_], NATMUL, cross[Id, composite[modulo[x_], NATMUL]], 
        ASSOC] := composite[modulo[x], NATMUL, cross[NATMUL, Id]]

Lemma.

Assoc[composite[modulo[x], NATMUL], cross[modulo[x], Id], 
      cross[NATMUL, Id]]

composite[modulo[x_], NATMUL, 
        cross[composite[modulo[x_], NATMUL], Id]] := 
      composite[modulo[x], NATMUL, cross[NATMUL, Id]]

Theorem about the associativity of modular multiplication.

SubstTest[implies, 
      and[subclass[y, cart[cart[V, V], V]], 
        equal[composite[y, cross[Id, y], ASSOC], 
          composite[y, cross[y, Id]]]], associative[y], 
      y -> composite[modulo[x], NATMUL]]

associative[composite[modulo[x_], NATMUL]] := True

The restriction of multiplication modulo x to numbers less than x is also assocative.  The derivation is quite similar to that for addition.

ImageComp[composite[modulo[nat[x]], NATMUL], 
        cross[modulo[nat[x]], modulo[nat[x]]], V] // Reverse

union[
        image[modulo[nat[x_]], 
          image[NATMUL, 
            cart[nat[x_], 
              union[intersection[omega, complement[image[V, nat[x_]]]], 
                nat[x_]]]]], 
        intersection[omega, complement[image[V, nat[x_]]]]] := 
      union[intersection[omega, complement[image[V, nat[x]]]], 
        nat[x]]

SubstTest[implies, 
      and[associative[u], subclass[image[u, cart[v, v]], v]], 
      associative[
        composite[u, id[cart[v, v]]]], {u -> 
          composite[modulo[nat[x]], NATMUL], 
        v -> range[modulo[nat[x]]]}]

(% /. x -> x_) /. Equal -> SetDelayed

SubstTest[implies, equal[y, range[modulo[nat[x]]]], 
      associative[composite[modulo[nat[x]], NATMUL, id[cart[y, y]]]], 
      y -> nat[x]]

(% /. x -> x_) /. Equal -> SetDelayed

SubstTest[and, implies[p1, p2], 
        or[p1, p2], {p1 -> equal[0, nat[x]], 
          p2 -> associative[
              composite[modulo[nat[x]], NATMUL, id[cart[nat[x], nat[x]]]]]}] // 
      Reverse

(% /. x -> x_) /. Equal -> SetDelayed

SubstTest[implies, equal[y, nat[x]], 
      associative[composite[modulo[y], NATMUL, id[cart[y, y]]]], 
      y -> x]

(% /. x -> x_) /. Equal -> SetDelayed

Map[or[member[x, omega], #] &, 
      SubstTest[implies, equal[0, y], associative[y], 
        y -> composite[modulo[x], NATMUL, id[cart[x, x]]]]]

(% /. x -> x_) /. Equal -> SetDelayed

This is the final result.

SubstTest[and, implies[p1, p2], 
        or[p1, p2], {p1 -> member[x, omega], 
          p2 -> associative[composite[modulo[x], NATMUL, id[cart[x, x]]]]}] // 
      Reverse

associative[composite[modulo[x_], NATMUL, id[cart[x_, x_]]]] := 
      True