docs(wager): Stage 8, 3 corrections from the review of #101 (#102)

## Summary

A follow-up of #101, which is merged. It has the 3 corrections that the
automated review of #101 asked for. Each is a comment or a record. No
statement and no proof changes.

## Changes

- `Wager/Poly/Statements.agda`: the comment of `T8-Closed` said that T0
to T6 apply to each closed instance. That was too strong. The comment
now follows DC-8.3: a theorem about each typed target term applies under
its own hypotheses; T3, T5 and T6 are about the translation of a source
program; T2 and T4 are about types. The type of the statement did not
change.
- `Wager/Poly/Proofs.agda`: the header names each proof of the module.
- `Wager/TOOLCHAIN.adoc`: the last row of the gate watch of Stage 8
records the run with 91 files only, and points to the row of the side
item for the run with 96 files.

Not in this pull request: the failed check "Deposit findings for
gitbot-fleet" on #101. It is CI work, and this session does proof work
only.

## RSR Quality Checklist

### Required

- [x] Tests pass: `scripts/check-proofs.sh agda` passes with 96 modules,
and `scripts/check-proof-status.sh` passes. `just test` and `just
quality` were not run.
- [ ] Code is formatted: not run.
- [ ] Linter is clean: not run.
- [x] No banned language patterns in the changed files
- [x] No banned functions
- [x] SPDX license headers present on the changed source files
- [x] No secrets, credentials, or `.env` files included

## Testing

- `scripts/check-proofs.sh agda`: PASS, 96 gated modules.
- `scripts/check-proof-status.sh`: PASS.

---
_Generated by [Claude
Code](https://claude.ai/code/session_0136P7ZkUXubpMrTvbNd6qRK)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

verification/proofs/agda/Wager/Poly/Proofs.agda

@@ -4,7 +4,9 @@
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 --
--- Stage 8. Proofs of T8-Conv, T8-Inst and T8-Closed.
+-- Stage 8. Proofs of T8-Conv, T8-Inst, T8-Closed, T8-Closed-Instance,
+-- T8-Instance-Progress and T8-Instance-Preservation. The lemmas `sub-⇑`
+-- and `⇑-closed` are also used by `Wager.Poly.CoercionProofs`.
 open import Wager.L1.Signature
 open import Wager.Grade.Algebra
 import Wager.L2.Signature

verification/proofs/agda/Wager/Poly/Statements.agda

@@ -34,8 +34,11 @@ T8-Inst = ∀ {Δ Δ' n} (σ : TySub Δ' Δ) {γ : Usage n} {Γ : Cxᵖ Δ n}
           γ ▸ (λ i → sub σ (Γ i)) ⊢ᵖ inst σ t ∶ sub σ A
 
 -- T8-Closed. A typed term with no type variable is a typed term of the
--- target calculus of stages 1 to 5. So T0 to T6 apply to each closed
--- instance of an open term.
+-- target calculus of stages 1 to 5. A theorem about each typed target
+-- term, such as T0, thus applies to each closed instance of an open
+-- term, under its own hypotheses. T3, T5 and T6 are about the
+-- translation of a source program, and T2 and T4 are about types
+-- (DESIGN-CHOICES.adoc, DC-8.3). The statement below did not change.
 T8-Closed : Type
 T8-Closed = ∀ {n} {γ : Usage n} {Γ : Cxᵖ [] n} {t : Tmᵖ [] n} {A : Ty [] ★} →
             γ ▸ Γ ⊢ᵖ t ∶ A → γ ▸ Γ ⊢ ⌊ t ⌋ ∶ A

verification/proofs/agda/Wager/TOOLCHAIN.adoc

@@ -483,7 +483,7 @@ Each row is one change, alone. After each change the 2 commands `agda --safe Wag
 
 | All changes removed
 | None
-| PASS. The gate passed with 91 files before the watch. After the watch it ran with the 5 files of the side item: PASS, 96 files.
+| PASS, 91 files. This run was before the watch. The run after the watch had the 5 files of the side item also: see the last row of the next table.
 |===
 
 The second and the third test show that the proof of `T8-Closed` depends on the map `⌊_⌋` and on the text of a rule.