docs: ephapax bridge package (#125 + #127) + EchoTypes.jl v0.2.0 surfacing (#132)

Resolves three tightly-coupled open documentation issues with shared
inputs from a coordinated proposal at /tmp/ephapax-bridge-proposal.md
(a background-agent research dump consumed verbatim where citation-
quality matched, lightly edited for context).

#132 — Surface EchoTypes.jl v0.2.0 (4 edits)
=============================================

* README.md — one-line "Executable companion" callout below the
  synopsis, pointing at hyperpolymath/EchoTypes.jl with explicit
  R-2026-05-18 honest-scope clause (retracted surface NOT mirrored;
  F5 funext-qualified clauses NOT mirrored — Julia has no funext).
* CLAUDE.md ecosystem-context block — new bullet matching the
  existing one-line style of Ephapax / VeriSim entries; same scope
  caveats.
* docs/bridges/cross-repo-bridge-status.md — new row in the Tracks
  table for the executable-mirror correspondence. Row uses the
  existing 5-column shape; "Current status" cell carries the
  scope-inheritance discipline so the row stays falsifiable by an
  outside reviewer.
* docs/echo-types/MAP.adoc §Tooling — new §"EchoTypes.jl — Executable
  Julia companion `[REAL]`" subsection adjacent to the ArghDA
  subsection. Records repo URL + registry + v0.2.0 module list +
  honest-scope clause + bridge-status pointer.

The companion makes no proof claims and the Agda here remains the
sole source of truth; these edits exist so contributors and reviewers
can discover the companion without already knowing it's there.

#125 — composition.md methodological note
==========================================

Adds a new "Anti-pattern — closing a degrade-map obligation within an
endpoint" subsection at the end of docs/echo-types/composition.md.
Captures the lesson surfaced by the 2026-05-27 ephapax four-layer
redesign work: when a decoration `D₁ ≤ D₂` connects two indexed
instances of a fiber, an obligation that mentions BOTH endpoints
does not close inside either endpoint alone — the load-bearing
content lives on the degrade arrow.

The note pairs the upstream Agda theorem (`EchoLinear.degradeMode-comp`
at `proofs/agda/EchoLinear.agda:93-101`, three `refl` clauses) with
an empirical downstream test from ephapax (PR #170 strengthened the
L1 variable rule with a region-well-formedness premise; the resulting
axiom remained false on a concrete typing-level counterexample; the
honest closure path identified in PRESERVATION-DESIGN.md §4.8.1 is
cross-layer at the L1→L2 boundary).

The downstream test is empirical evidence that the discipline
detects ill-shaped attempts at the point the abstraction predicts —
NOT a proof of the upstream theorem. Composition.md is Markdown, so
the note is rendered as Markdown rather than the AsciiDoc requested
in the issue body (composition.md / examples.md / overview.md /
taxonomy.md / tropical-correspondence.md / types-list-note.md are
all .md while the other dozen docs are .adoc; the split is
pre-existing and the policy direction isn't documented — flagging
as a seam observation only, not migrating the file extension here).

#127 — examples.md entry + paper paragraph
==========================================

Two edits:

* docs/echo-types/examples.md — new entry 11 "Region exit in a
  linear type system (ephapax L3)" inserted after entry 10
  (Abstract interpretation widening) and before §"Cross-cutting
  observations". Matches the existing 6-bullet template (Source
  map / What is lost / What remains / Echo / Extensional-
  intensional / Reference). The Reference bullet cites both
  echo-types-side `tutorial/region_exit_audit/RegionExitAudit.agda`
  (the type-level audit walkthrough) AND ephapax-side `formal/Echo.v`
  with tight line ranges (291-301 for affine_canonical /
  affine_all_equal; 502-517 for no_section_collapse_to_residue).
