# Attempt tree · Top class and symmetry in the top-restriction lemma

Started 2026-10-20T16:35:27Z · 3 rows · 22 steps · final step R-1 · verdict proved

Status: ✓ proved · ✗ refuted · ⊘ blocked · ? open · ~ heuristic · ↺ superseded · ◐ partial. "← a, b": the step cites a and b. [error], [minor], [inherited]: audit grade.

## A1 · Solver · round 1 · 16:36–16:49 · proved

```text
16:41  A1-1   ✓ Lemma         The fibre F and the stalk formula
16:41  A1-2   ✓ Lemma         Top cohomology counts top components
16:42  A1-3   ✓ Proposition   Weights kill the connecting map                   ← A1-1, A1-2
16:42  A1-4   ✓ Example       Group case: U is a point                          ← A1-1, A1-3
16:42  A1-5   ✓ Audit         S1–S4 imply H5 with no symmetry
16:43  A1-6   ✓ Audit         Every use of symmetry in S1–S4                    ← A1-1, A1-2, A1-3, A1-5
16:44  A1-7   ✓ Lemma         Weight-free nonvanishing in degree -d             ← A1-1
16:45  A1-8   ✓ Proposition   Top restriction for affine spherical X            ← A1-5, A1-6, A1-7
16:46  A1-9   ✓ Summary       Verdict: claim holds; lemma uses no symmetry      ← A1-1, A1-2, A1-3, A1-4, A1-5, A1-6, A1-7, A1-8
```

## A2 · Auditor · round 2 · 16:49–17:03 · proved

```text
16:57  A2-1     Check         Audit of A1-1: fibre, properness, stalk formula   ← A1-1
16:58  A2-2   ✓ Lemma         Repair: finite-level stalk formula, no symmetry   ← A1-1
16:58  A2-3     Check         Audit of A1-2: top compactly supported cohomolog  ← A1-2
16:59  A2-4     Check         Audit of A1-3: the weight argument                ← A1-3, A2-3, A2-2
16:59  A2-5     Check         Audit of A1-4: group case                         ← A1-4
16:59  A2-6     Check         Audit of A1-5: S1–S4 ⇒ H5 is symmetry-free        ← A1-5
17:00  A2-7     Objection     Audit of A1-6: the symmetry table                 ← A1-6, A2-2
17:00  A2-8     Check         Audit of A1-7: weight-free nonvanishing           ← A1-7, A2-2
17:00  A2-9     Objection     Audit of A1-8: general spherical statement        ← A1-8, A2-8
17:01  A2-10    Lemma         Repair: top restriction for an affine G-variety   ← A1-8, A2-8, A2-9, A2-6, A2-2
17:01  A2-11    Check         Audit of A1-9 against the QUESTION                ← A1-9, A2-2, A2-8, A2-9, A2-10
17:02  A2-12    Verdict       Verdict of the adversarial audit                  ← A2-1, A2-2, A2-3, A2-4, A2-5, A2-6, A2-7, A2-8, A2-9, A2-10, A2-11
```

## R · root

```text
17:03  R-1    ✓ Summary       Verdict: top class; symmetry only in inputs       ← A1-1, A1-2, A1-3, A1-5, A1-6, A1-7, A2-2, A2-4, A2-6, A2-7, A2-8, A2-9, A2-10, A2-12
```