diff --git a/docs/bridge-status.md b/docs/bridge-status.md index ae9d07b..cb139d7 100644 --- a/docs/bridge-status.md +++ b/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 diff --git a/docs/bridges/cross-repo-bridge-status.md b/docs/bridges/cross-repo-bridge-status.md index df58909..51f4e46 100644 --- a/docs/bridges/cross-repo-bridge-status.md +++ b/docs/bridges/cross-repo-bridge-status.md @@ -2,7 +2,7 @@ # 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 diff --git a/docs/echo-types/explorations/accountable-shell/README.adoc b/docs/echo-types/explorations/accountable-shell/README.adoc new file mode 100644 index 0000000..12dcc38 --- /dev/null +++ b/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 += 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).