§7 · Agent 7 · Adversarial audit · 2026-10-17T03:21:52Z

Audit 7.12 · Check of the decomposition of \(V_{\omega_2}\ast\IC_0\): it holds ℓ-adically; Sun's version over \(\C\) is only stated

proved audit: correct

Second audit: correct. Verified the bookkeeping, the finite-type reduction and the quotations from Sun (Theorem 1.2; Remark 3.14 and Theorem 3.15, in the workspace extracts). The statement that the Betti version needs the transfer item is conservative but not wrong: identifying the Betti category C with the finite-type model is part of that item.

Re-derives the degree bookkeeping and the self-duality argument behind the decomposition of the minuscule Satake object of \(\GL_4/\Sp_4\), confirms the finite-type model and the applicability of Sun's decomposition theorem over finite fields, and notes that Sun's statement over \(\C\) has no published proof, so the Betti version rests on the workspace's transfer item, as the checked node already says.

Audit 7.12.

The decomposition \(P\simeq\IC_{(2,0)}\oplus\IC_{(1,1)}\otimes(k[2]\oplus k\oplus k[-2])\) of Proposition 3.3 holds ℓ-adically over \(\overline{\F}_q\). Sun, Thm. 1.2 applies to \(Y^{(N)}/G_N\to Z^{(N)}/G_N\); Sun's version over \(\C\) (his Thm. 3.15) is stated with the proof deferred (his Remark 3.14), so over \(\C\) the result needs the workspace's transfer item, which Proposition 3.3 already states. The trace \(1+q+q^2+q^3=(1+q)(1+q^2)\) matches Audit 7.6 and pins the multiplicity polynomial \(q+q^2+q^3\) of \(\IC_{(1,1)}\) in \(V_{\omega_2}\ast\IC_0\) in the notation of Lemma 4.4.

  1. Degree bookkeeping, re-done. \(P=m_!k_Y[D]\) is self-dual (\(\mathbb D(k_Y[D])=k_Y[D]\), \(m\) proper). Over \(\cO_{(2,0)}\), \(P=k[D]\): the fibre is a point as a set, and the cohomology of a one-point scheme is \(k\) even if it is non-reduced; so \(A=k\). At \(x\in\cO_{(1,1)}\), \(P_x=H^*(Q^3)[D]\), one-dimensional in degrees \(-D,-D+2,-D+4,-D+6\). Support condition: \(\mathcal H^i(\IC_{(2,0)})_x=0\) for \(i\ge-\dim\cO_{(1,1)}=-D+4\), and \(\mathcal H^{-D}(\IC_{(2,0)})_x\ne0\), being the stalk of the sheaf of locally constant functions on the smooth locus, of rank the number of branches. \(\IC_{(1,1)}[-j]=k[D-4-j]\) contributes in degree \(-D+4+j\). Degrees \(-D+4,-D+6\) force \(j=0,2\), each once; self-duality of \(P\) and of \(\IC_{(2,0)}\) makes \(B\) symmetric, so \(j=-2\) occurs and exhausts degree \(-D+2\); \(j=\pm4\) is excluded since degree \(-D+8\) is empty. Hence \(B=k[2]\oplus k\oplus k[-2]\) and \((\IC_{(2,0)})_x=k[D]\). The normalization \(\IC_{(1,1)}=k[\dim\cO_{(1,1)}]\) is standard.
  1. Finite-type model. Perfectness on \(\Lambda_0+t^{-1}\widetilde W\) depends on \(\omega\bmod t^2\), so \(Y\to Z\) is pulled back from \(Y^{(N)}\to Z^{(N)}\) for \(N\ge3\); \(Y^{(N)}\) is a smooth fibration over \(\Gr(2,4)\) whose fibres are translates of \(X(\mathcal O/t^N)\).
  1. Sources. Sun, Thm. 1.2: for a proper morphism with finite diagonal between \(\F_q\)-stacks of finite type with affine stabilizers and an ι-pure complex \(K_0\), \(Rf_*K\simeq\bigoplus{}^pR^if_*K[-i]\) with semisimple terms; it applies to \(Y^{(N)}/G_N\to Z^{(N)}/G_N\). Over \(\C\), Sun's Remark 3.14 says the foundations are not written and Thm. 3.15 is only stated.
  1. Outcome. The decomposition holds ℓ-adically over \(\overline{\F}_q\); over \(\C\) it needs the transfer item, already stated in Proposition 3.3. Severity: a stated hypothesis, already stated.

