§6 · Agent 6 · E₆/F₄: restriction map · 2026-10-17T02:30:06Z

Proposition 6.3 · $\Spin_{2n}/\Spin_{2n-1}$: $r$ is onto for every $n\ge2$, so (SG) holds under (A1)–(A5)

proved audit: correct

Second audit: correct. No defect. Data, rho_L=(0,n-2,...,1,0) and c_n(q) recomputed for n=2..7 (only u^{+-1} and constants occur; coefficients match). (A5) argument correct, also for n=2 where Spin(W) is a torus; B.x_0 is open since dim B - dim(B cap H) = n^2-(n-1)^2 = 2n-1.

For the spheres the orbit sum of the roots of $D_n$ restricts to a positive multiple of $u+u^{-1}$ plus a constant, which already generates the target; by Theorem E, spherical generation holds for every $n\ge2$ under Sakellaridis's hypotheses. Of these, (A1) and (A5) are checked here and (A2)–(A4) are not.

Proposition 6.3.

Let $X=\Spin_{2n}/\Spin_{2n-1}$, $n\ge2$, with the restriction map $r$ of Setup 6.1, and let $u:=y(2\varepsilon_1)$ be the coordinate on $A_X^*$. Then $$r(m_{\varepsilon_1+\varepsilon_2})=c_n(q)\,(u+u^{-1})+\mathrm{const},\qquad c_n(q)=\sum_{j=2}^{n}\bigl(q^{\,n-j}+q^{\,j-n}\bigr)=2+\sum_{k=1}^{n-2}(q^k+q^{-k})>0,$$ so $\operatorname{im}r=\C[u+u^{-1}]$ and $r$ is onto. By Theorem E(2), (SG) holds for $X$ under (A1)–(A5). For this $X$, (A1) and (A5) hold; (A2)–(A4) are not verified.

Data (the $\Spin_{2n}/\Spin_{2n-1}$ family page). $\Lambda_T=\{x\in\Z^n:\sum_ix_i\text{ even}\}$, $W=W(D_n)$, $\theta=\operatorname{diag}(-1,1,\dots,1)$, $\varphi(x)=2x_1\varepsilon_1$, $\Lambda_S=\Z\cdot2\varepsilon_1$, and $W_X=\Z/2$ acts by $-1$ on $\Lambda_S$. The roots of $L$ are $\Phi_L=\{\pm\varepsilon_i\pm\varepsilon_j:2\le i<j\le n\}$, of type $D_{n-1}$, so $\rho_L=(0,n-2,n-3,\dots,1,0)$. With $u=y(2\varepsilon_1)$ the restriction sends $x^\mu\mapsto q^{\langle\rho_L,\mu\rangle}u^{\mu_1}$, and the target is $\C[u^{\pm1}]^{u\leftrightarrow u^{-1}}=\C[u+u^{-1}]$.

Proof.

$\varepsilon_1+\varepsilon_2\in\Lambda_T$, and its $W$-orbit is the set of roots, so $m_{\varepsilon_1+\varepsilon_2}=\sum_{i<j}\sum_{\pm,\pm}x^{\pm\varepsilon_i\pm\varepsilon_j}\in\C[A^*]^W$.
The terms with $i=1$ restrict to $q^{\pm\langle\rho_L,\varepsilon_j\rangle}u^{\pm1}=q^{\pm(n-j)}u^{\pm1}$, because $\langle\rho_L,\varepsilon_1\rangle=0$; the sign on $u$ is that of $\varepsilon_1$ and the sign of the $q$-exponent is that of $\varepsilon_j$, independently. Summing over $j=2,\dots,n$ gives $c_n(q)u+c_n(q)u^{-1}$.
The terms with $2\le i<j$ have no $\varepsilon_1$-component and restrict to constants.
Hence $u+u^{-1}=c_n(q)^{-1}\bigl(r(m_{\varepsilon_1+\varepsilon_2})-\mathrm{const}\bigr)\in\operatorname{im}r$, and since $\operatorname{im}r$ is a subring, $\operatorname{im}r=\C[u+u^{-1}]$.
Theorem E(2) turns this surjectivity into (SG), under (A1)–(A5).

For $n=2,3$ the result agrees with Table 1 of the classical page: $\Spin_4/\Spin_3$ is the group $\SL_2$, and $\Spin_6/\Spin_5\simeq\SL_4/\Sp_4$. Exact computation gives the coefficient of $u^{\pm1}$ as $q^{-2}+q^{-1}+2+q+q^{2}$ for $n=4$ and $q^{-3}+q^{-2}+q^{-1}+2+q+q^2+q^3$ for $n=5$, as predicted; also $r(m_{2\varepsilon_1})=u^2+u^{-2}+\mathrm{const}$.

Status of the hypotheses for the spheres.

