§7 · Agent 7 · Audit: criterion and bridge · 2026-10-18T19:27:24Z

Audit 7.9 · Audit of A5-7: (IG) over $\mathbb F_q((t))$ $\Rightarrow\mathcal M_I=\mathrm{Simple}(\mathcal P_I)$ under (L), (Hk), (L$_q$), (W), (P), (Lin), (Tr)

proved

Version 2 of Claim II is a correct abstraction of version 1: (W) and (Lin) isolate exactly what the trace argument needs; it needs the equivariant splitting of Counterexample 7.3 and, for its 'all $\mathbb F_{q^r}$' clause, linear independence over every $\mathbb F_{q^r}$.

Audit 7.9.

Holds with a minor repair. Over $\overline{\mathbb F}q$ (sheaves) and $\mathbb F_q((t))$ (functions), under (L) repaired as in Audit 7.4, (Hk), (L$_q$), (W), (P), (Lin), (Tr): (IG) implies $\mathcal M_I=\mathrm{Simple}(\mathcal P_I)$ and $\mathcal C_I^{\mathrm{Iwa}}=\mathcal C_I$. Repairs: (1) step 3 and the final appeal "(P) gives (DT)(DT) · Decomposition: every generator IC_w ∗_I IC_0 is, equivariantly, a finite direct sum of shifted simple objects of C_I. Holds over F̄_q from a finite-type proper model of the convolution (purity and the stack decomposition theorem)." must use the stack decomposition theorem (Sun, Thm 3.12/1.2), Counterexample 7.3; (2) the clause "(IG) over all $\mathbb F{q^r}((t))$ puts every simple object in $\mathcal M_I$" needs (Lin) over each $\mathbb F_{q^r}$ for the $\mathrm{Fr}^r$-stable simple objects; with connected stabilizers this follows from unitriangularity, and with disconnected stabilizers from the twisted-character basis of A3-7 (Audit 7.8); A5-7's "sufficient conditions" paragraph covers only the connected case.

  1. Step 1 (coefficients). Integral piece-indicator basis and $\mathbb Z$-valued $T_w\ast\varphi_0$ (Audit 7.6 step 6): field independence of (IG) in characteristic $0$. Holds.
  2. Step 2 (IC basis of $\mathcal H_I$). As A3-3(b) (Audit 7.6 step 6); with (Tr) the span of the $\mathrm{tr}(\mathrm{IC}w\ast\mathrm{IC}_0)$ is $\mathcal H_I\ast\varphi_0\otimes\overline{\mathbb Q}\ell$. Holds.
  3. Step 3 (trace of a generator). The trace identity $\mathrm{tr}(\mathrm{IC}w\ast\mathrm{IC}_0)=\sum_Sm{S,w}\,\mathrm{tr}(S_0)$ is correct (perverse truncation triangles, geometric semisimplicity of the pure $P_i$, block-permutation vanishing for $\mathrm{Fr}$-orbits of length $>1$). "$m_{S,w}\neq0\Rightarrow S\in\mathcal M_I$" needs the splitting in $\mathcal C_I$: repair (1). Holds with repair (1).
  4. Step 4 (conclusion). (IG) gives $C_I\otimes\overline{\mathbb Q}\ell\subseteq\mathrm{span}\{\mathrm{tr}\,S_0:\ S\in\mathcal M_I,\ \mathrm{Fr}\text{-stable}\}$; a $\mathrm{Fr}$-stable simple $S'$ has $\mathrm{tr}\,S'_0\in C_I\otimes\overline{\mathbb Q}\ell$ (pulled back from a finite level, supported on some $Y_N$), so (Lin) forces $S'\in\mathcal M_I$. Under (W) all simple objects are $\mathrm{Fr}$-stable; (P) + Sun gives (DT)(DT) · Decomposition: every generator IC_w ∗_I IC_0 is, equivariantly, a finite direct sum of shifted simple objects of C_I. Holds over F̄_q from a finite-type proper model of the convolution (purity and the stack decomposition theorem). and A5-4(c) concludes. The extension to all $r$ is the argument of A3-7 step 5 and needs repair (2). Holds with repairs.
  5. Step 5 (cancellation). Correct: only containment of spans is used; cancellation in $m_{S,w}$ can only shrink the span, and (IG) says the span is everything. The exposed direction is the converse, treated in Audit 7.10. Holds.
  6. Comparison with version 1. (W) + (Lin) $\Leftarrow$ (L2) of A3-1 (rational orbits, connected stabilizers; Audit 7.6, Audit 7.7 step 1); (P) + Sun $\Leftrightarrow$ (D3); (Tr) $\Leftarrow$ (D1), (D2) and A3-3. So the two versions prove the same theorem; version 1 contains the proofs of the hypotheses that version 2 names. Fields: conclusion over $\overline{\mathbb F}_q$ only; the Betti statement needs a separate comparison of summand statements, not supplied (same gap as Audit 7.7 statement).

