§7 · Agent 7 · Adversarial audit · 2026-10-17T03:21:52Z
Audit 7.3 · Audit of the orbit count, the trace dictionary and the IC expansion: they hold under D0–D3The standing inputs of the sheaf–function dictionary over F̄_q, p ≠ 2: D0 Chen–Yi's orbit geometry; D1 traces of Frobenius and the perverse t-structure; D2 decomposition of Satake objects into shifted IC sheaves; D3 Lang's theorem; D4 unitriangularity of Satake traces; D5 comparison of F̄_q with C., and D4D4 · Unitriangularity of the Satake traces tr V_λ in the basis T_λ = 1_{Kt^λK} (Zhu (5.6.2), Lemma 5.6.3; Lusztig, Kato). is elementary
proved audit: correct
An in-run check confirming that the Lang orbit count, the trace formula for Satake objects and the IC-basis expansion are correct under the stated obligations, that the characteristic-\(p\) stabilizer lemma holds for \(p\) odd, and that the Lusztig–Kato input D4D4 · Unitriangularity of the Satake traces tr V_λ in the basis T_λ = 1_{Kt^λK} (Zhu (5.6.2), Lemma 5.6.3; Lusztig, Kato). is elementary.
Audit 7.3.
- Lemma 4.2 holds under D0D0 · Orbit geometry over F̄_q, p ≠ 2 (Chen–Yi, Prop. 17, Thm 18): orbits indexed by Λ_S^+, closures, the support bound and the stabilizers. and D3D3 · Lang's theorem for the arc group L⁺G and its stabilizers over F_q.: \(K\backslash\cO_\mu(\F_q)\simeq H^1(\F_q,\Stab)=H^1(\F_q,\pi_0Z_{G^\theta}(\mu))\). The characteristic-\(p\) form of "the fixed points of an involution of a connected unipotent group are connected" holds for \(p\) odd, so the stabilizer lemma of D0D0 · Orbit geometry over F̄_q, p ≠ 2 (Chen–Yi, Prop. 17, Thm 18): orbits indexed by Λ_S^+, closures, the support bound and the stabilizers. transfers.
- Lemma 4.3 holds under D1D1 · Traces and t-structure: proper base change and the Grothendieck–Lefschetz trace formula on convolution fibres, with a Frobenius-compatible perverse t-structure whose simple objects are the IC sheaves., with the normalisations of the classical page; D4D4 · Unitriangularity of the Satake traces tr V_λ in the basis T_λ = 1_{Kt^λK} (Zhu (5.6.2), Lemma 5.6.3; Lusztig, Kato). is not needed as a deep input.
- Lemma 4.4 (part 1) holds when \(Z_{G^\theta}(S)\) is connected; with \(Z_{G^\theta}(S)\) disconnected the basis must be refined to the \(\tr\IC_{\chi,\nu}\), as Theorem 4.11 does.
- Lemma 4.4 (parts 3–4) holds under D1D1 · Traces and t-structure: proper base change and the Grothendieck–Lefschetz trace formula on convolution fibres, with a Frobenius-compatible perverse t-structure whose simple objects are the IC sheaves. and D2D2 · Decomposition: each Satake object V_λ ∗ IC_0 is pure and splits into shifted IC sheaves with finite-dimensional multiplicity spaces (Sun, Thm 1.2; Chen–Yi, Prop. 70)..
- Orbits. Lang's theorem applies to the pro-unipotent part and to the identity component of the stabilizer. For the fixed points, filter the connected unipotent group by \(\theta\)-stable normal subgroups with vector-group quotients; since \(H^1(\Z/2,V)=0\) when \(2\) is invertible, the fixed points are connected at each step.
- Traces. The stalk formula and the Grothendieck–Lefschetz formula on the finite-type fibre \(m^{-1}(x)\subseteq\Gr_{\le\lambda}\) give \(\tr(V_\lambda\ast\IC_0)=\tr(V_\lambda)\ast_K\varphi_0\), with the classical page's convention \((f\ast\varphi)(x)=\sum_{gK}f(g)\varphi(g^{-1}x)\) and \(\operatorname{vol}K=1\). The unitriangularity \(\tr V_\lambda=\pm\one_{Kt^\lambda K}+(\text{lower})\) follows from \(V_\lambda|_{\Gr_\lambda}=\underline k[\langle2\rho,\lambda\rangle]\) and finite lower sets; the explicit Lusztig–Kato Satake transform is cited but unused. Cosmetic.
- Basis. The proof uses the support in \(\overline{\cO_\nu}\) (D0D0 · Orbit geometry over F̄_q, p ≠ 2 (Chen–Yi, Prop. 17, Thm 18): orbits indexed by Λ_S^+, closures, the support bound and the stabilizers.), one \(K\)-orbit per label (Lemma 4.2), and the nonzero value \((-1)^{\delta(\nu)}\) on \(\cO_\nu(\F_q)\) of the canonical Weil structure.
- Multiplicity spaces. \(\operatorname{Aut}(\bigoplus_\nu\IC_\nu\otimes E_\nu)=\prod_\nu\GL(E_\nu)\) because \(\End(\IC_\nu)=k\) and \(\Hom(\IC_\nu,\IC_{\nu'})=0\); \(m^{(n)}_{\nu\lambda}=\sum_i(-1)^i\tr A_{\nu,i}^n\). The Vandermonde step is valid because eigenvalues for distinct \(i\) have distinct absolute values (BBD 5.4.1), so there is no cancellation across degrees. The alternating-sum convention agrees with \(\tr(M[1])=-\tr M\).
Builds on
- Setup 4.1 · Set-up of the sheaf–function dictionary over \(\F_q(\!(t)\!)\): Weil objects, trace functions, obligations D0–D5The standing inputs of the sheaf–function dictionary over F̄_q, p ≠ 2: D0 Chen–Yi's orbit geometry; D1 traces of Frobenius and the perverse t-structure; D2 decomposition of Satake objects into shifted IC sheaves; D3 Lang's theorem; D4 unitriangularity of Satake traces; D5 comparison of F̄_q with C.
- Lemma 4.2 · \(K\)-orbits on \(X(\F_q(\!(t)\!))\) via Lang's theorem: \(\Lambda_S^+\) exactly when \(Z_{G^\theta}(S)\) is connected
- Lemma 4.3 · The trace of \(V_\lambda\ast\IC_0\) is \(\tr(V_\lambda)\ast\varphi_0\), and the traces of the \(V_\lambda\) form a basis of \(\cH_K\)
- Lemma 4.4 · Expansion of \(\tr(V_\lambda\ast\IC_0)\) in the IC basis: the coefficients are traces of Frobenius on multiplicity spaces
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
A4-2 to A4-4: Lang, trace dictionary and IC-basis expansion hold under D0-D3; D4 is elementary
A4-2 (holds under D0, D3). \(K\backslash\mathcal O_\mu(\mathbb F_q)\simeq H^1(\mathbb F_q,\mathrm{Stab})=H^1(\mathbb F_q,\pi_0Z_{G^\theta}(\mu))\): correct (Lang on the pro-unipotent and identity components). The char-\(p\) version of 'fixed points of an involution on a connected unipotent group are connected' holds for \(p\) odd (filtration by vector groups, \(H^1(\mathbb Z/2,V)=0\)), so D0's stabilizer lemma transfers.
A4-3 (holds under D1). Stalk formula + Grothendieck–Lefschetz on the finite-type fibre \(m^{-1}(x)\subseteq\mathrm{Gr}_{\le\lambda}\) gives \(\mathrm{tr}(V_\lambda\ast\mathrm{IC}_0)=\mathrm{tr}(V_\lambda)\ast_K\varphi_0\) with the pages' convention \((f\ast\varphi)(x)=\sum_{gK}f(g)\varphi(g^{-1}x)\), \(\mathrm{vol}K=1\): normalisations match classical.html. D4 is not needed as a deep input: \(\mathrm{tr}V_\lambda=\pm\mathbf 1_{Kt^\lambda K}+\)lower follows from \(V_\lambda|_{\mathrm{Gr}_\lambda}=\underline k[\langle2\rho,\lambda\rangle]\) and finite lower sets; Lusztig–Kato's explicit Satake transform is cited but unused. Cosmetic.
A4-4.1 unitriangularity (holds under \(Z_{G^\theta}(S)\) connected). Uses support in \(\overline{\mathcal O_\nu}\) (D0), one \(K\)-orbit per label (A4-2), trace \((-1)^{\delta(\nu)}\ne0\) on \(\mathcal O_\nu(\mathbb F_q)\) with the canonical Weil structure. Correct; with disconnected \(Z\) the basis must be refined to \(\mathrm{tr}\,\mathrm{IC}_{\chi,\nu}\) (as A4-11 does).
A4-4.3/4.4 (holds under D1, D2). \(\mathrm{Aut}(\bigoplus_\nu\mathrm{IC}_\nu\otimes E_\nu)=\prod\mathrm{GL}(E_\nu)\) by \(\mathrm{End}(\mathrm{IC}_\nu)=k\), \(\mathrm{Hom}(\mathrm{IC}_\nu,\mathrm{IC}_{\nu'})=0\); \(m^{(n)}_{\nu\lambda}=\sum_i(-1)^i\mathrm{tr}A_{\nu,i}^n\); the Vandermonde step is valid because eigenvalues of \(A_{\nu,i}\) for distinct \(i\) have distinct absolute values (BBD 5.4.1), so no cross-degree cancellation. The alternating-sum sign convention is consistent with \(\mathrm{tr}(M[1])=-\mathrm{tr}M\).
Sources
- A4.json Setup 4.1..A4-4
- classical.html §1
- sources/bbd-perverse.pdf 5.4.1