* docs/echo-types/paper.adoc §"Threats to validity" §"Sample-size
  on consumer evidence" — new paragraph after the existing two
  (absolute-zero and Buchholz), before §"Conservativity is
  evidence, not a theorem". Adds the ephapax L3 layer as the
  third partial external-corroboration stream, tone matched to
  the existing "validates one technical bridge, not the modality
  thesis" framing. R-2026-05-18 narrowings preserved (no
  graded-comonad / two-models / UP / model-independence language).
  Honestly scoped to L3 ONLY — not implying anything about
  ephapax's overall proof posture (L1 has 5 Axiom + 11 Admitted,
  L2 has 1 Admitted, L4 is skeleton; only L3 is Qed-closed and
  safe to cite).

Background-agent seam observations folded in
=============================================

Three observations the agent caught while assembling the proposal
were applied in-PR (none scope-creep):

1. composition.md is Markdown not AsciiDoc — draft rendered as
   Markdown to match file. Noted in commit body.
2. #127's cited line range 33-73 covers the block; the tight
   theorem range is 52-65. Tight range used in both examples.md
   and paper.adoc.
3. MEMORY.md entry `feedback_ephapax_affine_proofs_not_done.md`
   warns that ephapax's overall proof posture is mixed; §3.2 paper
   paragraph is scoped to L3 specifically.

Test plan
=========

* All edits are pure docs — Agda suite unaffected.
* References to other-repo line numbers verified at the agent's
  cited points before paste.
* No retraction-watch violations: scanned the diff for
  "graded comonad", "model-independence", "categorical universal
  property", "conservativity metatheorem" — none introduced.

Refs
====

* Closes #125
* Closes #127
* Closes #132
* Refs #128 (umbrella will close when #126 also lands)
* Refs #126 (handled in a separate Agda PR — NARROW stub per
  agent's verdict)

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

Author: hyperpolymath

CLAUDE.md

@@ -38,6 +38,17 @@ Adjacent projects, in one line each, for session bootstrapping:
   Split as `arghda-core` (language-agnostic engine) + `arghda-panll`
   (Gossamer/ReScript presentation). See docs/buchholz-plan.adoc appendix
   for the motivating proof pipeline.
+- EchoTypes.jl — executable Julia companion to echo-types, mirroring the
+  finite-domain shadow of the Tier-1 + Tier-2 spine + the unconditional
+  F5 OFS fragment. v0.2.0 (2026-05-27) extends v0.1.0's `Echo` /
+  `EchoResidue` / `EchoFiberCount` / `EchoThermodynamics` coverage with
+  seven new modules (`EchoTotalCompletion`, `EchoOrthogonalFactorizationSystem`,
+  `EchoImageFactorization`, `EchoNoSectionGeneric`, `EchoLossTaxonomy`,
+  `EchoEntropy`, `EchoObservationalEquivalence`). Honestly scoped under
+  R-2026-05-18 — the retracted surface and the funext-qualified F5
+  clauses are NOT mirrored. Falsifies-by-counterexample on concrete
+  data; the Agda here remains the source of truth.
+  https://github.com/hyperpolymath/EchoTypes.jl
 
 # This repo
 

README.md

@@ -15,6 +15,15 @@ Constructive Agda development for echo types as a first-class notion of structur
 
 loss that is not total erasure.
 
