First we must define $Sp(4)$ as in Taylor so that we can use his cosets. It is with respect to $J = \begin{pmatrix} 0_2 & 1_2 \\ 1_2 & 0_2 \end{pmatrix}$. The following program inputs a prime $p$ and outputs $Sp_4(\mathbb{F}_p)$.


We make sure it has the correct number of elements.

We define the space of 4 by 4 matrices.

The representatives in $\mathcal{B}_3$ (over $\mathbb{F}_2$) are given by the following:



We will also have need of $\mathcal{B}_1$, so we define that as well.



We now want to consider the image of the injection $\sigma_{g}: \mathcal{B}_1 \rightarrow \mathcal{B}$ induced by some $g \in K_0(1)$. Since our version of $Sp(4)$ is now a list, we cannot pick an element randomly. So just put $G[j]$ for $j$ being any number between $0$ and $719$. The following program takes as input an element of $G$ in the form $G[j]$ and outputs the elements in $\mathcal{B}_3$ that lie in the image of $\sigma_{g}$.




We can also run this more delicately to get the distribution for how they partition. We first run it over all $g$ with determinant of $C$ not being 0 to see we really hit $p1$ elements in $\mathcal{B}_3$.
The program detCnotzero inputs the set $G$ and outputs all the elements of $G$ with $C$ having nonzero determinant.



There are 384 elements of $G$ that have determinant of $C$ not zero.
The next command gives what elements in $\mathcal{B}_3$ are hit by $g$ as we run over $g*b_1 = b_3 *h$ for $g$ having determinant of $C$ nonzero, $b_1 \in\mathcal{B}_1$, $b_3 \in \mathcal{B}_3$ and $h \in G$. Note it prints them all out because I wanted to make sure the program was running correctly. After this program is one that only spits something out if we have a counterexample to what we expect.
WARNING: Output truncated! full_output.txt We are good because for g= [0 0 1 0] [0 0 0 1] [1 0 0 0] [0 1 0 0] we have T= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 0 1 0] [0 1 0 1] [1 0 0 0] [0 1 0 0] we have T= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 1 0 0] [0 0 1 0] [0 1 0 1] [1 0 0 0] we have T= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 1 0 0] [1 0 1 0] [0 1 0 1] [1 0 0 0] we have T= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 0 1 0] [0 0 0 1] [1 0 1 0] [0 1 0 0] we have T= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 0 0 1] [1 0 0 0] [0 1 0 0] [1 0 1 0] we have T= [0 0 1 0] [0 1 0 0] [0 0 1 0] ... We are good because for g= [1 0 0 1] [1 0 0 0] [1 1 0 1] [0 1 1 0] we have T= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [1 0 0 0] [0 1 0 1] [0 1 1 1] [1 0 0 1] we have T= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 1 1 1] [1 0 0 1] [1 0 0 0] [1 1 0 0] we have T= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [1 1 1 0] [0 1 1 1] [0 1 0 1] [1 0 1 0] we have T= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 0 1 1] [0 0 0 1] [1 0 1 1] [1 1 0 0] we have T= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [1 1 0 0] [0 1 0 0] [0 1 1 0] [1 0 1 1] we have T= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] WARNING: Output truncated! full_output.txt We are good because for g= [0 0 1 0] [0 0 0 1] [1 0 0 0] [0 1 0 0] we have T= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 0 1 0] [0 1 0 1] [1 0 0 0] [0 1 0 0] we have T= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 1 0 0] [0 0 1 0] [0 1 0 1] [1 0 0 0] we have T= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 1 0 0] [1 0 1 0] [0 1 0 1] [1 0 0 0] we have T= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 0 1 0] [0 0 0 1] [1 0 1 0] [0 1 0 0] we have T= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 0 0 1] [1 0 0 0] [0 1 0 0] [1 0 1 0] we have T= [0 0 1 0] [0 1 0 0] [0 0 1 0] ... We are good because for g= [1 0 0 1] [1 0 0 0] [1 1 0 1] [0 1 1 0] we have T= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [1 0 0 0] [0 1 0 1] [0 1 1 1] [1 0 0 1] we have T= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 1 1 1] [1 0 0 1] [1 0 0 0] [1 1 0 0] we have T= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [1 1 1 0] [0 1 1 1] [0 1 0 1] [1 0 1 0] we have T= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 0 1 1] [0 0 0 1] [1 0 1 1] [1 1 0 0] we have T= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [1 1 0 0] [0 1 0 0] [0 1 1 0] [1 0 1 1] we have T= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] 

