# Attempt tree · The induction in “ICs and standards span alike”

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:44 · proved

```text
16:37  A1-1   ✓ Setup         The statement and the induction variable
16:38  A1-6   ~ Computation   Order facts checked on two dominance orders       ← A1-1
16:39  A1-2   ✓ Lemma         Boundary term is standard-generated               ← A1-1
16:39  A1-3   ✓ Lemma         IC in the standard span, no induction             ← A1-1, A1-2
16:39  A1-4   ✓ Lemma         Strict down-set equality from the hypothesis      ← A1-1, A1-3
16:39  A1-5   ✓ Proposition   Step 5 written out, hypothesis marked             ← A1-1, A1-2, A1-3, A1-4
16:40  A1-7   ✓ Counterexample One orbit alone: spans differ                     ← A1-2, A1-3, A1-6
16:41  A1-8   ✓ Remark        The reader's reading, corrected                   ← A1-4, A1-5, A1-7
16:41  A1-9   ✓ Summary       Verdict                                           ← A1-5, A1-7, A1-8
```

## A2 · Auditor · round 2 · 16:44–16:51 · proved

```text
16:48  A2-1   ✓ Audit         Audit of A1-1                                     ← A1-1
16:48  A2-2   ✓ Audit         Audit of A1-2                                     ← A1-2
16:48  A2-3   ✓ Audit         Audit of A1-3                                     ← A1-3
16:48  A2-4   ✓ Audit         Audit of A1-4                                     ← A1-4, A2-1
16:49  A2-5   ✓ Audit         Audit of A1-5                                     ← A1-5, A2-2, A2-3, A2-4, A2-6
16:49  A2-6   ✓ Supplement    Induction-free hard inclusion under PH            ← A2-5
16:49  A2-7   ~ Audit         Audit of A1-6                                     ← A1-6
16:50  A2-8   ✓ Audit         Audit of A1-7                                     ← A1-7
16:50  A2-9   ✓ Repair        Neither inclusion holds for one orbit             ← A1-7, A2-8
16:50  A2-10  ✓ Audit         Audit of A1-8                                     ← A1-8, A2-4, A2-8, A2-9
16:50  A2-11  ✓ Audit         Audit of A1-9 and completeness                    ← A1-9, A2-1, A2-2, A2-3, A2-4, A2-5, A2-8, A2-10
16:50  A2-12  ✓ Verdict       Verdict of the 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
16:52  R-1    ✓ Summary       Verdict: induction on down-sets                   ← A1-1, A1-2, A1-3, A1-4, A1-5, A1-7, A1-8, A2-5, A2-6, A2-8, A2-9, A2-12
```