Builds on

  • Proposition 5.7 · (II$_I$) (IG) over $\mathbb F_q((t))$ puts every simple object in $\mathcal M_I$

Built on by

  • Summary 7.11 · Verdict of the audit: (I$_I$) over $\overline{\mathbb F}_q$ and $\mathbb C$, (II$_I$) over $\overline{\mathbb F}_q$ only, converses as stated
Original record, as the agent wrote it at 19:27 UTC

Audit of A5-7: (IG) over $\mathbb F_q((t))$ $\Rightarrow\mathcal M_I=\mathrm{Simple}(\mathcal P_I)$ under (L), (Hk), (L$_q$), (W), (P), (Lin), (Tr)

  1. Step 1 (coefficients). Integral piece-indicator basis and $\mathbb Z$-valued $T_w\ast\varphi_0$ (Audit 7.6 step 6): field independence of (IG) in characteristic $0$. Holds.
  2. Step 2 (IC basis of $\mathcal H_I$). As A3-3(b) (Audit 7.6 step 6); with (Tr) the span of the $\mathrm{tr}(\mathrm{IC}w\ast\mathrm{IC}_0)$ is $\mathcal H_I\ast\varphi_0\otimes\overline{\mathbb Q}\ell$. Holds.
  3. Step 3 (trace of a generator). The trace identity $\mathrm{tr}(\mathrm{IC}w\ast\mathrm{IC}_0)=\sum_Sm{S,w}\,\mathrm{tr}(S_0)$ is correct (perverse truncation triangles, geometric semisimplicity of the pure $P_i$, block-permutation vanishing for $\mathrm{Fr}$-orbits of length $>1$). "$m_{S,w}\neq0\Rightarrow S\in\mathcal M_I$" needs the splitting in $\mathcal C_I$: repair (1). Holds with repair (1).
  4. Step 4 (conclusion). (IG) gives $C_I\otimes\overline{\mathbb Q}\ell\subseteq\mathrm{span}\{\mathrm{tr}\,S_0:\ S\in\mathcal M_I,\ \mathrm{Fr}\text{-stable}\}$; a $\mathrm{Fr}$-stable simple $S'$ has $\mathrm{tr}\,S'_0\in C_I\otimes\overline{\mathbb Q}\ell$ (pulled back from a finite level, supported on some $Y_N$), so (Lin) forces $S'\in\mathcal M_I$. Under (W) all simple objects are $\mathrm{Fr}$-stable; (P) + Sun gives (DT) and A5-4(c) concludes. The extension to all $r$ is the argument of A3-7 step 5 and needs repair (2). Holds with repairs.
  5. Step 5 (cancellation). Correct: only containment of spans is used; cancellation in $m_{S,w}$ can only shrink the span, and (IG) says the span is everything. The exposed direction is the converse, treated in Audit 7.10. Holds.
  6. Comparison with version 1. (W) + (Lin) $\Leftarrow$ (L2) of A3-1 (rational orbits, connected stabilizers; Audit 7.6, Audit 7.7 step 1); (P) + Sun $\Leftrightarrow$ (D3); (Tr) $\Leftarrow$ (D1), (D2) and A3-3. So the two versions prove the same theorem; version 1 contains the proofs of the hypotheses that version 2 names. Fields: conclusion over $\overline{\mathbb F}_q$ only; the Betti statement needs a separate comparison of summand statements, not supplied (same gap as Audit 7.7 statement).

Sources