fix+feat: paper.adoc conflict resolution + related-work [EXPAND] cleared + Track C land

[hyperpolymath]

Summary

Stacked on #118. Closes the three remaining session items from the user-prioritised batch:

1. 🔴 P0 — paper.adoc merge-conflict resolution
2. Lane 1 close-out item 1 — paper.adoc [EXPAND] tag 2 (related-work pass) cleared
3. Lane 2 close-out item 2 — Track C (per-example raw-Σ counter-programs) landed

1. P0 conflict resolution

Three unresolved git conflict markers at paper.adoc:557,1137,1156 from merge commit cab99f1 (reframe/retraction-2026-05-18). Resolution:

• HEAD chunk (579 lines, lines 558-1136): substantive proof-size + threats-to-validity + related-work analysis. Kept verbatim.
• Incoming chunk (17 lines, lines 1138-1155): [EXPAND] note + 2-cat ruleout note. Kept verbatim.
• Conflict markers stripped, no content lost.
• Duplicate == Reframing note (2026-05-18) at lines 1207-1243 deleted; single canonical copy at lines 1158-1194 retained.

Net: paper.adoc 1278 → 1238 lines. Now well-formed AsciiDoc on main.

2. Related-work [EXPAND] tag 2 cleared

Discovered both stale TODO notes (related-work expansion + 2-cat ruleout fold-in) had their content silently delivered in substantive subsections of == Related work:

• === HoTT homotopy fibres
• === Graded comonads, coeffects, and QTT (the lineage we are motivated by, but explicitly not an instance of)
• === Lenses and optics (the witness-transport leg) — already contains the 2-categorical rule-out at lines 948-953

Replaced both stale notes with a single explanatory NOTE pointing at the delivered subsections + docs/echo-types/comparators.adoc companion. Lane 1 close-out: only the ordinal-appendix [EXPAND] (tag 4) remains, correctly gated on the Bachmann-Howard milestone per design.

3. Track C — proofs/agda/examples/EchoVsSigma.agda

Three lemmas pairing each headline example with the small raw-Σ counter-program the Echo interface refuses to export at affine mode:

Lemma	Distinguishes
parser-sigma-distinguishes	echo-parse-nested vs echo-parse-pair at parses ≡ true (via proj₁ + paren-nested≢paren-pair)
provenance-sigma-distinguishes	echo-prov-true vs echo-prov-false at project ≡ 0 (via prov ∘ proj₁ + true≢false)
absint-sigma-distinguishes	echo-pos-p1 vs echo-pos-p2 at α ≡ pos (via proj₁ + p1≢p2)

Mirrors EchoAbstractionBarrier.sigma-distinguishes at the per-example level. Together with EchoAbstractionBarrier.affine-consumer-cannot-distinguish, establishes the Gate 3 matched-positive + matched-negative pair discipline ("raw Σ would leak; Echo blocks it").

Build verification: agda proofs/agda/All.agda, proofs/agda/Smoke.agda, proofs/agda/examples/All.agda all exit 0 under --safe --without-K, zero postulates. Wired into examples/All.agda; pinned in Smoke.agda under own using block.

Roadmap updates

• Lane 1: item 1 (related-work) now LANDED; only ordinal-appendix EXPAND tag remains (correctly out-of-scope).
• Lane 2: item 2 (Track C) now LANDED. Only item 3 (Gate-2 nominee re-audit ≥3/4 surviving) remains for full Lane 2 close-out.

Retraction discipline (R-2026-05-18) respected throughout

No new prose introduces graded-comonad, full-universal-property, model-independence, or general-parametricity claims.

Test plan

• agda proofs/agda/All.agda exits 0 under --safe --without-K
• agda proofs/agda/Smoke.agda exits 0 (new Track C pins verified)
• agda proofs/agda/examples/All.agda exits 0 (new EchoVsSigma wired)
• agda proofs/agda/examples/EchoVsSigma.agda typechecks in isolation
• Zero conflict markers remain in paper.adoc (grep -nE '^<<<<<<<|^=======|^>>>>>>>')
• Single == Reframing note section (no duplicate)
• AsciiDoc rendering of paper.adoc + roadmap.adoc is well-formed

Net diffstat: +140 / -65 across 5 files.

🤖 Generated with Claude Code