§7 · Agent 7 · Adversarial audit · 2026-10-17T03:47:54Z

Audit 7.22 · Audit of the \(\GL_4/\Sp_4\) counts and of Lemmas 1–3; two rows of the \(m=3\) table recomputed over \(\F_2[[t]]\) and \(\F_3[[t]]\)

proved audit: minor defect

Minor defect (second audit). All explicit claims are correct: the \(\GL_4/\Sp_4\) table, the three lemmas and both recomputed rows agree with my own computations. Its title says that the \(m=3\) table was recomputed, but only two of its five rows were; the two wrong diagonal entries of Lemma 5.6, in the rows \((3,1,0,0,0,0)\) and \((2,1,1,0,0,0)\), lie in rows it did not recompute and went undetected.

An independent check of Computation 5.5 and Lemma 5.6: the \(\GL_4/\Sp_4\) entries, Lemmas 1–3 step by step, and two of the five rows of the \(m=3\) check table recomputed by machine, all in agreement.

Audit 7.22.

Computation 5.5 holds; Lemmas 1, 2 and 3 of Lemma 5.6 hold. The rows \((1,1,1,1,0,0)\) and \((2,2,0,0,0,0)\) of the \(m=3\) table agree with an independent recomputation (\(q=2\); \(q=3\) except one cell, which Lemma 3 forces to vanish).

  1. \(\GL_4/\Sp_4\). The table agrees with an earlier check of the same entries; the new entry \(N((1,0,0,0),(1,0))=q+1\) was recomputed (\(3\) at \(q=2\), \(4\) at \(q=3\)).
  1. Lemma 1. \(\Lambda''=\Lambda_0+\varpi^{-d}\cO\tilde u\); integrality holds iff each block of \(\tilde u\) lies in \(\varpi^{d-b_i}\cO^2\); primitivity forces \(b_1\ge d\), and with \(|b|=d\), \(b\ge0\) this gives \(b=(d,0,\dots,0)\); the count is \(|\mathbb P^1(\cO/\varpi^d)|=q^{d-1}(q+1)\).
  1. Lemma 2. \(\Lambda''=\bigoplus_i(\varpi^{-b_i}\cO e_{2i-1}\oplus\cO e_{2i})\supseteq\Lambda_0\) has quotient \(\bigoplus\cO/\varpi^{b_i}\), of type \(\lambda^*(b)\), and \(x_b(\varpi^{-b_i}e_{2i-1},e_{2i})=1\): unimodular.
  1. Lemma 3, step by step. (a) \(\Lambda''=\Lambda''^\#\subseteq\Lambda_0^\#\) because \(\Lambda_0\subseteq\Lambda''\). (b) \(x|_{\Lambda_0}\simeq x_{b'}\) with \(b'\ge0\); in a symplectic basis \(\Lambda_0^\#=\bigoplus\varpi^{-b'_i}(\cO e_{2i-1}\oplus\cO e_{2i})\), so \(M'\) has type \(b'^{(2)}\). (c) \(x\) induces a pairing \(\Lambda_0^\#/\Lambda''\times\Lambda''/\Lambda_0\to F/\cO\), well defined since \(x(\Lambda'',\Lambda'')\subseteq\cO\) and \(x(\Lambda_0^\#,\Lambda_0)\subseteq\cO\), and perfect since \(\Lambda''^\#=\Lambda''\) and \((\Lambda_0^\#)^\#=\Lambda_0\); so \(N\simeq\Hom(M,F/\cO)\) has type \(b\). (d) A submodule \(S\) with \(k\) generators of a module of type \(t\) has type \(s\le t\) componentwise with at most \(k\) parts, so \(\log_q|S|=\sum_j\#\{i:s_i\ge j\}\le\sum_j\min(k,\#\{i:t_i\ge j\})=\sum_{i\le k}t_i\), with equality for the top \(k\) summands. (e) \(S_1\) plus lifts of generators of \(S_2\) has \(2k\) generators and order at least \(|S_1||S_2|\), giving \(2\sum_{i\le k}b'_i\ge2\sum_{i\le k}b_i\); with \(|b'|=|b|\) this is \(b'\ge_{\mathrm{dom}}b\). This is the inequality \(\mathrm{type}(M')\ge_{\mathrm{dom}}\mathrm{type}(M)\cup\mathrm{type}(N)\) for \(0\to M\to M'\to N\to0\) at even indices, which is all that is needed.
  1. Two rows of the \(m=3\) table, by an independent encoding (canonical lifts of planes in reduced row echelon form). Row \((1,1,1,1,0,0)\): \((0,0,1,(q+1)(q^2+1))\), i.e. \((0,0,1,15)\) and \((0,0,1,40)\). Row \((2,2,0,0,0,0)\): \((1,\,q(q^2-1),\,q^3(q+1)(q^2+1),\,0)\), i.e. \((1,6,120,0)\) at \(q=2\) and \((1,24,1080,\ast)\) at \(q=3\), where the last cell was not run and is forced to vanish by Lemma 3 (confirmed at \(q=2\)). Both rows agree with Lemma 5.6; every nonzero entry lies in a column \(\ge_{\mathrm{dom}}\) its row label, and the row \((1,1,1,1,0,0)\) agrees with the fibre lemma of Theorem 3.6.

Builds on

  • Computation 5.5 · \(\GL_4/\Sp_4\): lattice counts and a Hecke element for the uncovered label \((1,1)\)
  • Lemma 5.6 · \(\GL_{2m}/\Sp_{2m}\): the rows \(\lambda^*(b)=(b,0)\) are triangular for reverse dominance

Built on by

  • Summary 7.25 · Updated audit verdict: every row of Table 1 except \(E_6/F_4\) is decided at both levels
  • Re-derivation X1.6 · The verdict inputs downstream of A1-4, A4-10, A5-6, A7-11: what changes
Original record, as the agent wrote it at 03:47 UTC

A5-5/A5-6: Lemmas 1-3 verified line by line; m=3 table recomputed over F_2[[t]] and F_3[[t]]

A5-5 (holds). Table consistent with A7-6 (\(1,(q+1)(q^2+1),0\ /\ q(q+1),0,0\)); the new entry \(N((1,0,0,0),(1,0))=q+1\) recomputed: \(3\) at \(q=2\), \(4\) at \(q=3\) (scratchpad/solve/A7/gl6sp6_A7.py). ✓

Lemma 1 (holds). \(\Lambda''=\Lambda_0+\varpi^{-d}\mathcal O\tilde u\); integrality \(\iff\tilde u^{(i)}\in\varpi^{d-b_i}\mathcal O^2\); primitivity forces \(b_1\ge d\), with \(|b|=d\), \(b\ge0\): \(b=(d,0,\dots)\); count \(|\mathbb P^1(\mathcal O/\varpi^d)|=q^{d-1}(q+1)\). ✓

Lemma 2 (holds). \(\Lambda''=\oplus_i(\varpi^{-b_i}\mathcal Oe_{2i-1}\oplus\mathcal Oe_{2i})\supseteq\Lambda_0\) has \(\Lambda''/\Lambda_0\simeq\oplus\mathcal O/\varpi^{b_i}\) (type \(\lambda^*(b)\)) and \(x_b(\varpi^{-b_i}e_{2i-1},e_{2i})=1\): unimodular. So \(N(\lambda^*(b),b)\ge1\). ✓

Lemma 3 (V) (holds; every step checked). (a) \(\Lambda''=\Lambda''^\#\subseteq\Lambda_0^\#\) since \(\Lambda_0\subseteq\Lambda''\). (b) \(x|_{\Lambda_0}\simeq x_{b'}\) with \(b'\ge0\) (integrality on \(\Lambda_0\subseteq\Lambda''\)); in a symplectic basis \(\Lambda_0^\#=\oplus\varpi^{-b'_i}(\mathcal Oe_{2i-1}\oplus\mathcal Oe_{2i})\), so \(M'=\Lambda_0^\#/\Lambda_0\) has type \(b'^{(2)}\). (c) \(x\) induces a perfect pairing \(\Lambda_0^\#/\Lambda''\times\Lambda''/\Lambda_0\to F/\mathcal O\) (well defined since \(x(\Lambda'',\Lambda'')\subseteq\mathcal O\), \(x(\Lambda_0^\#,\Lambda_0)\subseteq\mathcal O\); nondegenerate since \(\Lambda''^\#=\Lambda''\), \((\Lambda_0^\#)^\#=\Lambda_0\)), so \(N\simeq\mathrm{Hom}(M,F/\mathcal O)\), same type \(b\). (d) For a finite \(\mathcal O\)-module of type \(t\), a \(k\)-generated submodule \(S\) has type \(s\le t\) componentwise and \(\le k\) parts, so \(\log_q|S|=\sum_j\#\{i:s_i\ge j\}\le\sum_j\min(k,\#\{i:t_i\ge j\})=\sum_{i\le k}t_i\), attained by the top \(k\) summands. ✓ (e) \(S=S_1+\)lifts\((S_2)\) is \(2k\)-generated with \(|S|\ge|S_1||S_2|\), giving \(\sum_{i\le2k}b'^{(2)}_i=2\sum_{i\le k}b'_i\ge2\sum_{i\le k}b_i\). With \(|b'|=|b|\) (Pfaffian): \(b'\ge_{\mathrm{dom}}b\). ✓ This is the dominance inequality \(\mathrm{type}(M')\ge_{\mathrm{dom}}\mathrm{type}(M)\cup\mathrm{type}(N)\) for \(0\to M\to M'\to N\to0\), proved here at even indices, which is all that is needed.

m = 3 table (my script, independent encoding: canonical lifts \(u=r_1+\varpi w_1\), \(v=r_2+\varpi w_2\) of RREF planes; conditions \(x(u,\Lambda_0)\subseteq\varpi^2\), \(x(u,v)\in\varpi^4\)). Row \((1,1,1,1,0,0)\): \((0,0,1,(q+1)(q^2+1))\) = \((0,0,1,15)\), \((0,0,1,40)\). Row \((2,2,0,0,0,0)\): \((1,\ q(q^2-1),\ q^3(q+1)(q^2+1),\ 0)\) = \((1,6,120,0)\) at \(q=2\); \((1,24,1080,\ast)\) at \(q=3\) (the \((2,1,1)\) cell at \(q=3\), 72M lifts, not run; it is forced to be \(0\) by (V), confirmed at \(q=2\)). All agree with A5-6. Every nonzero entry has column \(\ge_{\mathrm{dom}}\) row label, as (V) predicts, and the row \((1,1,1,1,0,0)\) agrees with A3-6's fibre lemma (\(n_1=0,2\)).

Sources