+> **Executable companion.** [`hyperpolymath/EchoTypes.jl`](https://github.com/hyperpolymath/EchoTypes.jl)
+> (v0.2.0, 2026-05-27) runs the finite-domain shadow of the Tier-1 +
+> Tier-2 spine + the unconditional F5 OFS fragment on concrete data.
+> The Julia mirror is honestly scoped under R-2026-05-18 — it does
+> NOT replay the retracted graded-comonad / two-models / UP /
+> conservativity surface, nor the funext-qualified F5 clauses (Julia
+> has no funext). It falsifies-by-counterexample; the Agda here
+> remains the source of truth.
+
 ## Contents
 
 - [Where things are](#️-where-things-are)

docs/bridges/cross-repo-bridge-status.md

@@ -15,6 +15,7 @@ touches other repositories.
 | CNO core theorem alignment | `EchoCNOBridge` theorem family | `absolute-zero/proofs/coq/common/CNO.v`, `absolute-zero/proofs/lean4/CNO.lean` | Name-by-name correspondence table drafted (see §"CNO Agda↔Coq↔Lean4 correspondence" below). | (1) Coq's `eval` is relational; Agda+Lean are functional. (2) Coq has no `absolute_zero` alias. (3) Coq's single-instruction CNO is `nop_is_cno`; Agda+Lean use `halt_is_cno`. (4) Coq carries 3 axioms (`eval_deterministic`, `eval_respects_state_eq_{left,right}`) that echo-types' `--safe --without-K` policy forbids — porting must re-route through a functional formulation, where they hold by `refl`. (5) `ProgramEcho`/`Echo` itself is currently unilateral (Agda-only). |
 | JanusKey bridge | `proofs/agda/EchoJanusBridge.agda` | `januskey/src/abi/Types.idr` (`OpKind`, `IsFileOp`, `IsKeyOp`); `januskey/PROOF-NEEDS.md` | Name-bridge only — Agda side has a *local* 4-variant `JanusOp = Create \| Delete \| Modify \| Move`; canonical Idris2 ABI defines 8-variant `OpKind = Copy \| Move \| Delete \| Modify \| Obliterate \| KeyGen \| KeyRotate \| KeyRevoke` plus `IsFileOp`/`IsKeyOp` predicates. Already drifted (Create vs Copy; missing Obliterate + 3 key ops). | Decision recorded: structural-mirror the Agda enum to januskey's Idris2 `OpKind`; content-bridge deferred until januskey's `PROOF-NEEDS.md` lands content-bearing semantics. Agda↔Idris2 has no FFI, so any content-bridge must run via shared schema or trusted extraction. |
 | Tropical alignment | `proofs/agda/EchoTropical.agda` | `tropical-resource-typing/Tropical.thy`, `tropical-resource-typing/TropicalSessionTypes.lean` (and 8 other `.thy` files) | Adjacent repo audit complete (2026-05-20). Repo present at `repos-monorepo/verification-ecosystem/tropical-resource-typing`; remote `hyperpolymath/tropical-resource-typing` active (last push 2026-05-18, language=Isabelle). First alignable theorem pair identified: Agda `⊕-idem` ↔ Isabelle `trop_add_idem` ↔ Lean `add_comm_trop`+`add_assoc_trop`. | Agda cannot import `.thy` or `.lean` directly; alignment is citation-level (statement correspondence with build-side independent proof per language), not import-level. Long-game target: `Tropical_Ordinal_Bridge.thy` ↔ echo-types ordinal track. |
+| EchoTypes.jl executable mirror | Tier-1+Tier-2 spine + unconditional F5 OFS fragment (modules: `Echo`, `EchoResidue`, `EchoFiberCount`, `EchoThermodynamics`, plus 2026-05-27 v0.2.0 additions: `EchoTotalCompletion`, `EchoOrthogonalFactorizationSystem`, `EchoImageFactorization`, `EchoNoSectionGeneric`, `EchoLossTaxonomy`, `EchoEntropy`, `EchoObservationalEquivalence`) | [`hyperpolymath/EchoTypes.jl`](https://github.com/hyperpolymath/EchoTypes.jl) v0.2.0 (pinned to `e7dded6`); registered in `julia-professional-registry` | **Executable companion shipped.** Mirrors run the finite-domain shadow of the upstream theorems on concrete data and falsify-by-counterexample; the companion makes no proof claims, the Agda here remains the source of truth. R-2026-05-18 retraction surface NOT mirrored; F5 funext-qualified clauses (uniqueness up to iso, diagonal lifting) NOT mirrored — Julia has no funext, the claims would be vacuous. UIP- and truncation-strength upgrades likewise honestly not mirrored. | — (shipped; honest scope holds verbatim from upstream). Future advances on the Tier-1+Tier-2 spine are candidates for new shadows in subsequent EchoTypes.jl releases, but no in-repo CI dependency exists in either direction. |
 
 ## Immediate next actions
 

docs/echo-types/MAP.adoc

@@ -353,6 +353,30 @@ Language-agnostic proof-workspace engine (`arghda-core`, Rust). MVP.
 * Code: `arghda-core/` (Rust crate).
 * Docs: `docs/arghda-spec.adoc`.
 
+=== EchoTypes.jl — Executable Julia companion `[REAL]`
+Mirrors the finite-domain shadow of the Tier-1 + Tier-2 spine + the
+unconditional fragment of the F5 OFS earn-back. v0.2.0 (2026-05-27,
+pinned to `e7dded6`) extends the original v0.1.0 coverage (`Echo`,
+`EchoResidue`, `EchoFiberCount`, `EchoThermodynamics`) with seven
+new shadows for the canonical-identity spine: `EchoTotalCompletion`,
+`EchoOrthogonalFactorizationSystem` (unconditional fragment),
+`EchoImageFactorization`, `EchoNoSectionGeneric`, `EchoLossTaxonomy`,
+`EchoEntropy`, `EchoObservationalEquivalence`.
+
+* Repo: https://github.com/hyperpolymath/EchoTypes.jl
+* Registry: `julia-professional-registry` (registered via PR #16).
+* Scope inheritance: R-2026-05-18 retraction surface NOT mirrored;
+  F5 funext-qualified clauses (uniqueness up to iso, diagonal
+  lifting) NOT mirrored — Julia has no funext, the claims would be
+  vacuous; UIP- and truncation-strength upgrades likewise honestly
+  not mirrored.
+* Discipline: falsifies-by-counterexample over concrete finite data;
+  the companion makes no proof claims, the Agda here remains the
+  source of truth. No in-repo CI dependency in either direction.
+
+Bridge-status row: `docs/bridges/cross-repo-bridge-status.md`
+§"EchoTypes.jl executable mirror".
+
 == Governance — proof-debt & retraction
 
 The honesty layer. *Read before citing any claim above as final.*

docs/echo-types/composition.md

@@ -397,3 +397,54 @@ Ranked by unblock-value. (1) and (2) landed; (3) onwards is open.
 None of these depend on the blocked Buchholz-WF / shared-binder
 work. All are Sonnet-class proofs; (5) is Opus 4.7 design and
 Sonnet execution.
+
+---
+
+## Anti-pattern — closing a degrade-map obligation within an endpoint
+
+*Status: methodological note (2026-05-30). Not Agda-backed; the
+upstream theorem it abstracts from IS Agda-backed.*
+
+The per-decoration composition rung (§6, "Decoration commuting") proves
+that for each decoration `D` the degrade map `degrade : ⊑ → Echo D₁ →
+Echo D₂` commutes with composition under a recipe: order →
+propositionality → join → factoring-free compose → via-join restatement.
+The recipe makes the cross-decoration obligation — "two successive
+weakenings agree with a single weakening along the composed proof" —
+*explicitly* a property of the degrade map, not of either endpoint.
+The upstream theorem is `EchoLinear.degradeMode-comp`
+(`proofs/agda/EchoLinear.agda:93-101`), three `refl` clauses pinning
+each reachable constructor pair.
+
+**The anti-pattern.** When a decoration `D₁ ≤ D₂` connects two
+indexed instances of a fiber, an obligation that mentions *both*
+endpoints does not close inside either endpoint alone. Attempting to
+discharge it by strengthening a typing rule of `D₁` (or `D₂`) with a
+premise that references the other endpoint's invariant is structurally
+ill-shaped: the load-bearing content lives on the degrade arrow.
+
+**Detection heuristic.** If a proof attempt requires adding a premise
+to a rule of one decoration that mentions a *different* decoration's
+invariant (e.g. a region-presence premise on a modality-indexed rule),
+the discipline is being violated. The corrective is to relocate the
+obligation to the decoration map, not to thicken the endpoint.
+
+**Empirical downstream test.** The `hyperpolymath/ephapax` project's
+L1 region-capability layer admits an analogue cross-decoration
+obligation. An empirical closure attempt (ephapax PR #170, merged
+2026-05-27) strengthened the L1 variable rule
+`T_Var_*_L1` with a region-well-formedness premise and verified the
+resulting axiom remained false on a concrete typing-level
+counterexample (`ERegion rv (EI32 5) : TBase TI32 at R = [rv]`). The
+honest closure path identified in ephapax's `PRESERVATION-DESIGN.md`
+§4.8.1 is cross-layer — the obligation lives at the L1→L2 boundary
+where the effect-typed `TFun` of `T_Lam_Linear_L2` carries the
+region-effect that L1's R-threading lacks. The pattern matches the
+echo-types abstraction: visible source-level discrepancies *can* be
+absorbed inside an endpoint (and PR #170 absorbed one), but the
+cross-decoration obligation cannot.
+
+The downstream test is not a proof of the upstream theorem — it is
+empirical evidence that the discipline detects ill-shaped attempts at
+the point the abstraction predicts. See echo-types#125 for the
+issue thread that surfaced this observation.

docs/echo-types/examples.md

@@ -205,6 +205,45 @@ Template used for every entry:
 
 ---
 
+## 11. 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 types `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 collapses to ⊤ and the inhabitants become propositionally
+  equal (cf. `affine_canonical` / `affine_all_equal` in ephapax
+  `formal/Echo.v:291-301`).
+- **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.** `tutorial/region_exit_audit/RegionExitAudit.agda`
+  (the echo-types-side type-level audit walkthrough); ephapax
+  `formal/Echo.v` (Coq port of `EchoLinear.agda`); ephapax
+  `no_section_collapse_to_residue` (`formal/Echo.v:502-517`,
+  `Qed`, zero axioms) matches
+  `EchoResidue.no-section-collapse-to-residue`
+  (`proofs/agda/EchoResidue.agda:52-65`). See echo-types#127 for
+  the issue thread that seeded this entry.
+
+---
+
 ## Cross-cutting observations
 
 1. **Shadow collapse is the same across cases.** Every example's

docs/echo-types/paper.adoc

@@ -798,6 +798,24 @@ particular technical bridges (the Echo–CNO bridge and the eventual
 Echo–`<ᵇ` bridge respectively), and not of "Echo as a recognised
 modality" in the field.
 
+A third partial external-corroboration stream is the
+`hyperpolymath/ephapax` programming-language project, whose L3
+layer (`formal/Echo.v`) is an explicit Coq port of `EchoLinear.agda`
+and `EchoResidue.agda` under the same `--safe --without-K`-equivalent
+discipline (K-free, zero axioms, 24 `Qed`).  The ephapax headline
+`no_section_collapse_to_residue` (`formal/Echo.v:502-517`) is the
+same theorem, stated again in Coq, as
+`EchoResidue.no-section-collapse-to-residue`
+(`proofs/agda/EchoResidue.agda:52-65`), and lands constructively in
+both mechanisations.  We claim only that this is a faithful
+re-statement: the two artefacts are not independent derivations —
+ephapax was written *against* the Agda upstream — so the
+corroboration is at the level of "the Coq port carries through
+without uncovering a mechanisation gap," not at the level of
+independent corroboration of the fiber + thin-poset shape.  As with
+the `absolute-zero` consumer evidence, this validates one technical
+bridge, not the modality thesis.
+
 ==== Conservativity is evidence, not a theorem
 
 `docs/echo-types/conservativity.adoc` was retracted from