§7 · Agent 7 · Adversarial audit · 2026-10-17T03:43:09Z

Audit 7.21 · Audit of \(\GL_n/(\GL_p\times\GL_q)\) in the pair model: normal form, componentwise bound and \((\mathrm{SG})\) over every \(F\)

proved audit: correct

Second audit: correct. Every step agrees with my independent re-derivation of Theorem 5.4 (and with computations over \(\F_2[[t]]\)).

An independent check of Theorem 5.4: the Goursat normal form classifies the orbits, the quotient-module argument gives the componentwise support bound, and Proposition B gives \((\mathrm{SG})\) in every residue characteristic for the pair model, which coincides with the involution model exactly when \(2\) is a unit.

Audit 7.21.

Theorem 5.4 holds: \(K\backslash X(F)\leftrightarrow\{a_1\ge\dots\ge a_p\ge0\}=\Lambda_S^+\), the componentwise support bound, and \((\mathrm{SG})\) over every \(F\), for the pair model. Severity: none.

  1. Normal form. For a lattice \(L\subset U\oplus V\), \(L/(A'\oplus B')\) is the graph of an isomorphism \(\psi:A/A'\to B/B'\): the kernel of the projection to \(A/A'\) is zero, because \(\pi_Ul\in A'=L\cap U\) implies \(l-\pi_Ul\in L\cap V=B'\). Take a stacked basis \(u_i\) of \(A\) with \(A'=\bigoplus\varpi^{a_i}\cO u_i\). The lifts \(v_i\) of \(\psi(\bar u_i)\) (\(a_i>0\)) are independent modulo \(\varpi B\), since their images form a basis of \((B/B')\otimes\F_q\); they extend to a basis of \(B\), and the extra vectors are moved into \(B'\) by subtracting their \(\psi\)-components. An index count gives \(B'=\bigoplus\varpi^{a_i}\cO v_i\oplus\bigoplus\cO v_j\). Hence \(L=\bigoplus_i(\varpi^{a_i}\cO u_i+\varpi^{a_i}\cO v_i+\cO(u_i+v_i))\), a normal form determined by \(a=\mathrm{type}(\pi_VL/L\cap V)\), with at most \(p=\operatorname{rk}V\) nonzero \(a_i\). So \(K\backslash X(F)\leftrightarrow\Lambda_S^+\) for every \(F\).
  1. Support bound. \(L'=g^{-1}L_0\supseteq L_0\) with \(L'/L_0\simeq\bigoplus\cO/\varpi^{\lambda_i}\). Since \(x_0\in X(\cO)\) means \(L_0=(L_0\cap U_0)\oplus(L_0\cap V_0)\), we have \(\pi_{V_0}(L_0)\subseteq L'\cap V_0\); so \(\pi_{V_0}(L')/(L'\cap V_0)\) is a quotient of \(L'/L_0\), and its type is componentwise at most \(\lambda\) (the number of parts \(\ge j\) drops under quotients, so the conjugate partitions and then the partitions drop componentwise). The componentwise order has finite lower sets, \(f_a=T_{(a,0,\dots,0)}\) has value \(\ge1\) at \(t^\lambda x_0\in O_a\), and Proposition B gives \((\mathrm{SG})\) for every \(F\).
  1. Pair model versus involution model. The involution model's base point is the pair of \(\pm1\)-eigenspaces of \(J\), which is defined over \(\cO\) iff \(2\in\cO^\times\). For \(q\) odd the two models and their basic functions agree; for \(q\) even they differ (the label \((\val2,\dots,\val2)\) of the involution base point is plausible and immaterial). Over \(\F_q(\!(t)\!)\), \(q\) odd, the conclusion coincides with Lemma 4.8, which needed the dictionary inputs 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.; Theorem 5.4 needs neither.

Builds on

  • Theorem 5.4 · \(\GL_n/(\GL_p\times\GL_q)\), pair model: orbits, lifts, a componentwise support bound and \((\mathrm{SG})\) over every \(F\)
  • 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.25 · Updated audit verdict: every row of Table 1 except \(E_6/F_4\) is decided at both levels
  • Lemma X3.1 · The pair model as rank-\((n-p)\) projectors; its orbit label is a polar Smith part
  • Summary X3.7 · A7-25, A7-32 re-derived; the \(\mathrm{GL}_n/(\mathrm{GL}_p\times\mathrm{GL}_q)\) row
Original record, as the agent wrote it at 03:43 UTC

A5-4 GL_n/(GL_p x GL_q) pair model: normal form, componentwise bound and (SG) over every F hold

Normal form (i) (holds). For a lattice \(L\subset U\oplus V\): \(L/(A'\oplus B')\) is the graph of an isomorphism \(\psi:A/A'\to B/B'\) (kernel of the projection to \(A/A'\) is \(0\) because \(\pi_Ul\in A'=L\cap U\Rightarrow l-\pi_Ul\in L\cap V=B'\)). Stacked basis \(u_i\) of \(A\) with \(A'=\oplus\varpi^{a_i}\mathcal Ou_i\); the lifts \(v_i\) of \(\psi(\bar u_i)\) (\(a_i>0\)) are independent mod \(\varpi B\) (the \(\bar v_i\) are a basis of \((B/B')\otimes k\)), extend to a basis of \(B\), and the extra vectors are moved into \(B'\) by subtracting their \(\psi\)-components; index count gives \(B'=\oplus\varpi^{a_i}\mathcal Ov_i\oplus\oplus\mathcal Ov_j\). Hence \(L=\oplus_i(\varpi^{a_i}\mathcal Ou_i+\varpi^{a_i}\mathcal Ov_i+\mathcal O(u_i+v_i))\), an \(H(F)\)-normal form determined by \(a=\mathrm{type}(\pi_VL/L\cap V)\), with at most \(p=\mathrm{rk}\,V\) nonzero \(a_i\). \(K\backslash X(F)\leftrightarrow\{a_1\ge\dots\ge a_p\ge0\}=\Lambda_S^+\), any \(F\). ✓

Support bound (iii) (holds). \(L'=g^{-1}L_0\supseteq L_0\), \(L'/L_0\simeq\oplus\mathcal O/\varpi^{\lambda_i}\); since \(x_0\in X(\mathcal O)\) means \(L_0=(L_0\cap U_0)\oplus(L_0\cap V_0)\), \(\pi_{V_0}(L_0)\subseteq L'\cap V_0\), so \(\pi_{V_0}(L')/(L'\cap V_0)\) is a quotient of \(L'/L_0\) and its type is componentwise \(\le\lambda\) (number of parts \(\ge j\) decreases under quotients, hence conjugate partitions and then partitions decrease componentwise). Componentwise order has finite lower sets; \(f_a=T_{(a,0,\dots)}\) with \(t^\lambda x_0\in O_a\) and value \(\ge1\). Proposition B \(\Rightarrow\) (SG), every \(F\). ✓

Pair model vs \(J\)-model. The \(J\)-model's base point is the \(\pm1\)-eigenspace decomposition of \(J\), which exists over \(\mathcal O\) iff \(2\in\mathcal O^\times\); for \(q\) odd the two models and their \(\varphi_0\) agree, for \(q\) even they differ (A5's label \((\mathrm{val}\,2,\dots)\) for the \(J\)-point is plausible and immaterial). Over \(\mathbb F_q(\!(t)\!)\), \(q\) odd, the conclusion coincides with A4-8 (which needed D0, D3); A5-4 needs neither. Holds; severity none.

Sources