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

Audit 7.10 · Audit for the spheres: the restriction-map proof (under (A)), the proof over \(\F_q(\!(t)\!)\) and the lattice proof (any \(F\), \(q\) odd) are consistent and correct

proved audit: correct

Second audit: correct. No defect. The proof of Proposition 1.3 was re-checked step by step (Witt plus reflection; spinor norm of r_{f1+f2} r_{f1+u f2} is u; unit and non-unit norm cases; Spin(O)-orbits = SO(O)-orbits via SO(W)(O); support bound) and is correct, including for F = F_q((t)) with q odd. Lemma 4.8 is conditional on D0, D3 (and q odd); its full audit belongs to its own group. The O'Meara item numbers (92:1, 92:3) could not be checked against sources in the packet.

Checks Proposition 6.3 by hand and audits the two other proofs that (SG) holds for \(\Spin_{2n}/\Spin_{2n-1}\): the lattice-theoretic one over any non-archimedean \(F\) with odd residue characteristic, and the one over \(\F_q(\!(t)\!)\). All three agree, so the sphere row holds at both levels for every \(n\ge2\), the function level unconditionally for odd \(q\).

Audit 7.10.

Proposition 6.3 holds under (A): \(\Lambda_T=\{x:\sum x_i\text{ even}\}\), \(\Lambda_S=2\Z\varepsilon_1=\varphi(\Lambda_T)\), \(\rho_L=(0,n-2,\dots,1,0)\); the terms of \(m_{\varepsilon_1+\varepsilon_2}\) with \(i=1\) give \(u^{\pm1}q^{\pm(n-j)}\), so the coefficient of \(u^{\pm1}\) is \(c_n(q)=\sum_{j=2}^n(q^{n-j}+q^{j-n})>0\), the rest is constant, and \(u+u^{-1}\in\operatorname{im}r\) generates \(\C[u+u^{-1}]\).
Proposition 1.3 holds for \(q\) odd and every non-archimedean local field \(F\). Oddness of \(q\) enters at four places (the classification of unimodular lattices, Hensel's lemma for \(1+\varpi\cO\), Witt cancellation over \(\cO\), and spinor-norm theory), not only through \(2\in\cO^\times\) in the normalization; residue characteristic 2 would need a different lattice theory.
Lemma 4.8, which holds under its standing inputs D0 (orbits, orbit closures, the support bound and connected stabilizers over \(\overline{\F}_q\)) and D3 (rationality of the orbit representatives and compact-openness of the orbits over \(\F_q\)), gives the same conclusion over \(\F_q(\!(t)\!)\).

Three routes, one conclusion: the sphere row holds at both levels for all \(n\ge2\), the sheaf level by Proposition III and the function level unconditionally for odd \(q\). The entry "\(n\ge4\) open" in Table 1 of the Summary tab is closed. Severity: none.

The restriction-map proof. Re-derived by hand from the data of the \(\Spin_{2n}/\Spin_{2n-1}\) family page; the computation is that of Proposition 6.3.

The lattice proof, step by step.

\(\SO_{2n}(F)\) is transitive on the quadric \(Q(F)=\{x:x^{\mathsf T}Jx=2\}\simeq X(F)\) by Witt's theorem, composed with a reflection to correct the determinant.
The image of \(\Spin_{2n}(F)\) in \(\SO_{2n}(F)\) is the kernel of the spinor norm, and the spinor norm of the split group \(\SO_{2n-1}(F)\) is onto \(F^\times/F^{\times2}\), since \(2n-1\ge3\) and the space contains a hyperbolic plane.
Primitive vectors of a given norm \(c\) form one orbit of the orthogonal group of the lattice: for a unit \(c\), by the classification of unimodular lattices by rank and discriminant; for a non-unit \(c\), through a unimodular binary lattice \(\langle y,z\rangle\) of discriminant \(-(1-cB(z,z))\), which is \(-1\) times a square by Hensel's lemma, hence a hyperbolic plane, followed by Witt cancellation over \(\cO\) and the elements \(\operatorname{diag}(a^{-1},a)\) of the hyperbolic plane.
Orbits of \(\SO(\cO)\) are obtained with a reflection in a unit vector of the nonzero orthogonal complement \(L'\) of that hyperbolic plane; orbits of \(\Spin(\cO)\) coincide with those of \(\SO(\cO)\), because the stabilizer of each representative contains \(\SO(V_0)(\cO)\), \(V_0=\langle e_2,\dots,e_{2n-1}\rangle\) hyperbolic, whose spinor norm is onto \(\cO^\times/\cO^{\times2}\) when the rank of \(V_0\) is at least 2.
The orbits are the pole orders \(m\ge0\), with representatives \(x_m=t^{m(\varepsilon_1+\varepsilon_2)}x_0\), and the pole-order bound gives the support condition of Corollary C.

All steps are correct (O'Meara, 92:1 and 92:3, for \(p\ne2\)).

The proof over \(\F_q(\!(t)\!)\). Lemma 4.8 holds under D0 and D3 and gives the same conclusion for \(F=\F_q(\!(t)\!)\).

The three routes are consistent, and together they decide the sphere row at both levels.

Builds on

Proposition 6.3 · \(\Spin_{2n}/\Spin_{2n-1}\): \(r\) is onto for every \(n\ge2\), so (SG) holds under (A1)–(A5)
Proposition 1.3 · Spheres \(\Spin_{2n}/\Spin_{2n-1}\): (SG) for odd residue characteristic
Lemma 4.8 · Under the two conditions of Proposition III, (SG) holds over \(\F_q(\!(t)\!)\) without Sakellaridis's hypotheses

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

Spheres: A6-3 (under (A)), A4-8 (over F_q((t))) and A1-3 (any F, q odd) are consistent and correct

A6-3 (holds under (A)). \(\Lambda_T=\{\sum x_i\text{ even}\}\), \(\Lambda_S=2\mathbb Z\varepsilon_1=\varphi(\Lambda_T)\), \(\rho_L=(0,n-2,\dots,1,0)\); the \(i=1\) terms of \(m_{\varepsilon_1+\varepsilon_2}\) give \(u^{\pm1}q^{\pm(n-j)}\), coefficient \(c_n(q)=\sum_{j=2}^n(q^{n-j}+q^{j-n})>0\); the rest is constant. \(\mathrm{im}\,r\ni u+u^{-1}\) generates \(\mathbb C[u+u^{-1}]\). Re-derived by hand. ✓

A1-3 (holds for \(q\) odd, every \(F\)). Each lattice step checked: Witt + reflection for \(\mathrm{SO}(F)\)-transitivity; \(\mathrm{im}\,\mathrm{Spin}(F)=\ker(\text{spinor norm})\) and spinor norm of split \(\mathrm{SO}_{2n-1}(F)\) onto \(F^\times/F^{\times2}\) (hyperbolic plane, \(2n-1\ge3\)); primitive vectors of norm \(c\): unit \(c\) via classification of unimodular lattices by rank and discriminant, non-unit \(c\) via a unimodular binary \(\langle y,z\rangle\) of discriminant \(-(1-cB(z,z))=-\square\) (Hensel), hence \(\simeq H\), Witt cancellation over \(\mathcal O\), and \(\mathrm{diag}(a^{-1},a)\) in \(H\); \(\mathrm{SO}(\mathcal O)\) via a reflection in \(L'\ne0\); \(\mathrm{Spin}(\mathcal O)=\mathrm{SO}(\mathcal O)\) orbits via spinor norm of \(\mathrm{SO}(W)(\mathcal O)\) onto \(\mathcal O^\times/\mathcal O^{\times2}\) (\(\mathrm{rk}\,W\ge2\)); \(x_m=t^{m(\varepsilon_1+\varepsilon_2)}x_0\); pole order bound for the support. All correct (O'Meara 92:1, 92:3 for \(p\ne2\)). \(q\) odd enters at four places (unimodular classification, Hensel for \(1+\varpi\mathcal O\), Witt cancellation over \(\mathcal O\), spinor-norm theory), not only through \(2\in\mathcal O^\times\) in the normalisation; residue characteristic 2 would need a different lattice theory.

A4-8 (holds under D0, D3) gives the same over \(\mathbb F_q(\!(t)\!)\). Three routes, one conclusion: the sphere row is both-hold for all \(n\ge2\) (sheaves: Prop. III; functions: unconditional for \(q\) odd). Summary Table 1's '\(n\ge4\) open' is closed. Severity: none.

Sources

A6.json Proposition 6.3, Lemma 6.9
A1.json Proposition 1.3
A4.json Lemma 4.8
families/spin.html

Table 1. Page production by session
	tokens	US $
This conversation: the search, the audit, the pages and propositions, and the VI characteristic-p run01:44–05:19 UTC	802 M	$490
Setup pages16:17–19:42 UTC	37 M	$19
Shareable animation17:16–17:22 UTC	1 M	$1
Proposition IIb: figures and the linear-algebra lemma19:48–20:05 UTC	14 M	$7
Audit pass: the repairs by Agents X1–X4, their re-checks and Propositions VI–VII (with the audit skill)19:35–02:12 UTC	275 M	$113
Proposition IX: converse search, verdict and trace formalism19:56–02:12 UTC	199 M	$106
Audit pass on the VI characteristic-p run; the simplified VIb page and the VI corrections05:21–07:33 UTC	268 M	$107
Removing the detail switch; Proposition IX restated; the hub and verdict reviewed and simplified05:34–15:56 UTC	38 M	$20
C_K for the categorical statements, in the Iwahori run's conversation18:27–18:32 UTC	9 M	$3
Total	1,642 M	$866