docs(CLAIMS_AUDIT): verify mappings — add VERDICT + EVIDENCE columns

Verification pass against `session/slice-4-narrowing` HEAD: every
proposed `(module, theorem)` mapping checked by grep against the
actual source.

Schema change: surface inventory and phrase sweep both extended
from 5 → 7 cols (added VERDICT + EVIDENCE). Verdict scheme:

* MATCHES — theorem(s) mechanise the sentence as written
* WEAKER-THAN-CLAIM — codebase supports a strictly weaker form
  (pointwise vs strict, K-free skeleton vs full HoTT, partial
  closure vs umbrella)
* NO-BACKING — no theorem in the codebase backs the sentence
* CONJECTURE-OK — sentence is openly a non-claim (positioning,
  scope, retraction citation, `NONE-PROPOSED`, `LOCATE-FAILED`)
  and that is honest

Totals: MATCHES 70, WEAKER-THAN-CLAIM 4, NO-BACKING 0,
CONJECTURE-OK 15 (89 rows).

The four WEAKER-THAN-CLAIM rows are the load-bearing follow-ups
for the next Gate G1 session:

* S-002 — gh-desc overstates Buchholz/Veblen + thermodynamic-
  stability closure (10–11/13 rank-mono constructors under WfCNF;
  global `_<ᵇ_` WF still open; thermo bounds only on `Fin n`).
* S-006 — README structural-fact triangle elides the
  pointwise-vs-strict split.
* S-017 — `no-section-collapse` and `no-section-visible` are both
  in `EchoCharacteristic.agda`, not `EchoResidue.agda` as the
  proposed mapping says.
* S-023 — `EchoVsQuotient.Sophisticated.equalizer→echo-pair` and
  `EchoVsGalois.Sophisticated.meet→echo-intersection` (cited by
  `roadmap-gates.adoc:61-62` + `docs/gate-1-distinct-phenomenon.adoc:53-54`
  as the 2-cell certificates for Gate G1) refer to modules that
  do not exist in the codebase; the 2-cell half of the
  distinctness claim is unmechanised.

ID ordering reverted to original insertion order (the sort commit
`4cba187` is effectively undone; the surface-alpha sort is no
longer applied — verification was easier to perform against the
stable original numbering). All 89 IDs retained.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath