xref: /aosp_15_r20/external/emboss/doc/modular_congruence_multiplication_proof.tex (revision 99e0aae7469b87d12f0ad23e61142c2d74c1ef70) 
1%This proof is used in Emboss to propagate alignment restrictions through
2%multiplication: if a and b are non-constant integers, their product can still
3%have a known alignment.
4%
5%Forgive me on the details and formatting, math majors, I never completed my
6%math degree.  --bolms
7%
8%Thanks to Aaron Webster for helping me format this as an actual proof.
9\documentclass{article}
10\usepackage[utf8]{inputenc}
11\usepackage[english]{babel}
12\usepackage{amssymb,amsmath,amsthm}
13\title{Modular Congruence of the Product of Two Values with Known Modular Congruences}
14\author{Emboss Authors}
15\date{2017}
16
17\begin{document}
18\maketitle
19
20\newtheorem{theorem}{Theorem}
21
22%(Draft)
23%TODO(webstera): Try to simplify this proof.
24
25\begin{theorem}
26Given
27
28\begin{align*}
29  &{a} \equiv {r} \pmod{{m}} \\
30  &{b} \equiv {s} \pmod{{n}} \\
31  &{a}, {r}, {m}, {b}, {s}, {n} \in \mathbb{Z}
32\end{align*}
33
34then
35
36\begin{align*}
37  &{a}{b} \equiv {r}{s} \pmod{G\left(\dfrac{{m}}{G\left({m}, {r}\right)},
38\dfrac{{n}}{G\left({n}, {s}\right)}\right) \cdot G\left({m}, {r}\right) \cdot
39G\left({n}, {s}\right)}
40\end{align*}
41
42where $G$ is the greatest common divisor function.
43\end{theorem}
44
45\begin{proof}
46\begin{align}
47  \text{Let }{q} &= G\left({m}, {r}\right) \label{eq:qdef} \\
48             {p} &= G\left({n}, {s}\right) \label{eq:pdef} \\
49             {z} &= G\left(\dfrac{{m}}{{q}}, \dfrac{{n}}{{p}}\right) =
50                    G\left(\dfrac{{m}}{G\left({m}, {r}\right)},
51                    \dfrac{{n}}{G\left({n}, {s}\right)}\right) \label{eq:zdef}
52\end{align}
53
54by the definition of modular congruence:
55\begin{align}
56  &\exists {x} \in \mathbb{Z} : {a} = {m}{x} + {r} \\
57  &\exists {y} \in \mathbb{Z} : {b} = {n}{y} + {s}
58\end{align}
59
60multiplying $\dfrac{{q}}{{q}}$ and distributing $\dfrac{1}{{q}}$:
61\begin{align}
62  &{a} = {q}\left(\dfrac{{m}{x}}{q} + \dfrac{{r}}{q}\right)
63\end{align}
64
65by the definition of ${q}$ in \eqref{eq:qdef}:
66\begin{align}
67  &\dfrac{{m}{x}}{q}, \dfrac{{r}}{q} \in \mathbb{Z} \label{eq:rqinz}
68\end{align}
69
70multiplying $\dfrac{{p}}{{p}}$ and distributing $\dfrac{1}{{p}}$:
71\begin{align}
72  &{b} = {p}\left(\dfrac{{n}{y}}{{p}} + \dfrac{{s}}{{p}}\right)
73\end{align}
74
75by the definition of ${p}$ in \eqref{eq:pdef}:
76\begin{align}
77  &\dfrac{{n}{y}}{{p}}, \dfrac{{s}}{{p}} \in \mathbb{Z} \label{eq:spinz}
78\end{align}
79
80multiplying $\dfrac{{z}}{{z}}$:
81\begin{align}
82  &{a} = {q}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} + \dfrac{{r}}{{q}}\right) \label{eq:aeqq}
83\end{align}
84
85by the definition of ${z}$ in \eqref{eq:zdef}:
86\begin{align}
87  &\dfrac{{m}{x}}{{q}{z}} \in \mathbb{Z} \label{eq:mxqzinz}
88\end{align}
89
90multiplying $\dfrac{{z}}{{z}}$:
91\begin{align}
92  &{b} = {p}\left({z} \cdot \dfrac{{n}{y}}{{p}{z}} + \dfrac{{s}}{{p}}\right) \label{eq:beqp}
93\end{align}
94
95by the definition of ${z}$ in \eqref{eq:zdef}:
96\begin{align}
97  &\dfrac{{n}{y}}{{p}{z}} \in \mathbb{Z} \label{eq:nypzinz}
98\end{align}
99
100\eqref{eq:aeqq} and \eqref{eq:beqp}:
101\begin{align}
102  &{a}{b} = {q}{p}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} +
103    \dfrac{{r}}{{q}}\right)\left({z} \cdot \dfrac{{n}{y}}{{p}{z}} +
104    \dfrac{{s}}{{p}}\right) \label{eq:abeqqp}
105\end{align}
106
107partially distributing \eqref{eq:abeqqp}:
108\begin{align}
109  &{a}{b} = {q}{p}\left({z}^2 \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
110    \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{r}}{{q}} \cdot
111    \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
112    \dfrac{{s}}{{p}} + \dfrac{{r}}{{q}} \cdot \dfrac{{s}}{{p}}\right) \label{eq:abeqqpexp}
113\end{align}
114
115extracting the $\dfrac{{r}{s}}{{q}{p}}$ term from \eqref{eq:abeqqpexp} and cancelling $\dfrac{{q}{p}}{{q}{p}}$:
116\begin{align}
117  &{a}{b} = {q}{p}\left({z}^2 \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
118    \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{r}}{{q}} \cdot
119    \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
120    \dfrac{{s}}{{p}}\right) + {r}{s} \label{eq:abeqqpextr}
121\end{align}
122
123factoring ${z}$ from \eqref{eq:abeqqpextr}:
124\begin{align}
125  &{a}{b} = {q}{p}{z}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
126    \dfrac{{n}{y}}{{p}{z}} + \dfrac{{r}}{{q}} \cdot \dfrac{{n}{y}}{{p}{z}} +
127    \dfrac{{m}{x}}{{q}{z}} \cdot \dfrac{{s}}{{p}}\right) + {r}{s}
128\end{align}
129
130because ${z}, \dfrac{{r}}{q}, \dfrac{{s}}{{p}}, \dfrac{{m}{x}}{{q}{z}},
131  \dfrac{{n}{y}}{{p}{z}} \in \mathbb{Z}$, per \eqref{eq:zdef}, \eqref{eq:rqinz}, \eqref{eq:spinz}, \eqref{eq:mxqzinz}, \eqref{eq:nypzinz}:
132\begin{align}
133  &{z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot \dfrac{{n}{y}}{{p}{z}} +
134    \dfrac{{r}}{{q}} \cdot \dfrac{{n}{y}}{{p}{z}} + \dfrac{{m}{x}}{{q}{z}} \cdot
135    \dfrac{{s}}{{p}} \in \mathbb{Z}
136\end{align}
137
138by the definition of modulus:
139\begin{align}
140  &{a}{b} \equiv {r}{s} \pmod{{q}{p}{z}}
141\end{align}
142
143by the definitions of ${q}$, ${p}$, and ${z}$ in \eqref{eq:qdef}, \eqref{eq:pdef}, and \eqref{eq:zdef}:
144\begin{align}
145  &{a}{b} \equiv {r}{s} \pmod{G\left(\dfrac{{m}}{G\left({m}, {r}\right)},
146    \dfrac{{n}}{G\left({n}, {s}\right)}\right) \cdot G\left({m}, {r}\right)
147    \cdot G\left({n}, {s}\right)}
148\end{align}
149
150\end{proof}
151\end{document}
152