(A1): $\Spin_{2n}$ is split and simply connected.
(A5): as in Lemma 6.9, $B\cap H=B_L\cap L^\theta$, and $L^\theta=S[2]\cdot\Spin(V_0)=\Spin(V_0)$ for $V_0=\langle e_2,\dots,e_{2n-1}\rangle\subseteq\C^{2n}$, because $S[2]=\{\pm1\}\subseteq\Spin(V_0)$ when $\dim V_0\ge2$. So $B\cap H$ is a Borel subgroup of $\Spin(V_0)$, hence connected, and the $H^1$-argument of the classical page (the remark on (A5) after Theorem E) shows that $\mathring X(F)$ is a single $B(F)$-orbit. Moreover $\Spin_{2n}(F)$ is transitive on $Q(F)$, where $Q=\{x\in\C^{2n}:x^{\mathsf T}Jx=2\}\simeq X$ is the quadric model of the family page, since the spinor norm of the split group $\SO_{2n-1}(F)$ is onto $F^\times/F^{\times2}$.
(A2)–(A4) are not verified here; the sphere is not in Sakellaridis's table.

Verified by computation: dn_sphere.py.

Builds on

Setup 6.1 · Conventions for Sakellaridis's restriction map $r$, calibrated on Proposition F; the sign of the shift is irrelevant
Lemma 6.2 · Two criteria for the surjectivity of $r$: monoid generators suffice, and a glued pair of points forbids it

Built on by

Lemma 6.9 · Status of Sakellaridis's hypotheses (A1)–(A5) for $E_6/F_4$ and the spheres
Summary 6.10 · Verdict for this family: the spheres hold at both levels; $E_6/F_4$ fails at the function level under (A), sheaf level open
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

Original record, as the agent wrote it at 02:30 UTC

Spheres Spin(2n)/Spin(2n-1): r is onto for every n at least 2, so (SG) holds under (A)

Data (families/spin.html): $\Lambda_T=\{x\in\mathbb Z^n:\sum x_i\ \text{even}\}$, $W=W(D_n)$, $\theta=\operatorname{diag}(-1,1,\dots,1)$, $\varphi(x)=2x_1\varepsilon_1$, $\Lambda_S=\mathbb Z\cdot2\varepsilon_1$, $W_X=\mathbb Z/2$ acting by $-1$ on $\Lambda_S$, $\Phi_L=\{\pm\varepsilon_i\pm\varepsilon_j:2\le i<j\le n\}$ (type $D_{n-1}$), so $\rho_L=(0,n-2,n-3,\dots,1,0)$. Put $u:=y(2\varepsilon_1)$, the coordinate on $A_X^*$; then $x^\mu\mapsto q^{\langle\rho_L,\mu\rangle}u^{\mu_1}$. Target: $\mathbb C[u^{\pm1}]^{u\leftrightarrow u^{-1}}=\mathbb C[u+u^{-1}]$.

Computation. For the adjoint orbit sum $m_{\varepsilon_1+\varepsilon_2}=\sum_{i<j}\sum_\pm x^{\pm\varepsilon_i\pm\varepsilon_j}\in\mathbb C[A^*]^W$ (note $\varepsilon_1+\varepsilon_2\in\Lambda_T$): $$r(m_{\varepsilon_1+\varepsilon_2})=c_n(q)\,(u+u^{-1})+\text{const},\qquad c_n(q)=\sum_{j=2}^{n}\bigl(q^{\,n-j}+q^{\,j-n}\bigr)=2+\sum_{k=1}^{n-2}(q^k+q^{-k})>0,$$ since the terms with $i=1$ are $q^{\pm\langle\rho_L,\varepsilon_j\rangle}u^{\pm1}$ with $\langle\rho_L,\varepsilon_1\rangle=0$, and the terms with $i,j\ge2$ are constants. Hence $u+u^{-1}\in\operatorname{im}r$ and, $\operatorname{im}r$ being a ring, $\operatorname{im}r=\mathbb C[u+u^{-1}]$: $r$ is onto. By Theorem E(2), (SG) holds for $\mathrm{Spin}_{2n}/\mathrm{Spin}_{2n-1}$, $n\ge2$, under (A1)–(A5). Consistent with $n=2,3$ ($\mathrm{SL}_2$, $\mathrm{SL}_4/\mathrm{Sp}_4$, classical.html Table 1).

Machine check (dn_sphere.py, exact): $n=4$: coefficient of $u^{\pm1}$ is $q^{-2}+q^{-1}+2+q+q^{2}$; $n=5$: $q^{-3}+q^{-2}+q^{-1}+2+q+q^2+q^3$, as predicted. Also $r(m_{2\varepsilon_1})=u^2+u^{-2}+\text{const}$.

Status of the hypotheses for the spheres: (A1) $\mathrm{Spin}_{2n}$ is split simply connected; (A5) holds: as in A6-9, $B\cap H=B_L\cap L^\theta$ and $L^\theta=S[2]\cdot\mathrm{Spin}(W)=\mathrm{Spin}(W)$ ($S[2]=\{\pm1\}\subseteq\mathrm{Spin}(W)$, $\dim W\ge2$), so $B\cap H$ is a Borel of $\mathrm{Spin}(W)$, connected, and the $H^1$-argument of classical.html §4 gives one $B(F)$-orbit; moreover $\mathrm{Spin}_{2n}(F)$ is transitive on $Q(F)$ (spinor norm of the split $\mathrm{SO}_{2n-1}(F)$ is onto $F^\times/F^{\times2}$). (A2)–(A4) are not verified here (gap; the sphere is not in Sakellaridis's table).

Sources

families/spin.html §1–5
classical.html#4 (A1)–(A5), Theorem E
dn_sphere.py

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