docs(gate-1): refresh adjacency notes with composition-iso evidence (#22)

## Summary

Refresh the six Gate 1 adjacency notes (`docs/adjacency/*.adoc`) to
discharge the Gate 1 test against current code:

- Cite the composition-track theorems that landed since the original
drafts: `Echo-comp-iso-{to, from, from-to, to-from}`, `cancel-iso-{to,
from}`, projection-pentagon `Echo-comp-iso-pent-{B, echo}` in
`proofs/agda/Echo.agda`. These are content distinguishing echo types
from refinement, lens/optic, HoTT-fiber, setoid-quotient,
provenance-semiring, and cubical neighbours — and none of the existing
notes cited them.
- Normalise `cubical-systems.adoc` to the canonical 5-section template
the other notes use (1. Nearest construction, 2. What do echo types add,
3. What do they not add, 4. Honest risk, 5. Verdict for Gate 1) so all
six notes discharge the test in the same shape.
- Add a "Compositional evidence (load-bearing across notes)" section to
the README pointing at the iso family and cancellation, since these are
now cited from multiple notes.

## Verdicts

Unchanged. `refinement-types`, `lenses-and-optics`, `setoid-quotients`,
`provenance-semirings`, `cubical-systems` all survive Gate 1;
`hott-fibers` remains a marginal pass dependent on Gate 2 / Gate 3
outcomes. The refresh strengthens the supporting evidence rather than
reopening the verdicts.

## Scope

Docs only. All cited theorems verified present in `proofs/agda/` on main
(20/20). Fully independent of any Agda edits.

## Test plan

- [x] All cited theorems by module and name resolve in `proofs/agda/` on
main
- [x] Diff against main is doc-only (`docs/adjacency/*.adoc`)
- [x] No postulates / no Agda changes / no new `--without-K` violations
to consider

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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

Author: hyperpolymath