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

docs/echo-types/paper.adoc

@@ -554,7 +554,6 @@ mechanised strength, neither less nor more.
 
 === Proof size per pillar
 
-<<<<<<< HEAD
 The four pillars together occupy ~930 lines across six modules, with
 zero postulates and three `rewrite` sites (one in the foundational
 `degrade-compose`; one in its `rel-model` lift; one in
@@ -1134,26 +1133,21 @@ Swamy et al. "Dependent types and multi-monadic effects in F\*"
 (POPL 2016);
 Vazou–Seidel–Jhala–Vytiniotis–Peyton Jones "Refinement types for
 Haskell" (ICFP 2014, Liquid Haskell).
-=======
-NOTE: *[EXPAND]* — detailed positioning against: Granule / QTT graded
-modalities; comonadic notions of computation (Uustalu–Vene);
-coeffects (Petriček–Orchard–Mycroft); HoTT fibrewise constructions;
-lens / optic literature (the witness-transport leg of
-`echo-pullback-univ` resembles the very-well-behaved *1-lens* laws —
-no 2-cell-equipped optic, see below). Make the novelty crisp: not a
-new object, but a fully mechanised characterisation package with a
-falsifiable-gate methodology.
-
-NOTE: *[2-cat ruled out, see `decisions/no-2-cat.adoc`]* — when the
-related-work pass expands the lens/optic comparison and the
-graded-modality positioning, fold in the 2-categorical rule-out: a
-"bicategorical echo" reading was considered and ruled out on the
-landed evidence (every would-be 2-cell appears as `refl` or is
-prop-forced trivial by `≤g-prop` / `⊑-prop`); the construction
-resembles a very-well-behaved *1-lens*, not a 2-cell-equipped optic.
-The closure note in `decisions/no-2-cat.adoc` is the load-bearing
-artifact; this paragraph should cite it rather than re-argue.
->>>>>>> docs/rule-out-2cat-and-roadmap-correction
+
+NOTE: *Related-work `[EXPAND]` cleared 2026-05-26.* The original
+`[EXPAND]` TODO requested detailed positioning against Granule / QTT
+graded modalities, Uustalu–Vene comonads, Petriček–Orchard–Mycroft
+coeffects, HoTT fibrewise constructions, and the lens / optic
+literature with the 1-lens-vs-2-cell-optic clarification. That work
+has been delivered above in §"HoTT homotopy fibres", §"Graded comonads,
+coeffects, and QTT", and §"Lenses and optics (the witness-transport
+leg)" — including the explicit 2-categorical rule-out at the end of
+the lens/optic subsection (`docs/echo-types/decisions/no-2-cat.adoc`
+is the load-bearing closure note). A companion single-page comparator
+table at `docs/echo-types/comparators.adoc` (Echo vs Granule / QTT /
+choreographic / Linear Haskell) ships the axis-by-axis summary form
+for reviewers who want the at-a-glance positioning rather than the
+prose narrative above.
 
 [#reframing-note]
 == Reframing note (2026-05-18)
@@ -1204,44 +1198,6 @@ via a genuine non-graph `StepND` model (§6 NOTE,
 `EchoStepNDModelF2.agda`). The graded-comonad, modality-level
 model-independence, and conservativity rows remain fully retracted.
 
-[#reframing-note]
-== Reframing note (2026-05-18)
-
-This draft was reframed after an adversarial three-reviewer review
-(graded-modality, semantics, and proof-assistant skeptics) found that
-the codebase contains no defense for five central claims, and that
-two were contradicted by the repository's own Gate-2 audit. The
-following claims were retracted, not weakened cosmetically:
-
-[cols="2,3", options="header"]
-|===
-| Retracted claim | Replaced by
-
-| "graded comonad" (counit/comultiplication, three comonad laws)
-| loss-graded *reindexing modality*; no nested `D_r D_s` is formed;
-  the equations hold by thinness of the grade order
-
-| "terminal-cone universal property"; "a category theorist accepts
-  echo as the limit of a cospan"
-| a *pointwise, funext-relative* mediator property; full terminality
-  is unstatable here without funext
-
-| "model independence across two agreeing models"
-| carrier-parametricity over a *fixed* grade poset; the second model
-  is the first with a `⊤` component, agreeing by `refl`
-
-| "conservativity metatheorem, discharged operationally by the build"
-| a *postulate-free build*: evidence for, not a proof of,
-  conservativity over MLTT+Σ
-
-| "funext quarantined behind an isolated module; no result crosses it"
-| no funext anywhere; the real funext-relativity is the pointwise
-  mediator property, now disclosed as the boundary
-|===
-
-The full per-attack analysis and the codebase pressure-test are in
-`docs/retractions.adoc`.
-
 == Conclusion
 
 Echo is the homotopy fibre equipped with a loss-grade lattice,

proofs/agda/Smoke.agda

@@ -378,6 +378,17 @@ open import EchoAbstractionBarrier using
   ; sigma-distinguishes
   )
 
+-- examples.EchoVsSigma — Track C of the Echo-vs-Σ identity claim.
+-- Per-example raw-Σ counter-programs paired with each headline
+-- example (parser, provenance, absint) — the matched-negative
+-- companions for Gate 3. See `roadmap.adoc` §Lane 2 close-out
+-- item 2.
+open import examples.EchoVsSigma using
+  ( parser-sigma-distinguishes
+  ; provenance-sigma-distinguishes
+  ; absint-sigma-distinguishes
+  )
+
 open import EchoGraded using
   ( Grade
   ; degrade

proofs/agda/examples/All.agda

@@ -15,3 +15,4 @@ import examples.TropicalArgmin
 import examples.EpistemicUpdate
 import examples.LinearErasure
 import examples.Transport
+import examples.EchoVsSigma

proofs/agda/examples/EchoVsSigma.agda

@@ -0,0 +1,104 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Track C of the Echo-vs-Σ identity claim consolidation
+-- (`roadmap.adoc` §Lane 2 close-out item 2; companion to
+-- `core/skepticisms/is-this-just-sigma-types.md` §5 and
+-- `docs/echo-types/sigma-distinctness-map.adoc` §"Demand 5").
+--
+-- For each headline example (parser, provenance, absint), exhibit the
+-- small raw-Σ counter-program that the Echo interface refuses to
+-- export at affine mode. Each `*-sigma-distinguishes` is the
+-- *negative companion* to the positive distinct-echoes-same-y theorem
+-- already in the example module: it shows the concrete consumer that
+-- would let the bug through if `proj₁` (or anything that factors
+-- through it) were exposed.
+--
+-- The pattern mirrors `EchoAbstractionBarrier.sigma-distinguishes` at
+-- the per-example level. Together with the affine-side guarantee in
+-- `EchoAbstractionBarrier.affine-consumer-cannot-distinguish`, these
+-- per-example negatives establish the Gate 3 "matched-positive +
+-- matched-negative pair" discipline ("raw Σ would leak; Echo blocks
+-- it") for each headline example.
+--
+-- Scope guardrail: each lemma is a *concrete instance* of the raw-Σ
+-- distinguish pattern at the linear-side echo, exhibiting what an
+-- unprotected Σ-projection would do with the example's distinct
+-- preimages. The corresponding affine-side guarantee that nothing of
+-- this shape can exist is the general `affine-consumer-cannot-distinguish`,
+-- not re-proven here per-example.
+
+module examples.EchoVsSigma where
+
+open import Echo                  using (Echo)
+
+open import EchoExampleParser
+  using ( Token
+        ; parses
+        ; paren-pair; paren-nested
+        ; echo-parse-pair; echo-parse-nested
+        ; paren-nested≢paren-pair
+        )
+open import EchoExampleProvenance
+  using ( Row; project
+        ; echo-prov-true; echo-prov-false
+        ; true≢false
+        )
+open Row using (prov)
+open import EchoExampleAbsInt
+  using ( Sign; Carrier; pos; α
+        ; p1; p2
+        ; echo-pos-p1; echo-pos-p2
+        ; p1≢p2
+        )
+
+open import Data.Bool.Base    using (Bool; true)
+open import Data.List.Base    using (List)
+open import Data.Product.Base using (Σ; _,_; proj₁)
+open import Relation.Binary.PropositionalEquality
+                              using (_≡_; _≢_)
+open import Function.Base     using (_∘_)
+
+----------------------------------------------------------------------
+-- Parser example (`EchoExampleParser`).
+--
+-- `paren-nested` (`((` `)` `)`) and `paren-pair` (`(` `)` `(` `)`)
+-- both have `parses ≡ true`. The Echo retains the distinction
+-- (`echo-parse-nested≢echo-parse-pair`). The raw-Σ counter-program
+-- below uses `proj₁` directly to recover the original `List Token`,
+-- distinguishing the two echoes via the already-proven
+-- `paren-nested≢paren-pair`. The Echo interface at affine mode would
+-- refuse to export `proj₁`; this lemma exhibits exactly what would
+-- leak if it didn't.
+
+parser-sigma-distinguishes :
+  Σ (Echo parses true → List Token)
+    (λ g → g echo-parse-nested ≢ g echo-parse-pair)
+parser-sigma-distinguishes = proj₁ , paren-nested≢paren-pair
+
+----------------------------------------------------------------------
+-- Provenance example (`EchoExampleProvenance`).
+--
+-- `row-with-prov-true` and `row-with-prov-false` project to the same
+-- payload (`project ≡ 0`) but carry distinct provenance Booleans. The
+-- Echo retains the provenance (`echo-prov-true≢echo-prov-false`). The
+-- raw-Σ counter-program composes `prov` with `proj₁` to leak the
+-- provenance Bool, distinguishing the two echoes via `true≢false`.
+
+provenance-sigma-distinguishes :
+  Σ (Echo project 0 → Bool)
+    (λ g → g echo-prov-true ≢ g echo-prov-false)
+provenance-sigma-distinguishes = prov ∘ proj₁ , true≢false
+
+----------------------------------------------------------------------
+-- Abstract-interpretation example (`EchoExampleAbsInt`).
+--
+-- `p1` and `p2` both abstract to `pos` under the 5-element sign
+-- lattice (`α p1 ≡ α p2 ≡ pos`). The Echo retains the concrete
+-- carrier (`echo-pos-p1≢echo-pos-p2`). The raw-Σ counter-program
+-- uses `proj₁` to recover the concrete Carrier, distinguishing via
+-- `p1≢p2`.
+
+absint-sigma-distinguishes :
+  Σ (Echo α pos → Carrier)
+    (λ g → g echo-pos-p1 ≢ g echo-pos-p2)
+absint-sigma-distinguishes = proj₁ , p1≢p2

roadmap.adoc

@@ -161,14 +161,17 @@ gate cross-links) landed in-session. Tracks B + C remain.
 
 *Close-out criterion (falsifiable).* All three hold:
 
-. Track B (consumer-side abstraction barrier) — same artefact named in
-  Lane 1's close-out. (Lane 1 and Lane 2 share this artefact; that is
-  intentional, not duplication.)
-. Track C (per-example raw-Σ counter-programs) lands as
-  `proofs/agda/examples/EchoVsSigma.agda`, pairing each headline
-  example with the small Σ-misuse it blocks. Pinned in Smoke.
+. *LANDED 2026-05-26.* Track B (consumer-side abstraction barrier) —
+  same artefact named in Lane 1's close-out. (Lane 1 and Lane 2 share
+  this artefact; that is intentional, not duplication.)
+. *LANDED 2026-05-26.* Track C (per-example raw-Σ counter-programs)
+  shipped as `proofs/agda/examples/EchoVsSigma.agda`, pairing each
+  headline example (parser, provenance, abs-int) with the small
+  Σ-misuse it blocks. Builds clean under `--safe --without-K`;
+  pinned in `Smoke.agda` under own `using` block.
 . The Gate 2 nominee list is re-audited and crosses the *comfortable*
   threshold (≥ 3 of 4 surviving), not merely the honest minimum.
+  *(Remaining open item for Lane 2 close-out.)*
 
 *Artefacts (landed today).* `core/skepticisms/is-this-just-sigma-types.md`
 (canonical answer doc, 5-section structure mirroring the demands);