Builds on

  • Proposition 3.3 · Decomposition of \(V_{\omega_2}\ast\IC_0\) for \(\GL_4/\Sp_4\): \(\IC_{(1,1)}\) is a retract with multiplicity \(k[2]\oplus k\oplus k[-2]\)

Built on by

  • Summary 7.19 · First audit verdict: conclusions (i)–(v) survive with their hypotheses; the only candidate divergence is \(E_6/F_4\)
Original record, as the agent wrote it at 03:21 UTC

A3-3: the decomposition of V_omega2 * IC_0 holds; Sun's C-version is only stated, so transfer stays open

Degree bookkeeping re-done. \(P=m_!\underline k_Y[D]\), self-dual (\(\mathbb D(\underline k_Y[D])=\underline k_Y[D]\), \(m\) proper). Over \(\mathcal O_{(2,0)}\): \(P=\underline k[D]\) (fibre a point as a set; \(R\Gamma\) of a one-point scheme is \(k\) even if non-reduced), so \(A=k\). Stalk at \(x\in\mathcal O_{(1,1)}\): \(H^*(Q^3)[D]\), degrees \(-D,-D+2,-D+4,-D+6\), each rank 1. Support condition: \(\mathcal H^i(\mathrm{IC}_{(2,0)})_x=0\) for \(i\ge-\dim\mathcal O_{(1,1)}=-D+4\), and \(\mathcal H^{-D}(\mathrm{IC}_{(2,0)})_x=(j_*\underline k)_x\ne0\) — justified (it is the sheaf of locally constant functions on the smooth locus, rank = number of branches \(\ge1\)). \(\mathrm{IC}_{(1,1)}[-j]=\underline k[D-4-j]\) contributes degree \(-D+4+j\). Degrees \(-D+4,-D+6\) force \(j=0,2\in B\) with multiplicity 1; self-duality of \(P\) and of \(\mathrm{IC}_{(2,0)}\) makes \(B\) symmetric, so \(j=-2\) occurs and exhausts degree \(-D+2\); \(j=\pm4\) is excluded by the absence of degree \(-D+8\). Hence \(B=k[2]\oplus k\oplus k[-2]\), \((\mathrm{IC}_{(2,0)})_x=k[D]\). The self-duality argument for \(B\) is valid. Normalisation: \(\mathrm{IC}_{(1,1)}=\underline k[\dim\mathcal O_{(1,1)}]\), standard.

Finite-type model (holds). Perfectness on \(\Lambda_0+t^{-1}\tilde W\) depends on \(\omega\bmod t^2\), so \(Y\to Z\) is pulled back from \(Y^{(N)}\to Z^{(N)}\) (\(N\ge3\)); \(Y^{(N)}\) is a smooth fibration over \(\mathrm{Gr}(2,4)\) with fibres translates of \(X(\mathcal O/t^N)\).

Sources. sources/sun-decomposition.pdf exists; its Thm. 1.2 is exactly 'proper, finite diagonal, \(\mathbb F_q\)-stacks of finite type with affine stabilizers, \(\iota\)-pure \(K_0\Rightarrow Rf_*K\simeq\bigoplus{}^pR^if_*K[-i]\), semisimple' — applies to \(Y^{(N)}/G_N\to Z^{(N)}/G_N\). But the \(\mathbb C\)-version (Sun Thm. 3.15) is stated with the proof deferred ('we will publish the details somewhere else', Remark 3.14), so 'over \(\mathbb C\) his final section' is a statement, not a proof. A3-3 does acknowledge the transfer as open item 1. Outcome: holds \(\ell\)-adically over \(\overline{\mathbb F}_q\); over \(\mathbb C\) needs H = open item 1 (D5). Severity: needs stated hypothesis (already stated). Consistency: trace \(1+q+q^2+q^3=(1+q)(1+q^2)\) matches A7-6 and pins \(m_{(1,1),\omega_2}=q+q^2+q^3\) in A4-4's notation.

Sources