The next step is to deal with the case when $g$ satisfies that $C$ has determinant 0, but $F = \begin{pmatrix} a_{11} & a_{12} \\ c_{21} & c_{22} \end{pmatrix}$ has nonzero determinant.



There are 192 elements of $G$ that satisfy $det(C) = 0$ but $det(F) \neq 0$. We now check that we get $s_3 = p$ in this case.
WARNING: Output truncated! full_output.txt We are good because for g= [0 1 0 0] [0 0 1 0] [0 0 0 1] [1 0 0 0] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 1 0 0] [1 0 1 0] [0 0 0 1] [1 0 0 0] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [1 0 0 0] [0 1 0 0] [0 0 1 0] [0 1 0 1] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 1 0 0] [0 0 1 0] [0 0 0 1] [1 0 1 0] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] ... We are good because for g= [0 1 1 0] [1 1 1 1] [0 0 1 1] [1 1 0 1] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 1 1 0] [0 0 1 0] [0 0 1 1] [1 1 0 1] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [1 1 1 0] [0 0 1 1] [0 0 0 1] [1 0 0 1] we have T[0]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [1 0 1 1] [1 1 0 0] [0 1 0 0] [0 1 1 0] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] WARNING: Output truncated! full_output.txt We are good because for g= [0 1 0 0] [0 0 1 0] [0 0 0 1] [1 0 0 0] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 1 0 0] [1 0 1 0] [0 0 0 1] [1 0 0 0] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [1 0 0 0] [0 1 0 0] [0 0 1 0] [0 1 0 1] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 1 0 0] [0 0 1 0] [0 0 0 1] [1 0 1 0] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] ... We are good because for g= [0 1 1 0] [1 1 1 1] [0 0 1 1] [1 1 0 1] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [0 1 1 0] [0 0 1 0] [0 0 1 1] [1 1 0 1] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [1 1 1 0] [0 0 1 1] [0 0 0 1] [1 0 0 1] we have T[0]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] We are good because for g= [1 0 1 1] [1 1 0 0] [0 1 0 0] [0 1 1 0] we have T[0]= [0 0 0 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] we have T[1]= [0 0 1 0] [0 1 0 0] [0 0 1 0] [0 0 0 0] 




The following code checks that $s_3 = 0$ in the case that $det(C) = det(F) = 0$.

Only stuff above this line is relevant for the check.













WARNING: Output truncated! full_output.txt ... Traceback (click to the left of this block for traceback) ... IndexError: list index out of range WARNING: Output truncated! full_output.txt ... Traceback (most recent call last): File "<stdin>", line 1, in <module> File "_sage_input_51.py", line 10, in <module> exec compile(u'open("___code___.py","w").write("# * coding: utf8 *\\n" + _support_.preparse_worksheet_cell(base64.b64decode("Zm9yIGogaW4gWzAuLjI4OF06CiAgICBiMz1NKFtbMSwwLFMxW2pdLDBdLFswLDEsMCwwXSxbMCwwLDEsMF0sWzAsMCwwLDFdXSkqTShbWzIsMCwwLDBdLFswLDEsMCwwXSxbMCwwLDEsMF0sWzAsMCwwLDJdXSkKICAgIGNvc2V0X3BhcnRpdGlvbihTMltqXSxiMyk="),globals())+"\\n"); execfile(os.path.abspath("___code___.py")) File "", line 1, in <module> File "/tmp/tmpuALo0m/___code___.py", line 3, in <module> exec compile(u'for j in (ellipsis_range(_sage_const_0 ,Ellipsis,_sage_const_288 )):\n b3=M([[_sage_const_1 ,_sage_const_0 ,S1[j],_sage_const_0 ],[_sage_const_0 ,_sage_const_1 ,_sage_const_0 ,_sage_const_0 ],[_sage_const_0 ,_sage_const_0 ,_sage_const_1 ,_sage_const_0 ],[_sage_const_0 ,_sage_const_0 ,_sage_const_0 ,_sage_const_1 ]])*M([[_sage_const_2 ,_sage_const_0 ,_sage_const_0 ,_sage_const_0 ],[_sage_const_0 ,_sage_const_1 ,_sage_const_0 ,_sage_const_0 ],[_sage_const_0 ,_sage_const_0 ,_sage_const_1 ,_sage_const_0 ],[_sage_const_0 ,_sage_const_0 ,_sage_const_0 ,_sage_const_2 ]])\n coset_partition(S2[j],b3) File "", line 2, in <module> IndexError: list index out of range 

