Twisting argument (Serre, Cohomologie galoisienne I §5). Tori \(S_y\) with the same \(\dim W''_y\) are conjugate under \(\mathrm{SO}(W)(\bar F)\): \(S_y(\bar F)\) is the split torus of a hyperbolic frame of eigenvectors of \(P(y)\), and Witt’s extension theorem carries one frame to another of the same size; a conjugator \(g\) gives the cocycle \(\sigma \mapsto g^{-1}\sigma (g)\) in \(N_x=N_{\mathrm{SO}(W)}(S_x)\), and \(H^1(F,N_x)\) is finite. Equal classes give a Galois-fixed, hence rational, conjugator in \(\mathrm{SO}(W)(F)\), which lifts to \(\mathrm{GSpin}(W)(F)\) and conjugates the tori.

Each \(\theta _{\pi _i}\) lies in \(\mathrm{QC}(G,\eta _i)\) for its central character \(\eta _i\), and \(m_{\mathrm{geom}}\) is linear on the span of these spaces (Chapter 7).

The multiplicity formula for \((G_\alpha ,H_\alpha ,\xi _\alpha )\) and linearity of \(m_{\mathrm{geom}}\).

Not yet formalized. The regular nilpotent elements form one geometric orbit, whose rational orbits are indexed by a subset of \(H^1(F,Z_{G_x}(N))\), finite by Borel–Serre (1964), Thm. 6.1.

Not yet formalized. As in the proof of [ 5 ] , (3.4.7): \(G_{x,\mathrm{ad}}(F)\) acts transitively on \(\mathrm{Nil}_{\mathrm{reg}}(\mathfrak g_x)\), stability makes \(X\mapsto \theta (xe^X)\) invariant under it, and the local expansion is unique.

Not verbatim in the literature (adapted from, or derived from, published results); not yet formalized. Ingredients: [ 5 ] , (12.1.2), stated there for pure inner forms; its proof does not use purity.

