diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml index ad9436d..e387253 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.machine_readable/6a2/META.a2ml @@ -14,7 +14,7 @@ [metadata] project = "echo-types" -last-updated = "2026-06-12" +last-updated = "2026-06-21" # ============================================================ # Architecture Decision Records @@ -319,6 +319,38 @@ PRs #161/#162/#163. module = "proofs/agda/EchoEphapaxBridge.agda" supersedes = "none" +[[architecture-decisions]] +id = "adr-012" +title = "Ordinal/Buchholz track RETIRED from echo-types; disposition = extraction" +status = "accepted" +date = "2026-06-21" +context = """ +The transfinite ordinal / Buchholz / Veblen ascent (target ψ₀(Ω_ω)) outgrew +echo-types. It was PARKED 2026-06-20 (D-2026-06-20: consumer-less after the +Groove cleave resolved to a finite, well-foundedness-only zipper), then +escalated to RETIRED 2026-06-21 (D-2026-06-21). The landed artifact is correct +(--safe --without-K, zero postulates, in the green closure); Echo Core never +depended on it beyond the OmegaMarkers <- Buchholz.Syntax <- EchoOrdinal bridge. +""" +decision = """ +No new ordinal rung is opened in echo-types. The disposition is extraction to +its own ordinal-notation repository — the physical cross-repo cut is the +owner's (tracking issue #263). Firewall: OmegaMarkers <- Buchholz.Syntax <- +EchoOrdinal STAY; everything else under proofs/agda/Ordinal/ MOVES. Order-type +fidelity to ψ₀(Ω_ω) (D-2026-06-14) remains an OPEN external problem — +retirement neither closes nor over-claims it. +""" +consequences = """ +The [recent-work] / [current-workstream] blocks in STATE.a2ml are preserved as +HISTORY of the 2026-06-05 -> 2026-06-12 ordinal-track arc, not live work. +Hand-off record: docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc. +Live tracks: composition (landed); establishment (Pillars A–D+F closed, Pillar +E in-repo complete at the bounded-claim level); variance resolved (#243); +aggregation generalised (#175). +""" +module = "proofs/agda/Ordinal/ (whole subtree except the STAY firewall)" +supersedes = "none" + # ============================================================ # Development practices (relevant subset) # ============================================================ diff --git a/docs/bridges/cross-repo-bridge-status.md b/docs/bridges/cross-repo-bridge-status.md index 37be14b..6be0636 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-06-18. +Last updated: 2026-06-21. This file is the single status ledger for echo-type bridge work that touches other repositories. @@ -14,7 +14,7 @@ touches other repositories. | CNO bridge (Agda) | `proofs/agda/EchoCNOBridge.agda` | `absolute-zero/proofs/agda/CNO.agda` (direct import) | **Content-bridge done.** Bridge imports `IsCNO`, `empty-is-cno`, `halt-is-cno`, `cno-composition`, `absolute-zero-is-cno`, `seq-comp` from absolute-zero's `CNO.agda` and exhibits `cno-program-echo : (p : Program) → IsCNO p → ProgramEcho p` plus three concrete instances. `CNO.agda` builds clean under `--safe --without-K`, no postulates. | — (closed at content-bridge level; cross-prover theorem-statement alignment is the next row.) | | 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. | +| 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` ↔ the (now-RETIRED, extracting) echo-types ordinal track — that long-game alignment moves with the ordinal extraction (echo-types#263, owner decision D-2026-06-21); it is not an echo-types deliverable. | | 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. | diff --git a/wiki/Home.adoc b/wiki/Home.adoc index 387136d..1c41085 100644 --- a/wiki/Home.adoc +++ b/wiki/Home.adoc @@ -44,6 +44,14 @@ toc::[] (constant / no-section) case and the partial (injective / has-section) case, with the `IsConstantOpener` boundary and its connection to the affine mode. + +| <> +| End-user walkthrough: the one definition, making/reading an echo, the + totality completion, the no-section boundary, and four real consumers. + +| <> +| Gate-keeping + release runbook: the build cone, the identity gates, + rung-consolidation, machine-doc currency, and the release checklist. |=== == Who is this for? @@ -74,7 +82,9 @@ echo-types serves three audiences. Find your lane, then follow the reading order 3. `scripts/kernel-guard.sh` + `.github/workflows/agda.yml` — the CI cone that must stay green. + 4. `.machine_readable/6a2/STATE.a2ml` (EI-2 record + current state) and - `docs/bridges/cross-repo-bridge-status.md` (downstream ledger). + `docs/bridges/cross-repo-bridge-status.md` (downstream ledger). + + 5. <> — the full gate-keeping + + release runbook (build cone, gates, rung-consolidation, release checklist). | *An end user* + (wiring Echo into another language) @@ -85,7 +95,9 @@ echo-types serves three audiences. Find your lane, then follow the reading order 3. *EchoTypes.jl* — the executable Julia shadow; falsifies-by-counterexample on concrete finite data. + 4. <> — a worked first-class echo property to - see the shape of a consumer-facing result. + see the shape of a consumer-facing result. + + 5. <> — the + from-the-outside-in walkthrough (definition → totality → no-section → consumers). |=== == Canonical sources of truth diff --git a/wiki/Maintainer-Runbook.adoc b/wiki/Maintainer-Runbook.adoc new file mode 100644 index 0000000..002ab06 --- /dev/null +++ b/wiki/Maintainer-Runbook.adoc @@ -0,0 +1,117 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Maintainer Runbook +:toc: macro +:toclevels: 2 + +[.lead] +For *maintainers* — gate-keeping changes, keeping the proof cone green, keeping +the documentation honest, and cutting releases. Authoritative sources: +`roadmap-gates.adoc`, `CLAUDE.md` (current-rung-state + per-arc DO-NOT-reopen +lists), and `.machine_readable/6a2/`. + +toc::[] + +== 1. The non-negotiable build cone + +Every change must hold the invariant: + +[source,sh] +---- +agda -i proofs/agda proofs/agda/All.agda # exits 0 +agda -i proofs/agda proofs/agda/Smoke.agda # exits 0 +sh scripts/kernel-guard.sh # PASS +---- + +under `--safe --without-K`, with *zero postulates* in the load-bearing tracks +and no escape pragmas (`believe_me`, `assert_total`, `postulate`, `sorry`, +`Admitted`, `unsafeCoerce`). Every headline theorem is pinned in `Smoke.agda`; +every new module is wired into `All.agda` (an orphan module that compiles but +is not in `All.agda` is treated as dead code). + +== 2. The identity gates (the falsifiability contract) + +The identity claim rests on three gates, each with an explicit *failure action* +(see <> and `roadmap-gates.adoc`): + +. *Distinct phenomenon* — echo types name structured loss as distinct from + refinement types / lenses / HoTT fibres / quotients / provenance semirings. +. *Characteristic theorems* — at least two theorems are naturally echo-shaped, + not generic Σ lemmas. +. *Canonical examples* — at least one fully worked example where echo types are + the right explanatory unit. + +Gates are *reassessed at every tagged release* — surviving one round grants no +immunity in the next. A failed gate is recorded in `docs/retractions.adoc` (a +new dated `R-`/`F-` entry), *never silently revised*. Retractions are the +mechanism that makes the claim falsifiable; they are not failures of the repo. + +== 3. When a proof rung lands — rung-consolidation policy + +Per `CLAUDE.md`, each named theorem / iso-shape that lands triggers: + +. *Branch housekeeping* — enumerate open remote branches ahead of `main`; + decide landing / superseded / abandoned. +. *Cherry-pick* to a consolidation branch off latest `main`, in dependency + order (conflicts are usually additive, in `Smoke.agda` / `All.agda`). +. *Human docs* — sweep `roadmap.adoc`, `docs/echo-types/composition.md`, + `overview.md`, and the wiki for stale `(Open)` tags; use honest labels + `(Landed)` / `(Partial)` / `(Open)`. +. *Machine docs* — update `CLAUDE.md` current-rung-state and the `6a2/` files + (see Section 4). +. *Verify* — the build cone (Section 1). +. *Fast-forward `main`* and push. +. *Session ledger* — record the rung, the commits folded in, the remaining + open pieces, and the smallest useful next advance. + +== 4. Machine-doc currency discipline + +When a *track's status changes*, the change must propagate to all of: + +* `.machine_readable/6a2/STATE.a2ml` — `[metadata]` phase + the current-workstream + framing (historical blocks are preserved, not deleted; mark them HISTORY). +* `.machine_readable/6a2/META.a2ml` — add an ADR for any architecture-level + decision (status / supersedes per `[development-practices.versioning-of-decisions]`). +* `docs/bridges/cross-repo-bridge-status.md` — the bridge ledger. +* the wiki (<> one-line status + <>). + +Worked example: the 2026-06-21 ordinal-track *retirement* (`D-2026-06-21`) was +swept through STATE.a2ml (currency note + phase), META.a2ml (adr-012), the +bridge ledger (Tropical long-game row), and the wiki — keeping human and +machine documentation consistent. Mirror that pattern. + +== 5. Release checklist + +Versioning is SemVer 2.0.0 (current target `0.1.1`; recipe-extension target +`0.2.0+`). To cut a release: + +. [ ] Build cone green (Section 1) on `main`. +. [ ] Identity gates reassessed (Section 2); any failure recorded in + `docs/retractions.adoc`. +. [ ] `CHANGELOG.md` updated; `[Unreleased]` rolled to the version. +. [ ] Machine docs current (Section 4): `6a2/STATE.a2ml`, `META.a2ml`, + bridge ledger, wiki one-line status. +. [ ] Tag minted; mirrors (gitlab, codeberg) consistent. +. [ ] *Then*, author-driven and *not* auto-run: Zenodo DOI, installable library + packaging, outreach. Flag to the owner; do not start unprompted. + +== 6. CI lanes and known parked failures + +Substantive lanes that must stay green: Agda (`check` + `cold-check`), +`governance/*`, the secret scanners (`gitleaks`/`trufflehog`/`*-secrets`), +CodeQL (`analyze`), and Hypatia. A docs-only change passes the Agda lanes +trivially (no `.agda` touched). + +*Parked, do not chase:* `scorecard.yml` / `mirror.yml` `startup_failure` at 0s +is the billing-wall *pattern B* (a structural reusable-workflow failure, not a +Guix/Nix policy failure). Hypatia may post pre-existing repo-level findings +(e.g. a stale Scorecard `TokenPermissionsID` code-scanning alert that cannot +auto-clear while Scorecard is billing-walled); confirm the Hypatia *check +conclusion* (it is usually `success`) before treating a comment as a gate. + +== 7. Branch hygiene + +Single-`main` policy (Hypatia `GS007`). Remote-branch deletion is *owner / +GitHub-UI only* — agents get HTTP 403 and the MCP has no delete-branch +endpoint, so stale-branch cleanup is flagged in an issue and actioned by the +owner. diff --git a/wiki/Tutorial-Consuming-Echo.adoc b/wiki/Tutorial-Consuming-Echo.adoc new file mode 100644 index 0000000..2a9894a --- /dev/null +++ b/wiki/Tutorial-Consuming-Echo.adoc @@ -0,0 +1,118 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Tutorial: Consuming Echo Types +:toc: macro +:toclevels: 2 + +[.lead] +For *end users* — you want to use echo types' structured-loss vocabulary in +your own language, tool, or proof, and you are not (yet) extending the Agda. +This is a from-the-outside-in walkthrough: one idea, one definition, what you +can and cannot do with it, and four real consumers. For the stable interface +contract read `FOUNDATION_CONTRACT.md` first; for the honest "what it does and +does not add" read <>. + +toc::[] + +== 1. The one idea + +A function that is *not injective* throws information away: if `f a₁ = f a₂` +with `a₁ ≠ a₂`, then from the output alone you cannot tell which input you had. +An *echo* keeps the witness that would otherwise be forgotten — it is the +*fibre* of `f` over an output, the proof-relevant collection of inputs that +collapse onto it. + +== 2. The one definition + +[source,agda] +---- +Echo f y := Σ (x : A) , (f x ≡ y) +---- + +Read it as: an `Echo f y` is a pair of an input `x` together with *evidence* +that `f` sends `x` to `y`. It is exactly the homotopy fibre `fiber f y` +(`EchoFiberBridge.agda` pins `echo↔fib`). Everything load-bearing is verified +under `--safe --without-K` with zero postulates. + +== 3. Making and reading an echo + +[source,agda] +---- +echo-intro : (f : A → B) → (x : A) → Echo f (f x) +---- + +`echo-intro f x` is the canonical echo at `x`. To read it back, `proj₁` +recovers the input and `proj₂` is the equation `f x ≡ y`. An echo is therefore +a *receipt*: it records both the value and the witness the bare output dropped. + +== 4. The totality completion (the slogan) + +The single most-cited result is that the input space is recoverable from the +output space *together with its echoes*: + +[source,agda] +---- +A↔ΣEcho : A ↔ Σ B (Echo f) -- EchoTotalCompletion.agda +---- + +In words: *an irreversible computation, paired with its echoes, is a reversible +representation.* If you keep the fibres, you have lost nothing — `encode` and +`decode` round-trip. This is the design pattern a consumer adopts: run your +collapsing map, but carry the echo alongside the result. + +== 5. What you cannot do — the honest boundary + +Echo *records* loss; it does not *undo* it. If `f` genuinely collapses two +inputs to one output, there is no left inverse `raise : B → A` with +`raise ∘ f ≡ id`: + +[source,agda] +---- +no-section-of-collapsing-map -- EchoNoSectionGeneric.agda +---- + +This is the load-bearing negative result. A consumer that wants recovery must +*store the echo* (Section 4); it cannot reconstruct it from the output. The +boundary invariant *Echo IS-NOT a resource instance* (see +`FOUNDATION_CONTRACT.md`) is the same statement read at the interface level. + +== 6. Four real consumers + +These are in-repo or in-estate bridges, not hypotheticals (ledger: +`docs/bridges/cross-repo-bridge-status.md`). + +* *phronesis (agentic ethics).* An ethical verdict's provenance IS + `Echo verdict v`: the evaluator is non-injective, so the fibre retains *which* + expressions justify a verdict that the bare `Bool` forgets + (`verdict-forgets-provenance`); `proj₁` is the recovering section. +* *KitchenSpeak (nextgen-languages).* A sensor `@`-witness IS + `Echo (fired sensor thr) true` — the firing evidence is the echo + (`witness⇒echo` / `echo⇒witness`), machine-checked against the real `Echo`. +* *Invariant Path (Rust).* `classify_candidate` is a non-injective classifier; + the retained candidate plus its `losses` IS the echo over a classification. + Invariant Path is "a claim-path debugger, not a truth engine" *precisely + because* it keeps the echoes. +* *EchoAggregation (economics).* Rolling a micro ledger up to a macro total is + a collapsing map; `no-canonical-disaggregation` is the + Sonnenschein–Mantel–Debreu / representative-agent critique stated + type-theoretically — there is no canonical way back down. + +== 7. Honest scope + +Everything above is `--safe --without-K`, zero postulates. The fuller +universal-property story (uniqueness up to iso, diagonal lifting) is +*funext-qualified*; UIP- and truncation-strength refinements (the full (epi, +mono) image factorisation) are explicit earn-backs, not silently assumed. The +executable companion *EchoTypes.jl* mirrors the finite-domain shadow and +*falsifies by counterexample* on concrete data — but the Agda here is the +source of truth. See <> for the full add / does-not-add +table. + +== 8. Where to go next + +* `FOUNDATION_CONTRACT.md` — the stable `Echo.*` interface to build against. +* *EchoTypes.jl* — run the finite-domain shadow on your own data. +* `docs/bridges/cross-repo-bridge-status.md` — every consumer bridge, with its + honest scope and main blocker. +* <> — a worked first-class echo property + (perfect vs partial; section vs no-section) to see the shape of a result.