More proving lemma 2.

This commit is contained in:
Aaron Huber 2020-04-15 18:49:49 -04:00
parent 67b0ecdabb
commit 7f44d527bc
2 changed files with 46 additions and 104 deletions

View file

@ -7,6 +7,7 @@
%
\newcommand{\vect}{v}
\newcommand{\wElem}{w}
\newcommand{\dw}{\tilde{\wElem}}
\newcommand{\wSet}{W}
\newcommand{\sine}{s}
\newcommand{\hfunc}{h}

149
sop.tex
View file

@ -74,8 +74,8 @@ We next describe the nonzero terms of \cref{eq:sig-j-last}.
\subsection{f, f'}
\begin{Definition}
Define and then fix a total ordering of the $\dist$ distinct world elements to follow the total order of the natural numbers in $[\dist]$, such that $\forall i, j \in [\dist], i < j \implies \widetilde{\wElem_i} < \widetilde{\wElem_j}, i.e. \wElem_1 \prec\ldots\prec\wElem_\prodsize$.
%Given a fixed order $\wSet_{\order}: \left(\wSet, \wSet\right)\mapsto \mathbb{B}$ of possible worlds, define the lexographical order of distinct worlds $\wSet_\dist$ to be the ordering which complies to the identity mapping of elements in $[\prodsize]$ to elements in $[\dist]$ up to $\dist$, such that . In other worlds, $\forall \wElem, \wElem' \in \wSet_\dist, \widetilde{\wElem} < \wElem' \leftrightarrow \wSet_{\order}\left(\wElem, \wElem'\right) = T$.
Define and then fix a total ordering of the $\dist$ distinct world elements to follow the total order of the natural numbers in $[\dist]$, such that $\forall i, j \in [\dist], i < j \implies \dw_i < \dw_j, i.e. \wElem_1 \prec\ldots\prec\wElem_\prodsize$.
%Given a fixed order $\wSet_{\order}: \left(\wSet, \wSet\right)\mapsto \mathbb{B}$ of possible worlds, define the lexographical order of distinct worlds $\wSet_\dist$ to be the ordering which complies to the identity mapping of elements in $[\prodsize]$ to elements in $[\dist]$ up to $\dist$, such that . In other worlds, $\forall \wElem, \wElem' \in \wSet_\dist, \dw < \wElem' \leftrightarrow \wSet_{\order}\left(\wElem, \wElem'\right) = T$.
\end{Definition}
To help describe all possible world value matchings we introduce functions $f$ and $f'$.
\begin{Definition}
@ -97,43 +97,16 @@ We rewrite equation \eqref{eq:sig-j-last} in terms of $\dist$ distinct worlds, w
%\ex{\prod_{i = 1}^\prodsize \sine(\dMap{\wElem_{f(i)}})\ind{h(\dMap{\wElem_{f(i)}}) = j}}\cdot \ex{\prod_{i = 1}^\prodsize\conj{\sine(\dMap{\wElem'_{f'(i)}})}\ind{h(\dMap{w'_{f'(i)}}) = j}} \right)
\label{eq:sig-j-distinct}
\end{equation}
Observe that the cartesian product of world values assigned to $\wElem_1,\ldots,\wElem_\prodsize$ throughout the summation can be rearranged into groups of variables with distinct values, for each distinct element $\dist$ in the set $[\prodsize]$. For each $\dist \in [\prodsize]$, all possible combinations of $\dist$ world values can be equivalently modeled by taking the set of surjective functions $f:[\prodsize]\mapsto [\dist]$ and computing all world value combinations based on the total ordering of $\widetilde{\wElem_{f(1)}}\prec\cdots\prec\widetilde{\wElem_{f(m)}}$. For any $\dist$, all surjective mappings $f$ constitute all unique mappings with their symmetrical counterparts. Combining that with the total order over $\widetilde{\wElem_{f(1)}},\ldots,\widetilde{\wElem_{f(\dist)}}$ yields exactly the world value combinations containing $\dist$ distinct values which appear in the cartesian product of the sum, without double counting. What this all boils down to is a rearrangement of addends in the sum.
%The fact that \cref{eq:sig-j-last} $\equiv$ \cref{eq:sig-j-distinct} follows since \cref{eq:sig-j-distinct} is simply a rearrangement of the addends in the sum.
%The reason \cref{eq:sig-j-last} $\equiv$ \cref{eq:sig-j-distinct} is because the only surviving terms in $\term_1 - \term_2$ are bijective mappings of $\dist < \prodsize$ distinct pairs between $\wElem_1\ldots\wElem_\prodsize$ and $\wElem_1'\ldots\wElem_\prodsize'$. Another way of saying this is that the only surviving terms of $\term_1 - \term_2$ are those for which we have $\dist$ distinct world values such that the same cardianlity of variables in $\wElem_1\ldots\wElem_\prodsize$ that are mapped to distinct world $\wElem _i$ $\left(\forall i \in [\dist]\right)$ is the same as the cardinality of variables mapped from $\wElem_1'\ldots\wElem_\prodsize'$.\newline
%Note that for a given $\dist$, we may have several ways to map $\prodsize$ worlds to $\dist$ distinct values. We need to define what if means for $f$ and $f'$ to be matching.
Observe that the cartesian product of world values assigned to $\wElem_1,\ldots,\wElem_\prodsize$ throughout the summation can be rearranged into groups of variables with distinct values, for each distinct element $\dist$ in the set $[\prodsize]$. For each $\dist \in [\prodsize]$, all possible combinations of $\dist$ world values can be equivalently modeled by taking the set of surjective functions $f:[\prodsize]\mapsto [\dist]$ and computing all world value combinations based on the total ordering of $\dw_{f(1)}\prec\cdots\prec\dw_{f(m)}$. For any $\dist$, all surjective mappings $f$ constitute all unique mappings with their symmetrical counterparts. Combining that with the total order over $\dw_{f(1)},\ldots,\dw_{f(\dist)}$ yields exactly the world value combinations containing $\dist$ distinct values which appear in the cartesian product of the sum, without double counting. What this all boils down to is a rearrangement of addends in the sum.
\begin{Definition}
Functions $f:[\prodsize]\mapsto [\dist], f':[\prodsize]\mapsto [\dist']$ are said to be matching, denoted $\match{f}{f'}$, if and only if
\begin{enumerate}
\item $\dist = \dist'$
\item $\{|f^{-1}(i)| ~|~ \forall i \in [\dist]\} = \{|f'^{-1}(i')| ~|~ \forall i' \in [\dist] \}$, i.e., the set of preimage cardinalities for $f$ equals the set of preimage cardinalities for $f'$.
% \item $\forall i \in [\dist], |f^{-1}(i)| = |f'^{-1}(i)|$, or a symmetrical mapping exists, where $\forall i \in [\dist], \exists i' \in [\dist]$ such that $i'$ is unique, $|f^{-1}(i)| = |f^{-1}(i')|$.
\item $\forall i \in [\dist], |f^{-1}(i)| = |f'^{-1}(i)|$, i.e., the cardinality of variables mapped to $\dw_i$ equals the cardinality of variables mapped to $\dw_i'$, for all $i \in [\dist]$.
\end{enumerate}
\end{Definition}
%\begin{Definition}
%For every $i, j \in [\dist]~|~ i < j$, the numerical value of the concatenation of the numerically ordered elements of $f^{-1}(i)$ < the numerical value of the concatenation of the numerically ordered elements of $f^{-1}(j)$, where $<$ is the order of the natural numbers.
%\end{Definition}
%
%We illustrate with an example. Consider a join of $k = 3$ tuples, where $\dist = 2$, and we have that $f^{-1}(1) = 1$ and $f^{-1}(2) = 2$. Imposing the above ordering yields the following set of unique functions:
%\begin{align*}
%f_1 = \begin{cases}
% 1 \mapsto 1 &\implies\wElem_1 \mapsto \dMap{\wElem_1}\\
% 2, 3 \mapsto 2 &\implies\wElem_2, \wElem_3 \mapsto \dMap{\wElem_2}
% \end{cases}\\
%f_2 = \begin{cases}
% 2 \mapsto 1 &\implies\wElem_2 \mapsto \dMap{\wElem_1}\\
% 1, 3 \mapsto 2 &\implies\wElem_1, \wElem_3 \mapsto \dMap{\wElem_2}
% \end{cases}\\
%f_3 = \begin{cases}
% 3 \mapsto1 &\implies\wElem_3 \mapsto \dMap{\wElem_1}\\
% 1, 2 \mapsto 2 &\implies\wElem_1, \wElem_2 \mapsto \dMap{\wElem_2}
% \end{cases}
%\end{align*}
%The above mappings satisfy the ordering constraint so that for $f_1$, $1 < 23$, for $f_2$, $2 < 13$, and for $f_3$, $3 < 12$.
%Note that above orderings share no symmetry, while the symmetrical versions of the above, which are the orderings for the case when $f^{-1}(1) = 2$ and $f^{-1}(2) = 1$, break our above ordering requirements, and are therefore disallowed, thus avoiding double counting. Another way of saying this is that the preimage sizes follow the natural order of their respective counterparts in the image. For the case when the two are equal, we need a more defined order, and can distinguish using the same idea as first described.
\begin{Lemma}\label{lem:sig-j-survive}
When $f, f'$are matching, where $\forall j \in[\dist], \dMap{\wElem_j} = \dMap{\wElem'_j}$, \cref{eq:sig-j-distinct} is exactly
@ -179,89 +152,57 @@ Consider the "generic term"--
Let's rewrite the term based on its exact definition:
\begin{align*}
= &\ex{\prod_{i = 1}^{\prodsize}\sine(\widetilde{\wElem_{f(i)}})\cdot\conj{\sine(\widetilde{\wElem'_{f'(i)}})}}\\
= &\ex{\left(\prod_{i = 1}^{\dist}\sine(\widetilde{\wElem_{i}})^{|f^{-1}(i)|}\right) \cdot \left(\prod_{j = 1}^{\dist'}\conj{\sine(\widetilde{\wElem'_{j}})}^{|f^{-1}(j)|}\right)}
= &\ex{\prod_{i = 1}^{\prodsize}\sine(\dw_{f(i)})\cdot\conj{\sine(\dw'_{f'(i)})}}\\
= &\ex{\left(\prod_{i = 1}^{\dist}\sine(\dw_{i})^{|f^{-1}(i)|}\right) \cdot \left(\prod_{j = 1}^{\dist'}\conj{\sine(\dw'_{j})}^{|f^{-1}(j)|}\right)}
\end{align*}
Notice that each $i \in [\prodsize]$ has its own mapping to an element in $[\dist]$. We can thus rearrange all the elements of the product such that the preimage of function $f(i)$, i.e., $f^{-1}(i)$ yields the number of terms that will be mapped to a distinct variable $\widetilde{\wElem_i}$.
Further see how the requirement that $\widetilde{\wElem_i} = \widetilde{\wElem'_i}$ gives us the precise combinations we are looking for, where each random $\sine$ output value has its own matching complex conjugate.
\newline===============Old Stuff==============
To prove that \cref{lem:sig-j-survive} is true, consider what the expectation looks like when $f, f'$ are not matching. Looking at the first condition for $f, f'$ to be matching when $\dist \neq \dist'$ note that since $\dist \neq \dist'$ we know that one set of variables has at least one more distinct world than the other set of variables. Also, to be explicit, $\wElem_1\ldots\wElem_\dist, \wElem_1'\ldots\wElem_{\dist'}'$ are distinct world values such that $\forall i \neq j \in [\dist], \wElem_i = \wElem_i' \neq \wElem_j = \wElem_j'$. To make things easier, assume that $\dist < \dist'$. The opposite case of $\dist > \dist'$ has a symmetrical proof. Fixing variables $\wElem_1\ldots\wElem_\dist, \wElem_1'\ldots\wElem_\dist$, in both $\term_1$ and $\term_2$ we have one extra distinct value, $\wElem_{\dist'}'$. This distinct term cancels out all the other values in the expectations.
Notice that each $i \in [\prodsize]$ has its own mapping to an element in $[\dist]$. We can thus rearrange all the elements of the product such that the preimage of function $f(i)$, i.e., $f^{-1}(i)$ yields the number of terms that will be mapped to a distinct variable $\dw_i$.
Further see how the requirement that $\dw_i = \dw'_i$ gives us the precise combinations we are looking for, where each random $\sine$ output value has its own matching complex conjugate.
To prove that \cref{lem:sig-j-survive} is true, consider what the expectation looks like when $f, f'$ are not matching. The first condition for $f, f'$ to be matching is violated when $\dist \neq \dist'$.
\AH{The following observation isn't necessary to complete the proof. I'll just leave it for now in case it may be valuable down the road.}
Observe that $\forall \dist \in [\prodsize], \sum_{i = 1}^{\dist}|f^{-1}(i)| = \prodsize$ and that this fact implies for $\dist, \dist' \in [\prodsize] ~|~\dist \neq \dist', \exists i \in [m] ~|~\forall j \in [m], f^{-1}(i)| \neq |f'^{-1}(j)|$, meaning that if we have that $\dist \neq \dist'$, then the second matching condition is also violated.
\AH{Moving on...}Note that $\dw_1\ldots\dw_\dist, \dw_1'\ldots\dw_{\dist'}'$ are distinct world values such that $\forall i \neq j \in [\dist], \dw_i = \dw_i' \neq \dw_j = \dw_j'$. To make things easier, assume that $\dist < \dist'$. The opposite case of $\dist > \dist'$ has a symmetrical proof. Fixing variables $\dw_1\ldots\dw_\dist, \dw_1'\ldots\dw_\dist$, we have at least one $\dw_i$ without a conjugate, and at least one extra distinct value, $\dw_{\dist'}'$, for which no $\dw_{\dist'}$ exists. This (these) distinct term(s) cancel(s) out all the other values in the expectations.
\begin{align}
\term_1 - \term_2 = &\ex{\sine(\wElem_1)\conj{\sine(\wElem_1)}\cdot\ldots\cdot\sine(\wElem_\dist)\conj{\sine(\wElem_\dist)}\cdot\conj{\sine(\wElem'_{\dist'})}} - \ex{\prod_{i = 1}^{\dist}\sine(\wElem_i)^{j_i}}\ex{\left(\prod_{i = 1}^{\dist}\sine(\wElem_i)^{j_i}\right) \cdot \conj{\sine(\wElem'_{\dist'})}}\\
= &\ex{\sine(\wElem_1)\conj{\sine(\wElem_1)}\cdot\ldots\cdot\sine(\wElem_\dist)\conj{\sine(\wElem_\dist)}}\cdot \ex{\conj{\sine(\wElem'_{\dist'})}} - \ex{\prod_{i = 1}^{\dist}\sine(\wElem_i)^{j_i}}\ex{\prod_{i = 1}^{\dist}\sine(\wElem_i)^{j_i}} \cdot \ex{\conj{\sine(\wElem'_{\dist'})}}\\
= &0.
%&\sum_{\substack{\wElem_1,\ldots,\wElem_{\dist},\\ \wElem_1',\ldots,\wElem_{\dist}'\\\in \wSet}}\prod_{i = 1}^{\prodsize}\vect_i(\wElem_i)\vect_i(\wElem_i')
% \left(\ex{\prod_{i = 1}^{k}\sine(\wElem_i)\conj{\sine(\wElem_i')}\ind{\hfunc(\wElem_i) = \buck}\ind{\hfunc(\wElem_i') = \buck}} -
% \ex{\prod_{i = 1}^{k}\sine(\wElem_i)\ind{\hfunc(\wElem_i) = \buck}}\ex{\prod_{i = 1}\conj{\sine(\wElem'_i)}\ind{\hfunc(\wElem'_i) = \buck}} \right) \\
%
%
%\term_1 = \ex{\sine(\wElem_1)^{\dupSize_1}\cdot,\ldots,\cdot\sine(\wElem_m)^{\dupSize_m}\conj{\sine(\wElem_1')}^{\dupSize_1'}\cdot, \ldots,\cdot \conj{\sine(\wElem_{m}')}^{\dupSize_m'} \cdot, \ldots, \cdot \conj{\sine(\wElem_{m'}')}^{\dupSize_{m'}'}} = 0.
&\ex{\left(\prod_{i = 1}^{\dist}\sine(\dw_{i})^{|f^{-1}(i)|}\right) \cdot \left(\prod_{j = 1}^{\dist'}\conj{\sine(\dw'_{j})}^{|f^{-1}(j)|}\right)}\nonumber\\
= &\ex{\left(\prod_{i = 1}^{\dist}\sine(\dw_{i})^{|f^{-1}(i)|}\right) \cdot \left(\prod_{j = 1}^{\dist}\conj{\sine(\dw'_{j})}^{|f^{-1}(j)|}\right)\left(\prod_{l = \dist + 1}^{\dist'}\conj{\sine(\dw_l)}^{f'^{-1}(l)}\right)}\nonumber\\
= &\ex{\left(\prod_{i = 1}^{\dist}\sine(\dw_{i})^{|f^{-1}(i)|}\right) \cdot \left(\prod_{j = 1}^{\dist}\conj{\sine(\dw'_{j})}^{|f^{-1}(j)|}\right)} \cdot \prod_{l = \dist + 1}^{\dist'} \ex{\conj{\sine(\dw_l)}^{|f^{-1}(l)|}} = 0.\label{eq:lem-fmatch-pt1}
\end{align}
By the same reasoning in the proof of \cref{lem:exp-prod-rand-roots}, we can push the expectation into the product of two independent random values. \textit{Here at most we assume 2k wise independence, but we really would like less}. Then by \cref{lem:exp-sine}, we get an factor of zero in both products, giving a result of zero.\qed
In \cref{eq:lem-fmatch-pt1} the expectation can be pushed through the last product group since we know that all the operands are distinct from any others appearing in the overall product. Then, by \cref{lem:exp-sine} we get $0$ for that rightmost term, and this cancels out the rest of the terms in the overall product.
%Notice that, with $\dist < \dist'$, this means that there will be $\sum\limits_{n \in \{ [\dist'] - [\dist] \}}\dupSize_n'$ world values on either side that do not have a match since the number of $\prodsize$ products is constant. This leaves us with $\prod\limits_{\dupSize_{n^*} \in \{\dupSize_n | \forall n \in [m], \dupSize_n \neq \dupSize_n'\}}\sine(\wElem_i)^{\dupSize_{n^*} - \dupSize_{n'}} \cdot \prod\limits_{\dist_i' \in \{\dist' - \dist\}}\conj{\sine(\wElem_{m_i'}')}^{\dupSize_{m_i'}'}$ pairings, where $\forall \wElem_i \in \{\wElem_i | i \in [m], \dupSize_i \neq \dupSize_i'\}, \forall \dist_i' \in \{\dist_i' | \dist_i' \in \{\dist' - \dist\}\}, \wElem_i \neq \wElem_{\dist_i'}$, which in expectation is 0 by \cref{lem:exp-prod-rand-roots}. The proof is symmetric for the case of $\dist > \dist'$.
%
%From $\term_2$, notice that by the fact that $\dist' > \dist$, it has to be the case that $\dist' > 1$, which by \cref{lem:exp-prod-rand-roots} equals zero, setting the whole product to zero. The proof is symmetric for the case of $\dist > \dist'$.
%\qed\newline
%%\newline Assume $\dist < \dist'$.
%%\begin{align*}
%%\term_2 = &\ex{\prod_{i = 1}^ks(w_i)\ind{h(w_i) = j}}\cdot \ex{\prod_{i = 1}^\prodsize\overline{s(w'_i)}\ind{h(w'_i) = j}}\\
%%= &\ex{\sine(\wElem_1)^{\dupSize_1}\cdot\ldots\cdot\sine(\wElem_\dist)^{\dupSize_\dist}} \cdot
%% \ex{\conj{\sine(\wElem_1')}^{\dupSize_1'}\cdot\ldots\cdot\conj{\sine(\wElem_{\dist}')}^{\dupSize_\dist'}\conj{\sine(\wElem_{\dist + 1}')}^{\dupSize_{\dist + 1}'}\cdot\ldots\cdot\conj{\sine(\wElem_{\dist'}')}^{\dupSize_{\dist'}'}}\\
%%= &\ex{\sine(\wElem_1)^{\dupSize_1}\cdot\ldots\cdot\sine(\wElem_\dist)^{\dupSize_\dist}} \cdot 0 \\
%%= & 0
%%\end{align*}
%
%%Note that the second expectation in $\term_2$ cancels out by the fact that there is at least one distinct worl $\wElem_\dist'$ that does not match any of the other world value in the product, and by \cref{lem:exp-prod-rand-roots} yields zero.
To finish the proof of \cref{lem:sig-j-survive}, we now approach the case where $\dist = \dist'$, but the set of preimage cardinalities for $f, f'$ are unequal. Effectively this condition means that we end up with the same result of unequal pairs as when $\dist \neq \dist'$.
\textit{Here at most we assume 2k wise independence, but we really would like less}.
\AH{Can we bring it down to k-wise, since we have $<$ k terms which we are pushing the expectation through?}
To complete the proof, we now approach the case where $\dist = \dist'$, but there is a $\dw_i, \dw_i'$ with an unequal number of mappings.
\begin{align}
&\{|f^{-1}(i)| ~|~ \forall i \in [\dist]\} \neq \{|f'^{-1}(i')| ~|~ \forall i' \in [\dist] \}\\
\rightarrow &\exists i, i' \in [m] s.t. |f^{-1}(i)| \neq |f'^{-1}(i)|, |f^{-1}(i')| \neq |f'^{-1}(i')|\\
%\rightarrow &|\dupSize_s - \dupSize_s'| = |\dupSize_t - \dupSize_t'|\text{ by the fact that $\dist = \dist'$}
\end{align}
The above means that we will have at least two world values that don't match, i.e. a $\wElem_i \neq \wElem_{i'}'$, both of which $i \neq i' \in [m]$. Fixing all world values except $\wElem_i$ and $\wElem_{i'}'$,
\begin{align*}
&\exists i \in [\dist], |f^{-1}(i)| \neq |f'^{-1}(i)|\\
\implies &\exists j \in [m] ~|~i \neq j, |f^{-1}(j)| \neq |f'^{-1}(j)|\\
\implies &\exists i, j \in [\dist], i \neq j ~|~ |\dw_i| \neq |\dw_j|\\
%\implies &\exists \wElem_i \in \wSet ~|~ \nexists \wElem_i' \in \wSet ~|~ \wElem_i = \wElem_i'
\end{align*}
The above means that we will have at least two world values that don't match. Put another way, after the optimal number of matching world value pairs have been assigned, there will be at least one world value whose matching conjugate product is not the conjugate of the sine of the same world value. i.e. for $i \neq j$, there will exist at least one product of $\sine(\dw_i) \conj{\sine(\dw_{j}')}$.
\begin{align}
\term_1 - \term_2 = &\ex{\left(\prod_{i''= 1}^{\dist}\sine(\wElem_{i''})\conj{\sine(\wElem_{i''}')}\right)\sine(\wElem_i)\conj{\sine(\wElem_{i'}')}} - \ex{\prod_{i'' = 1}^{\dist}\sine(\wElem_{i''})}\cdot\ex{\prod_{i'' = 1}^{\dist}\conj{\sine(\wElem_{i''}')}}\\
= &\ex{\prod_{i''= 1}^{\dist}\sine(\wElem_{i''})\conj{\sine(\wElem_{i''}')}}\ex{\sine(\wElem_i)\conj{\sine(\wElem_{i'}')}} -
\ex{\prod_{i'' = 1 s.t. i'' \neq i}^{\dist}\sine(\wElem_{i''})}\cdot \ex{\sine(\wElem_{i})}\cdot\ex{\prod_{i'' = 1 s.t. i'' \neq i'}^{\dist}\conj{\sine(\wElem_{i''}')}}\cdot \ex{\conj{\sine(\wElem_{i'}')}}\\
= &0.
\end{align}
By the same arguments as before, we have at least one distinct world value in each expectation, which by independence of random variables allows us to push the expectations into the product, and then by \cref{lem:exp-prod-rand-roots} and \cref{lem:exp-sine} produce a zero in each product, yielding a value of zero.\qed
%To be clear, if the set of preimage sizes do not match, then we have for both $f, f'$ at least two preimage mappings to their respective distinct variables whose corresponding sizes are both unequal. In the notation above, we set the unmatching cardinalities to $\dupSize_s$, etc. to reference later on. Note that since $\dist$ is the same for both $f, f'$, the disagreement in cardinalities evens out across variables. For the sake of argument, define $\dupSize_s > \dupSize_s', \dupSize_t' > \dupSize_t$.
%
%Translating this to $\term_1$ and $\term2$ we have
%\begin{align}
%\term_1 = &\ex{\left(\prod_{i \in [\dist] | i \neq s, t}\sine(\wElem_i)^{\dupSize_i}\conj{\sine(\wElem_i')}^{\dupSize_i}\right)
% \sine(\wElem_s)^{\dupSize_s}\conj{\sine(\wElem_s')^{\dupSize_s'}}\sine(\wElem_t)^{\dupSize_t}\conj{\sine(\wElem_t')}^{\dupSize_t'} }\\
%= &\ex{\left(\prod_{i \in [\dist] | i \neq s, t}\sine(\wElem_i)^{\dupSize_i}\conj{\sine(\wElem_i')}^{\dupSize_i}\right)
% \sine(\wElem_s)^{\dupSize_s'}\conj{\sine(\wElem_s')^{\dupSize_s'}} \sine(\wElem_t)^{\dupSize_t}\conj{\sine(\wElem_t')}^{\dupSize_t} \cdot
% \sine(\wElem_s)^{\dupSize_s - \dupSize_s'} \conj{\sine(\wElem_t)}^{\dupSize_t' - \dupSize_t} }\\
%=& 0.
%\end{align}
%Note, that because we have that $\wElem_s \neq \wElem_t$, the expectation is zero by \cref{lem:exp-prod-rand-roots}.
%
%For $\term_2$, notice that since we have $m \geq 2$ for preimage sizes to disagree, both expectations yield zero by \cref{lem:exp-prod-rand-roots}.
%
%For the case where $\dupSize_s < \dupSize_s', \dupSize_t' < \dupSize_t$, the argument is symmetric.\qed\newline
%Since we have at least one extra \textit{distinct} world value, whose conjugate of its sine value is paired with the sine value of another distinct world value, the expectation will equal zero.
%\newline
%The proof is immediate and follows from the fact that the random $\sine$ functions are only guaranteed to produce a product of one under one of two possible conditions:
% \begin{enumerate}
% \item $\sine(\wElem)^\prodsize = 1$,
% \item $\sine(\wElem) \conj{\sine(\wElem)} = 1$.\qed
% \end{enumerate}
Let $n = \{i ~|~ |f^{-1}(i)| \neq |f'^{-1}(i)|\}$. Further, let $\dist_* = [\dist] - n$ and $f^{*-1}(i) = min\left(f^{-1}(i), f'^{-1}(i)\right)$. Then,
\begin{align*}
\term_1 = &\ex{\left(\prod_{i \in [\dist_*]} \sine(\dw_i)^{|f^{-1}(i)|} \conj{\sine(\dw_i)}^{|f'^{-1}(i)|}\right)
\left(\prod_{j \in n}\sine(\dw_i)^{|f^{*-1}|} \conj{\sine(\dw_i)^{|f^{*-1}|}}\right)
\left(\prod_{\substack{i' \in n ~|~\\f^{-1}(i') > f'{-1}(i')}} \sine(\dw_{i'})^{|f^{-1}(i')| - |f'^{-1}(i')|} \prod_{\substack{j' \in n ~|~\\ f'^{-1}('j) > f^{-1}(j')}} \conj{\sine(\dw_{j'})}^{|f'^{-1}(j')| - |f^{-1}(j')|}\right)}\\
= &\ex{\left(\prod_{i \in [\dist_*]} \sine(\dw_i)^{|f^{-1}(i)|} \conj{\sine(\dw_i)}^{|f'^{-1}(i)|}\right)
\left(\prod_{j \in n}\sine(\dw_i)^{|f^{*-1}|} \conj{\sine(\dw_i)^{|f^{*-1}|}}\right)} \cdot
\ex{\left(\prod_{\substack{i' \in n ~|~\\f^{-1}(i') > f'{-1}(i')}} \sine(\dw_{i'})^{|f^{-1}(i')| - |f'^{-1}(i')|} \prod_{\substack{j' \in n ~|~\\ f'^{-1}('j) > f^{-1}(j')}} \conj{\sine(\dw_{j'})}^{|f'^{-1}(j')| - |f^{-1}(j')|}\right)}\\
= &\ex{\left(\prod_{i \in [\dist_*]} \sine(\dw_i)^{|f^{-1}(i)|} \conj{\sine(\dw_i)}^{|f'^{-1}(i)|}\right)
\left(\prod_{j \in n}\sine(\dw_i)^{|f^{*-1}|} \conj{\sine(\dw_i)^{|f^{*-1}|}}\right)} \cdot
\ex{\prod_{\substack{i' \in n ~|~\\f^{-1}(i') > f'{-1}(i')}} \sine(\dw_{i'})^{|f^{-1}(i')| - |f'^{-1}(i')|}} \cdot \ex{\prod_{\substack{j' \in n ~|~\\ f'^{-1}('j) > f^{-1}(j')}} \conj{\sine(\dw_{j'})}^{|f'^{-1}(j')| - |f^{-1}(j')|}}\\
= &\ex{\left(\prod_{i \in [\dist_*]} \sine(\dw_i)^{|f^{-1}(i)|} \conj{\sine(\dw_i)}^{|f'^{-1}(i)|}\right)
\left(\prod_{j \in n}\sine(\dw_i)^{|f^{*-1}|} \conj{\sine(\dw_i)^{|f^{*-1}|}}\right)} \cdot
\prod_{\substack{i' \in n ~|~\\f^{-1}(i') > f'{-1}(i')}} \ex{\sine(\dw_{i'})^{|f^{-1}(i')| - |f'^{-1}(i')|}} \cdot \prod_{\substack{j' \in n ~|~\\ f'^{-1}('j) > f^{-1}(j')}} \ex{\conj{\sine(\dw_{j'})}^{|f'^{-1}(j')| - |f^{-1}(j')|}}\\
& = 0.
\end{align*}
Note that each $\sine$ function in the first expectation has its matching complex conjugate in the product terms. However, for each of the expectations in the rightmost products, each $\sine$ function has a distinct input. Therefore, by \cref{lem:exp-sine}, each of those inner expectations computes to $0$. This computation zeroes out the whole product.
%\AH{Here is where I have attempted to use prose to discuss the restrictions on $f$ and $f'$, rather than the use of \dist-tuples. Maybe there is a better, cleaner formal way?}
%E.g., for $\prodsize = 4, \dist = 2$, mappings could be such that one $\wElem_i$ is distinct, while the other three $\wElem_i$ are mapped to the other distinct value. Additionally, we would have the case where two $\wElem_i$ map to a distinct value, while the other two $\wElem_i$ map to a seperate distinct world. The expectations of equation \eqref{eq:sig-j-last} restrict $f$ and $f'$ to belonging to the same class of $\dist$-mapping, meaning, if the mapping $f$ for $\prodsize = 4, \dist = 2$ is in the setting of one distinct world and three equal world values, then $f'$ must be from that same set of mappings, and not from another class of mappings, such as when two $w_i$ map to a distinct world, while the other two $w_i$ map to a separate distinct world.
%\AH{Here is the use of \dist-tuples to explain the same thing.}
% In the example above, $f$ mappings for $\dist_{2_1}$ may only cross product with $f'$ mappings for $\dist_{2_1}$ and not with those for $\dist_{2_2}$. Likewise for $f, f'$ mappings of $\dist_{2_2}$.
\AH{Next on the agenda v------}
We now seek to show that when $f, f'$ are matching, that $\term_1 - \term_2$ will always equal 1.
\end{proof}