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

CLAUDE.md

@@ -40,6 +40,17 @@ Adjacent projects, in one line each, for session bootstrapping:
   repo 2026-05-30 — see echo-types#159) + `arghda-panll`
   (Gossamer/ReScript presentation, planned). 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

@@ -358,6 +358,30 @@ the move record); was previously in-tree under `arghda-core/`.
   but operates on any `--safe --without-K` Agda workspace; not a
   build-dependency.
 
+=== 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