Each regular germ of \(\theta \) and of \(\theta '\) equals the average (Lemmas 70 and 69); apply Theorem 71.

Apply the germ transfer to \(e(G_\alpha )\theta _1\) and \(\theta _\alpha \), using (STAB) and (TRANS).

By the classification of \(p\)-adic quadratic forms and Witt cancellation: if \(W''_{\alpha ,y}\) is \(0\) or a hyperbolic plane then \(W_\alpha \cong W\); \(\dim W''_{\alpha ,y}=1\) is impossible; otherwise a second class of the dimension and discriminant of \(W''_{\alpha ,y}\) exists.

\(W\) is the twist of \(W_\alpha \) by a cocycle in \(S_y\): twist \(W''_{\alpha ,y}\) into \(\iota (W'_{\alpha ,y})^\perp \) in block coordinates, a cocycle in \(SO(W_\alpha )_{W'_y}\), moved into \(S_y\) by [ 15 ] Lemma 10.2. Then the construction of Prop. 6.6.1(iii) for \(G_\alpha \) and the inverse twist \((W,\varphi _\alpha ^{-1})\), and symmetry of strong stable conjugacy.

Combine the two preceding lemmas.

The values of \(t\mapsto gC(\varphi _\alpha )(t)g^{-1}\) are Galois-fixed, hence rational (Galois descent); they commute with \(y\) and fix \(W'_y\). The inverse comes from \(g^{-1}\) and \(\varphi _\alpha ^{-1}\). Scalars are central and \(x\mapsto y\) by the choice of \(g\). \(e\) and \(e^{-1}\) are restrictions of \(F\)-linear maps \(C(W)\to C(W_\alpha )\), hence continuous. Stable conjugacy in \(G\) is Lemma 79. On \(T_{x,\natural }\) the centralizers of \(\bar t\) and \(\bar x\) in \(\mathrm{GSpin}(W)(\overline{F})\) and \(\mathrm{GSpin}(V)(\overline{F})\) agree (by the centralizer theorem, Theorem 7, and the commutativity of the Lie algebra of \(S_t\)); hence the rationality clauses for \(x\) give those for \(t\), and \(\mathrm{Ad}(g)\circ C(\varphi _\alpha )\) carries centralizers, fixed spaces and semisimplicity, so \(T_{x,\natural }\) and \(T_{y,\natural }\) correspond.

On \(V\) conjugate by the image of \(g\) under \(W_{\alpha ,\overline{F}}\subseteq V_{\alpha ,\overline{F}}\): the two compositions \(C(W)\to C(V_{\alpha ,\overline{F}})\) agree on \(W\).

\(h\) conjugates \((P(t)-1)|_{W''_t}\) to \((P(t')-1)|_{W''_{t'}}\); both determinants lie in \(F\).

\(\psi _\alpha \circ \mathrm{Ad}(g)\) conjugates \(1-\mathrm{Ad}t\) to \(1-\mathrm{Ad}t'\) over \(\overline{F}\); characteristic polynomials are unchanged by base change.

The torus isomorphism, with the invariance of \(\Delta \) and \(D^G\).

Speiser’s argument: average the cocycle over \(\mathrm{Gal}(L/F)\), \(L\) the normal closure of a field of definition, and use Dedekind’s independence of characters to find an invertible average \(B\) with \(a_\sigma \, \sigma (B)=B\) ( [ 21 ] , Ch. X §1 Prop. 3).

Hilbert 90 writes the cocycle as \(M^{-1}\sigma (M)\); \(v\mapsto Q(M^{-1}v)\) is an \(F\)-form of the discriminant of \(W\). Cohomologous cocycles give \(F\)-isometric forms by Galois descent.

Conjugation by \(x\) is a commuting product of left and right multiplication by elements of \(F[x]\), hence semisimple; it restricts to \(P(x)\) on \(\iota (W)\). Squarefree polynomials stay squarefree over \(\overline{F}\) in characteristic \(0\).

A skew \(Y\) lifts to \(\hat Y\in \mathfrak {gspin}(W_{\overline{F}})\) with \([\hat Y,v]=Y v\); \(\hat Y\) commutes with \(x\) (the difference \(x\hat Yx^{-1}-\hat Y\) is a traceless central element) and with \(W'_x\otimes \overline{F}\). These are \(F\)-linear conditions, so by flatness the \(\overline{F}\)-solutions are spanned by the \(F\)-solutions, which commute by the commutativity of the moved part of \(\mathfrak g_x\) over \(F\). Then \([[\hat Y_1,\hat Y_2],v]=[Y_1,Y_2]v\).

\(S_x(\overline{F})\) consists of the isometries of determinant \(1\) commuting with the semisimple \(P(x)\) and fixing \(W'_x\). If the corresponding Lie algebra is abelian, the eigenvalues \(\lambda \ne \pm 1\) of \(P(x)\) are simple and \(\dim E_{-1}\le 2\); the determinant on \(E_{-1}\) is \(1\), and Cayley–Hamilton on \(E_{-1}\) gives commutativity.

Not yet formalized. Galois-cohomological parametrization of stable classes, then Witt cancellation.

Own work, without Brauer groups (the statement is [ 5 ] , (12.1.6), with the sign of [ 14 ] ). \(e(G_\alpha )=1\) exactly when \(W_\alpha \cong W\). For a cocycle \(a\) in \(S_x\) choose lifts \(t_\sigma \in T_x(\bar F)\); the scalars \(t_\sigma \, \sigma (t_\tau )\, t_{\sigma \tau }^{-1}\) form its obstruction. Call \(a\sim b\) when they have lifts with equal obstructions; as \(T_x(\bar F)\) is commutative this is compatible with products. If \(W_\alpha \cong W_\beta \), a lift \(h\in \mathrm{GSpin}(W)(\bar F)\) of \(\varphi _a^{-1}\varphi _b\) (made proper by a rational reflection) conjugates a lift of \(a\) into one of \(b\), so \(a\sim b\); conversely \(a\sim b\) gives \(W_\alpha \cong W_\beta \) (Lemma 95). With at most two classes of the dimension and discriminant of \(W\), the sign is multiplicative.

Own work. The quotient \(v_\sigma =\varphi _1 s_\sigma t_\sigma ^{-1}\varphi _1^{-1}\) of the lifts is a \(1\)-cocycle in \(\mathrm{GSpin}(U_1)(\bar F)\), and \(C(\psi )\), \(\psi =\varphi _2\varphi _1^{-1}\), satisfies \(\sigma (C(\psi )z)=C(\psi )(v_\sigma \sigma (z)v_\sigma ^{-1})\). Hilbert 90 for the units of the central simple algebra \(C(U_1)\) (even dimension) or \(C^+(U_1)\) (odd dimension), deduced from Hilbert 90 for \(\mathrm{GL}_N\) and the fact that modules of equal dimension over a simple algebra are isomorphic, gives \(v_\sigma =u^{-1}\sigma (u)\); then \(z\mapsto C(\psi )(u^{-1}zu)\) is Galois-equivariant and descends to \(C(U_1)\cong C(U_2)\) (resp. \(C^+\)). The discriminants agree since \(\det \psi \) is Galois-fixed, so \(U_1\cong U_2\) by the classification of quadratic forms over \(F\) by rank, discriminant and Clifford invariant.

Over \(\bar F\) the plane is hyperbolic with hyperbolic pair \(f,f'\); \(\mathrm{SO}(\Pi )(\bar F)\) is the split torus scaling \(f,f'\) by \(t^{-1},t\), lifted to \(\mathrm{GSpin}\) by \(ff'+t\, f'f\), which commutes with \(x\) and fixes \(W'_x\), so it lies in \(S_x\). Twisting \(\Pi \) into the other binary form of its discriminant gives a cocycle with these values; the twisted form is not isometric to \(W\) by Witt cancellation.

On a line \(P(x)\) is the reflection in it, of determinant \(-1\). On a hyperbolic plane with hyperbolic pair \(f,f'\), \(P(x)\) is diagonal on \(f,f'\) (else it is a reflection), so the lifts \(h(s)=ff'+s\, f'f\) of the hyperbolic torus commute with \(x\) and lie in \(T_x(F)\), acting by \(s\) on \(f\): this contradicts compactness of \(T_x(F)/A(F)\).

Twist the block \(W''_x\) into the other form of its dimension and discriminant; the cocycle lies in \(SO(W)_{W'_x}\), so by [ 15 ] Lemma 10.2 it is cohomologous to one in \(S_x\); Witt cancellation.

\(W''_x\neq 0\) since \(x\) is not central; Lemmas 97 and 98.

Lemma 99.

From the previous lemma: if \(W_\alpha \not\cong W\) then \(e(G_\alpha )=-1\), since two \(p\)-adic forms of the same dimension and discriminant have Witt indices of opposite parity in odd dimension and of the same parity in even dimension.

The sum equals \(\sum _{\beta \in H^1(F,S_x)}e(G_{q_x(\beta )})\). If \(x\) is central this is \(e(G)=1\). Otherwise the sign is a character of the finite group \(H^1(F,S_x)\) taking the value \(-1\), so the sum vanishes.

Not yet formalized. Regroup by stable classes; \(n_\alpha (x)=|q_x^{-1}(\alpha )|\), and the rational classes of tori over \(\alpha \) are the orbits of \((N_x/S_x)(F)\) on \(q_x^{-1}(\alpha )\subseteq H^1(F,S_x)\), with stabilizers \(W(T')\) (orbit–stabilizer).

Torus by torus: non-quasi-split tori contribute \(0\); a quasi-split torus \(T_y\) of \(G_\alpha \) has \(\int _{T_y/A}=e(G_\alpha )\int _{T_x/A}\) for \(x\sim _{\mathrm{stab}}y\) (the torus transfer identifies the probability Haar measures, \(D^G\) and \(\Delta \); germ transfer at the regular orbits \(\mathcal O_x\), \(\mathcal O_y\)); regroup with the torus-class count; the stable weight is constant on \(T_{x,\natural }\).

The rearrangement at \(s{\gt}0\), and the finite sum over \(\alpha \) commutes with the limit.

\(\theta _1(cy)=\theta _1(y)\) on \(G_{\mathrm{reg}}(F)\) since the central characters are trivial on \(Z_{G,H}(F)\); \(e^X\) is regular for small regular \(X\), so the expansion at \(1\) is one at \(c\) (uniqueness of germs); \(\mathcal O_c=\mathcal O_1\).

Direct computation, with central translation of the germ.

Non-central and non-quasi-split classes have weight \(0\); the atom gives the value above.

Luo’s split family for the descended datum \((W'_x,V'_x)\), carried into \(V\) (or \(W\)) by the isometric embedding, paired with a regular element of the other factor.

Lemma 109.

Luo’s recipe applied to \((G,H)\) selects a regular orbit, which exists since \(G\) is quasi-split.

Sum (6.7.2) over \(\alpha \); rearrange by (6.7.5) using germ transfer and Prop. 6.6.1(i),(ii); the signed count kills every class but the atom.