# Attempt tree · Do orbit standards generate without finite orbit closures?

Started 2026-10-20T16:35:27Z · 3 rows · 26 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:46 · proved

```text
16:40  A1-1   ✓ Setup         Pieces of a level and the test point 0
16:40  A1-2   ✓ Lemma         The stalk at 0 is an exact test functor           ← A1-1
16:40  A1-3   ✓ Proposition   (a) Orbit standards do not generate               ← A1-1, A1-2
16:40  A1-4   ✓ Proposition   (b) Add one tail standard                         ← A1-1, A1-3
16:42  A1-5   ✓ Proposition   (c) Piece standards generate                      ← A1-4
16:42  A1-6   ✓ Lemma         Which orbit standards exist in C                  ← A1-1, A1-5
16:42  A1-7   ✓ Proposition   Criterion: when orbit standards suffice           ← A1-2, A1-5, A1-6
16:42  A1-8   ✓ Proposition   Criterion versus H1                               ← A1-6, A1-7
16:42  A1-9   ✓ Audit         Audit: tail coefficients, Ind, kernels            ← A1-3, A1-4, A1-6
16:44  A1-10  ✓ Summary       Verdict: pieces generate, orbits need (star)      ← A1-3, A1-4, A1-5, A1-7, A1-8, A1-9
```

## A2 · Auditor · round 2 · 16:46–16:58 · proved

```text
16:55  A2-1   ✓ Check         Pieces of a level: holds                          ← A1-1
16:55  A2-2   ✓ Check         Stalk functor: holds                              ← A1-2
16:55  A2-3   ✓ Lemma (repair R1) Stalks on a piece determine the object            ← A1-6, A1-3, A1-7
16:55  A2-4   ✓ Objection (minor, repaired) Thick span of shell standards = ker of stalk at   ← A1-3, A2-3
16:55  A2-5   ✓ Lemma (repair R2) Vanishing stalk at 0 puts F in the shell span, v  ← A1-3, A1-5, A2-3
16:55  A2-6   ✓ Objection (repaired) One extra tail standard generates; Ind witness:   ← A1-4, A2-7
16:55  A2-7   ✓ Lemma (repair R3) Shell standards have no maps to deeper tails      ← A1-4, A2-3
16:55  A2-8   ✓ Objection (hypothesis to add) Theorem G: holds once (L0) is added to (G)        ← A1-5
16:55  A2-9   ✓ Check         Visible orbits: holds given (L0), (L0′)           ← A1-6, A2-3, A2-8
16:55  A2-10  ✓ Check         Orbit-standard criterion (★): holds               ← A1-7, A2-3, A2-8
16:55  A2-11  ✓ Objection (scope) (★) ⇔ H1(a)_fin + H1(b) + visibility holds; two   ← A1-8, A2-12, A2-8
16:55  A2-12  ✓ Lemma (repair R4) H1(a)_fin and H1(b) do not force (★) for the axi  ← A1-8, A2-3
16:55  A2-13  ✓ Check         Tail coefficients: holds                          ← A1-9, A2-3
16:55  A2-14  ✓ Check         Summary against the question                      ← A1-10, A2-11, A2-8
16:55  A2-15  ✓ Verdict       A1's conclusions stand as repaired                ← A1-10, A2-3, A2-4, A2-5, A2-6, A2-7, A2-8, A2-11, A2-12
```

## R · root

```text
16:58  R-1    ✓ Summary       Verdict: pieces, not orbits                       ← A1-2, A1-3, A1-4, A1-5, A1-6, A1-7, A1-8, A2-3, A2-5, A2-7, A2-8, A2-11, A2-12, A2-15
```