docs: record Valence Shell / Ochránce as exploratory downstream consumer (#177)

## Summary

Conservative, **docs-only** entry recording Valence Shell / Ochránce as
a *possible downstream consumer* of Echo Types' structured-loss
semantics. The bridge is exploratory and has **Core Affect: NO**.

The framing: Echo Types' existing vocabulary for structured loss
(recoverable / constrained / residue-bearing / observationally
equivalent / genuinely lost) is a *candidate* classifier for shell and
filesystem state transitions; Ochránce may supply concrete receipt
evidence. This is downstream application evidence, not a new foundation,
and not a mechanised cross-repo theorem.

## Changes

- `docs/bridge-status.md` — new **§7** (Status / Dependencies / Blockers
/ Core Affect), matching the existing ledger format and the repo's "Core
Affect: NO" vocabulary.
- `docs/bridges/cross-repo-bridge-status.md` — new Tracks-table row +
revision-history entry + "Last updated" date bump.
- `docs/echo-types/explorations/accountable-shell/README.adoc` — short
exploratory note mirroring the existing `decoration-bridge/` precedent
(CAUTION banner, candidate-classification reading-aid table over
*existing* modules, explicit non-claims, termination criteria).

## Constraints honoured

- **No Agda touched.** Nothing under `proofs/` is changed; the verified
suite is unaffected by construction. Nothing is wired into `All.agda`,
`Smoke.agda`, or `EchoCanonicalIdentitySuite.agda`.
- **No postulates.**
- The identity claim, canonical identity layer, F5 / OFS
universal-property story, and establishment framing are untouched.
- Makes **no** claim about Valence Shell / Ochránce implementation
correctness, POSIX, Rust, the Lean→Rust correspondence, secure deletion,
GDPR, cryptographic integrity, or Ochránce attestation.
- Valence Shell's RMR / RMO terms appear only as clearly-marked
*downstream application vocabulary*; they are not adopted into the Echo
Types core.
- Cited modules (`EchoTotalCompletion`, `EchoLossTaxonomy`,
`EchoGraded`, `EchoResidue`, `EchoResidueTaxonomy`,
`EchoObservationalEquivalence`, `EchoNoSectionGeneric`) were verified to
exist before referencing.

https://claude.ai/code/session_01Jxr3Wy4ngpkbc2QwjEam82

---
_Generated by [Claude
Code](https://claude.ai/code/session_01Jxr3Wy4ngpkbc2QwjEam82)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

docs/bridge-status.md

@@ -41,3 +41,9 @@ This document strictly tracks the status of experimental extensions and bridges
 - **Dependencies:** `EchoIntegration`, `EchoChoreo`, `EchoGraded` (import only)
 - **Blockers:** Bridge is bounded by construction. Closes under any of the documented termination criteria: Track A/B/C failure, all candidate analogies retired, redundancy with retracted-prose graded-comonad framing, forbidden-rebrandings register addition, retraction-watch trip. Companion: `docs/echo-types/explorations/decoration-bridge/README.adoc`; module: `proofs/agda/EchoDecorationBridge.agda` (deliberately not in `All.agda`).
 - **Core Affect:** NO
+
+## 7. Valence Shell / Ochránce accountable-shell bridge (candidate downstream consumer)
+- **Status:** EXPLORATORY (candidate downstream consumer; no Agda artefact, no cross-repo theorem)
+- **Dependencies:** None in this repo. Adjacent (downstream) only: Valence Shell (`hyperpolymath/valence-shell` — shell state transitions, undo/redo, checkpoints, diff/replay); Ochránce (`hyperpolymath/ochrance` — A2ML manifests, Merkle state commitments, repair/attestation surfaces).
+- **Blockers:** No shared schema and no mechanised cross-repo theorem exist. The relationship is citation-level only: Echo Types' structured-loss vocabulary (recoverable / constrained / residue-bearing / observationally equivalent / genuinely lost) is a *candidate* classifier for shell state transitions, and Ochránce may supply concrete receipt evidence. This is downstream application evidence, not a new foundation. Echo Types makes **no** claim about Valence Shell or Ochránce implementation correctness, and **no** claim about POSIX, Rust, the Lean→Rust correspondence, secure deletion, GDPR, cryptographic integrity, or attestation. Companion note: `docs/echo-types/explorations/accountable-shell/README.adoc`. Nothing for this bridge is imported into `proofs/agda/All.agda`, `proofs/agda/Smoke.agda`, or `proofs/agda/EchoCanonicalIdentitySuite.agda`.
+- **Core Affect:** NO

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

@@ -2,7 +2,7 @@
 <!-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 # Cross-Repo Bridge Status
 
-Last updated: 2026-05-20.
+Last updated: 2026-06-02.
 
 This file is the single status ledger for echo-type bridge work that
 touches other repositories.
@@ -17,6 +17,7 @@ touches other repositories.
 | 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. |
 | Ephapax L3 bridge (Agda↔Coq) | `proofs/agda/EchoEphapaxBridge.agda` | `ephapax/formal/Echo.v` (Coq, 584 lines, 24 `Qed`, zero `Admitted` / zero `Axiom`) — explicit port of `EchoLinear.agda` + `EchoResidue.agda` under a K-free / zero-axiom discipline equivalent to `--safe --without-K` | **Navigability bridge done; content bridge NARROW** (2026-05-30). Two definitional `refl`-renames: `ephapax-L3-weaken = EchoLinear.weaken` and `ephapax-L3-no-section-collapse = EchoResidue.no-section-collapse-to-residue`. Coq headlines `mode_le_prop`, `weaken_collapses_distinction`, `affine_canonical`, `degrade_mode_comp`, `no_section_collapse_to_residue` (line 502-517) each match an Agda counterpart pinned in `Smoke.agda`. Scope: **L3 only** — ephapax-affine has Rust checkers only; L1 has 5 `Axiom` + 11 `Admitted`; L4 has no mechanised theorems yet (cf. ephapax `formal/PRESERVATION-DESIGN.md`, `docs/echo-types/paper.adoc` §"Threats to validity"). | Per-bridge docs `docs/bridges/ECHO-EPHAPAX-BRIDGE.adoc` (CNO-equivalent) not yet authored; tracked as follow-up issue. Full content bridge (round-trip CI between Agda + Coq) would require an Agda mirror of ephapax `formal/Echo.v` and is **not foreclosed** by the NARROW stub. |
+| Valence Shell / Ochránce accountable-shell bridge (exploratory, downstream) | Structured-loss vocabulary only — `EchoResidue` / `EchoResidueTaxonomy` / `EchoLossTaxonomy` / `EchoObservationalEquivalence` / `EchoNoSectionGeneric` cited at the reading-aid level. **No bridge module**; nothing added to `All.agda`, `Smoke.agda`, or `EchoCanonicalIdentitySuite.agda`. | Valence Shell (`hyperpolymath/valence-shell`) — shell state transitions, undo/redo, checkpoints, diff/replay. Ochránce (`hyperpolymath/ochrance`) — A2ML manifests, Merkle state commitments, repair/attestation surfaces. | **Exploratory — candidate downstream consumer. Core Affect: NO.** Echo Types' structured-loss semantics may *classify* shell state transitions by residue / loss form (recoverable / constrained / residue-bearing / observationally equivalent / genuinely lost); Ochránce may supply concrete receipt evidence. Downstream application evidence only — not a new foundation. No mechanised cross-repo theorem currently exists. Companion: `docs/bridge-status.md` §7 and `docs/echo-types/explorations/accountable-shell/README.adoc`. | No shared schema and no Agda↔Idris2 / Agda↔Rust import path; the relationship is citation-level only. Echo Types makes **no** claim about Valence Shell / Ochránce implementation correctness, and **no** claim about POSIX, Rust, the Lean→Rust correspondence, secure deletion, GDPR, cryptographic integrity, or attestation. Valence Shell's RMR/RMO vocabulary, if referenced, is downstream application vocabulary and is not adopted into the Echo Types core. |
 
 ## Immediate next actions
 
@@ -66,6 +67,12 @@ precisely to paper over this in the relational model.
 
 ## Revision history
 
+- 2026-06-02: Added the Valence Shell / Ochránce accountable-shell
+  bridge row as an exploratory downstream-consumer entry (Core Affect:
+  NO; citation-level only, no bridge module, nothing wired into
+  `All.agda` / `Smoke.agda` / `EchoCanonicalIdentitySuite.agda`).
+  Mirrored in `docs/bridge-status.md` §7 and the exploratory note
+  `docs/echo-types/explorations/accountable-shell/README.adoc`.
 - 2026-05-20: Closed CNO content-bridge row; baked Agda↔Coq↔Lean4
   correspondence table in; updated JanusKey row with the
   structural-mirror decision and the 4-vs-8 enum drift; closed the

docs/echo-types/explorations/accountable-shell/README.adoc

@@ -0,0 +1,118 @@
+// SPDX-License-Identifier: CC-BY-4.0
+// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Valence Shell / Ochránce accountable-shell bridge — exploratory
+:toc: macro
+:toclevels: 2
+:sectnums:
+:sectnumlevels: 2
+:icons: font
+
+[CAUTION]
+====
+*EXPLORATORY — downstream application evidence, not Gate theory.*
+Not load-bearing for the identity claim.  Subject to abandonment.
+Does not constrain Pillar E or any Lane 1–4 close-out.  *Core Affect:
+NO.*  There is no Agda artefact for this bridge; nothing here is
+imported into `proofs/agda/All.agda`, `proofs/agda/Smoke.agda`, or
+`proofs/agda/EchoCanonicalIdentitySuite.agda`, so the verified suite
+is unaffected by anything in this directory.
+====
+
+toc::[]
+
+== Scope, in one paragraph
+
+Valence Shell / Ochránce is a *possible downstream consumer* of Echo
+Types' structured-loss semantics.  The bridge is exploratory and has
+*Core Affect: NO*.  Valence Shell (`hyperpolymath/valence-shell`) is
+an accountable shell with reversible operations, undo/redo, named
+checkpoints, and diff/replay.  Ochránce (`hyperpolymath/ochrance`) is
+a filesystem verification framework that produces concrete receipt
+evidence — A2ML manifests, Merkle state commitments, and
+repair/attestation surfaces.  This directory records a *candidate*
+observation: that Echo Types' vocabulary for structured loss might
+serve as a semantic language for classifying the information change
+carried by a shell or filesystem state transition, and that Ochránce
+might supply the concrete evidence such a classification would
+consume.  The observation is exploratory.  It is not a generalisation
+claim, not a new identity claim, not a pillar, not a gate, and not a
+mechanised cross-repo theorem.
+
+== The candidate classification (reading aid only)
+
+A shell or filesystem state transition `s ↦ s'` carries an
+information change.  Echo Types already names several shapes of such
+change as *existing* artefacts in this repo, at the K-free honesty
+level:
+
+[cols="1,3", options="header"]
+|===
+| Informal class | Candidate Echo Types vocabulary (existing modules)
+
+| recoverable
+| a section / left-leg equivalence exists (`EchoTotalCompletion`,
+  `EchoLossTaxonomy` EQUIV case)
+
+| constrained
+| injective / graded narrowing (`EchoLossTaxonomy` INJ case,
+  `EchoGraded`)
+
+| residue-bearing
+| a lowering carries partial information (`EchoResidue`,
+  `EchoResidueTaxonomy`)
+
+| observationally equivalent
+| indistinguishable at the chosen observation mode
+  (`EchoObservationalEquivalence`)
+
+| genuinely lost
+| no section over the residue (`EchoNoSectionGeneric`,
+  trivial-residue collapse)
+|===
+
+The mapping is a reading aid only.  No claim is made that any Valence
+Shell or Ochránce operation *has been proved* to fall into any class.
+The table records which existing Echo Types theorem each informal
+class would correspond to *if* such a downstream classification were
+ever carried out.  The Agda named in the right column is the source
+of truth for what is actually proved; this directory adds nothing to
+it.
+
+== What this bridge does NOT claim
+
+* It does *not* claim Echo Types proves Valence Shell (or Ochránce)
+  implementation correctness.
+* It makes *no* claim about POSIX semantics, Rust, the Lean→Rust
+  correspondence, secure deletion, GDPR compliance, cryptographic
+  integrity, or Ochránce attestation.
+* It does *not* promote any cross-repo statement to core-theorem
+  status; *Core Affect: NO*.
+* It adds no postulates and no Agda modules.
+* Valence Shell's own RMR (Remove-Match-Reverse) / RMO
+  (Remove-Match-Obliterate) vocabulary is *downstream application
+  vocabulary*.  Where it appears here it is named only as the
+  consumer's own terminology; it is not adopted into, nor mirrored
+  by, the Echo Types core.
+
+== Direction of the bridge
+
+The bridge is one-directional by intent: Echo Types is *upstream*
+(the semantic vocabulary), Valence Shell and Ochránce are *downstream*
+(candidate consumers).  Downstream consumers must not alter the core
+theory.  Any future formal work would live in the consuming repos or
+in a clearly-separated bridge module, never in the canonical identity
+suite, the F5 / OFS universal-property story, or the establishment
+framing.
+
+== Status and termination
+
+Exploratory.  The bridge is retired if any of the following hold: the
+downstream repos adopt a different semantic foundation; no concrete
+Valence Shell / Ochránce operation is ever classified against the
+table above; or the relationship is found redundant with the existing
+in-repo residue / loss framing.
+
+Status anchors:
+
+* `docs/bridge-status.md` §7 (concise ledger, Core Affect: NO);
+* `docs/bridges/cross-repo-bridge-status.md` (cross-repo track table).