# Verdict: top class and symmetry in the top-restriction lemma

Origin: Toan, 2026-10-20 05:40, on `proof_graphs/spherical-generation/nodes/split.html`, step 6.

| statement | status | steps |
|---|---|---|
| I. \(H^{2e}_c(U)\ne0\) and survives into the stalk; weight-free alternative in degree \(-d\) | proved (in-run audit) | A1-1–A1-3, A1-7, A2-2, A2-4, A2-8 |
| II. S1–S4 ⇒ H5 uses no symmetry; general lemma with (Q0)–(Q2) | proved (in-run audit, A1-8 repaired by A2-10) | A1-5, A1-6, A2-6, A2-7, A2-9, A2-10 |

## Proposition I: the top class survives (proved)
**Assumes.** \(X\) affine; for the weight route, the \(\overline{\mathbb F}_q\) model and transfer to \(\mathbb C\) as on the pages.
**Statement.** \(F=\{g\in\mathrm{Gr}_{\le\lambda}:g^{-1}t^\lambda x_0\in L^+X\}\) is projective and \(t^\lambda\in U=F\cap\mathrm{Gr}_\lambda\). (a) \(\dim H^{2e}_c(U)=\#\{\)components of \(U\) of dimension \(e\}\ge1\), pure of weight \(2e\). (b) \(H^{2e}_c(U)\hookrightarrow H^{2e-d}((V_\lambda\ast\mathrm{IC}_0)_{t^\lambda x_0})\). (c) Without weights: the stalk at every \(y\in\mathrm{Gr}_{\le\lambda}\cdot L^+X\) contains \(k^{\pi_0(F_y)}\) in degree \(-d\).
**Proof.** 1. Fibre and stalk formula by proper base change at a finite level [[A1-1]], [[A2-2]]. 2. Top cohomology counts top components (trace map) [[A1-2]]. 3. The connecting map goes from weights \(\le2e-1\) to the pure weight-\(2e\) group, so vanishes (BBD 5.1.14(i)) [[A1-3]], [[A2-4]]. 4. \(\mathcal H^{-d}V_\lambda\supseteq\underline k\) (Deligne's formula, BBD 2.1.11), and \(H^0\) is left exact [[A1-7]], [[A2-8]].

## Proposition II: where symmetry enters (proved)
**Statement.** (a) The deduction S1–S4 ⇒ H5 uses only S1–S4, the closure order and H2 [[A1-5]], [[A2-6]]. (b) Symmetry is used to verify the inputs: S1 through the support bound (Prop. III, Lemma 3.1); S3 through \(Z_K(S)\) connected (Lemma 3.2; only "⇒" at fixed \(\lambda\), e.g. \(\mathrm{SL}_2/\mathrm{SO}_2\), \(\lambda=0\)); S4 through \(t^\lambda x_0=x_{\varphi(\lambda)}\) (Chen–Yi Prop. 17(i) and injectivity of \(\tau\)) [[A1-6]], [[A2-7]], [[A2-9]]. (c) For smooth affine \(X\) with (Q0) \(L^+X\) one orbit, (Q1) finiteness and placidity of \(Y_\lambda=\mathrm{Gr}_{\le\lambda}\cdot L^+X\), (Q2) a connected stabilizer at its dense orbit \(\psi(\lambda)\): \(\lambda\) satisfies H5 at \(\psi(\lambda)\), and only there; \(\psi(\lambda)=\varphi(\lambda)\) is exactly the support bound [[A2-10]].

## Gaps
- Unchecked classical numbers (no local text): SGA 4 XVII/XVIII, Hodge III 8.2.4, Saito, BBD §6. For non-symmetric \(X\), (Q1), (Q2) must be checked family by family.

## Routes ruled out
- (P1) from Chen–Yi Remark 37: it gives placidity only; finiteness fails for \(\mathbb A^1\) under \(\mathbb G_m\).

## Proposed edit (split.html, step 6)
Replace the weight argument by: "\(\mathcal H^{-d}(V_\lambda)\supseteq\underline k\), so \(H^{-d}\) of the stalk at \(x_\mu\) contains \(H^0(F,k)\ne0\) (\(t^\lambda\in F\))"; keep the weight argument as a remark, adding "\(\dim H^{2e}_c(U)\) = number of \(e\)-dimensional components". In "For a symmetric space", name the three uses of symmetry: support bound, \(Z_K(S)\) connected, \(t^\lambda x_0=x_{\varphi(\lambda)}\).