Pillar E / examples.md: ephapax L3 region-exit as canonical example (draft entry + paper paragraph)

[hyperpolymath]

What this is

A draft contribution for the Pillar E paper's canonical-examples section, and (upstream of that) an entry for `docs/echo-types/examples.md` following its existing template. Filed as a draft for owner review — does not assume the framing or wording you want, just offers concrete prose so review is cheap.

Echo-types' `tutorial/region_exit_audit/RegionExitAudit.agda` already models ephapax-L3-style regions as `Mode`-indexed `LEcho`. Today's ephapax work hardened the case that this is a machine-checked external corroboration, not just a tutorial reference. Specifically:

• ephapax `formal/Echo.v` (PR proof(Slice 3+4 Route A): (c) trichotomy + consumer-side first-eq derivation #166, proof(Path-3 prototype): same-left joint-bplus rank-mono extension #167) is an explicit Coq port of `EchoLinear.agda` + `EchoResidue.agda`.
• `no_section_collapse_to_residue` lands as `Qed` in ephapax with zero axioms — the same theorem as echo-types' headline irreversibility result.
• ephapax's L1+L2+L3+L4 stack composes via thin-poset decorations across four distinct conceptual layers (region capability / linearity-affinity / echo residue / dyadic mode), all sharing the same underlying judgment shape — exactly the `decoration-commuting` discipline echo-types proposes.

Draft entry for `docs/echo-types/examples.md`

Following the existing template (source map / what is lost / what remains / echo / extensional-intensional / reference). Suggested insertion point: after the existing entries, as the first external-system example (i.e. the first canonical example whose source map comes from a different formalisation):

---

N. Region exit in a linear type system (ephapax L3)

• Source map. `collapse_r : LiveAt r → ExitedAt r`, the
  operational `S_Region_Exit` rule of the ephapax calculus: a region
  scope `ERegion r e` reducing on a value `v` produces
  `(mem_free_region μ r, remove_first r R, v)`. The map sends a
  configuration with `r ∈ R` to one with `r ∉ R`, freeing the
  region's memory.
• What is lost. Which linear values (of type `TString r`,
  `TRef Lin (TString r)`, …) were live in `r` immediately before
  exit. After the step, `r` is unrecoverable as a region name,
  and the typing system cannot reconstruct which preimage configuration
  produced the post-step state.
• What remains. A proof-relevant residue: the residue value typed
  at `TEcho` (in ephapax's L3 layer) carries a witness of which
  value-shape was erased. Under Linear mode the residue must be
  observed (`T_Observe` consumes it); under Affine mode the residue
  may be silently lowered to the trivial residue `EchoR ⊤ TrivCert y`.
• Echo. `Echo collapse_r exited = Σ (LiveAt r) (λ s → collapse_r s ≡ exited)`.
  Under Linear mode the full fiber is retained; under Affine mode
  the codomain is collapsed to ⊤ and the inhabitants become
  propositionally equal (cf. `affine_canonical` /
  `affine_all_equal` in `Echo.agda`).
• Extensional / intensional. Intensional. The shadow
  (`{R-after-exit : list region_name}`) lets the typing system see
  the post-exit capability set, but the intensional core
  distinguishes which configuration produced it.
• Reference. ephapax `formal/Echo.v` (Coq port of
  `EchoLinear.agda`), `no_section_collapse_to_residue` (`Qed`,
  zero axioms); ephapax `formal/PRESERVATION-DESIGN.md` §6
  (L3 design); ephapax `tutorial/region_exit_audit/RegionExitAudit.agda`
  (echo-types side).

---

Draft paragraph for Pillar E paper (canonical-examples section)

A more compact form suitable for a paper's canonical-examples
discussion. Tone aligned to the R-2026-05-18 narrowed claim
(definitional Σ-identity + funext-relative + thin-poset reindexing +
separating model + carrier-parametric + `--safe --without-K`,
postulate-free).

A machine-checked external corroboration of the fiber + thin-poset
formulation comes from the ephapax programming-language project, an
independent calculus whose four-layer redesign (region capability /
linearity-affinity / echo residue / dyadic mode) was authored against
a Coq mechanisation rather than against echo-types directly. When that
redesign reached the irreversibility-residue layer, the natural
structure that emerged was the same fiber-plus-thin-poset shape
already mechanised in echo-types: ephapax's `formal/Echo.v` is a
direct Coq port of `EchoLinear.agda` and `EchoResidue.agda`,
and ephapax's headline `no_section_collapse_to_residue` lands as
`Qed` with zero axioms, mirroring the same-name theorem in
`EchoResidue.agda:33–73`. The convergence is evidence that the
formulation supports the third identity-claim criterion — canonical
examples where echo type is the right explanatory unit, not a
generic Σ-type — under cross-language reproducibility, with both
Linear and Affine modes manifesting as the same thin-poset
decoration over a shared fiber type former rather than as separate
echo type formers.

What this does NOT claim

• That ephapax's L3 is more advanced than echo-types (the reverse:
  ephapax ports from echo-types).
• That this single example settles the identity claim (it strengthens
  criterion 3, doesn't decide it).
• That the example should replace existing examples — it sits alongside
  the sign-loss / boolean-component / parser entries as a real-world
  external case.

What I am NOT proposing

• Modifying `paper.adoc` or `types-abstract.adoc` directly. The
  Pillar E narrative is the author's; this is just draft text.
• Implementing the `EchoEphapaxBridge.agda` module (filed separately
  as Lane-4 bridge candidate: EchoEphapaxBridge.agda (content bridge to hyperpolymath/ephapax L3) #126).

References

• ephapax `formal/Echo.v` (PR proof(Slice 3+4 Route A): (c) trichotomy + consumer-side first-eq derivation #166, proof(Path-3 prototype): same-left joint-bplus rank-mono extension #167)
• ephapax `formal/PRESERVATION-DESIGN.md` §6
• ephapax `formal/Counterexample.v` — three Qed lemmas for the
  preservation counterexample (the structural-loss source for L3's
  residue).
• echo-types `tutorial/region_exit_audit/RegionExitAudit.agda`
• echo-types `docs/echo-types/examples.md` (template followed)
• Related: composition.md: empirical evidence for decoration-violating closure being unsound (ephapax L1→L2 case) #125 (composition.md content), Lane-4 bridge candidate: EchoEphapaxBridge.agda (content bridge to hyperpolymath/ephapax L3) #126 (bridge proposal)

🤖 Generated with Claude Code

[hyperpolymath]

Now tracked under parent #128.