From f0b34823b4e82c2b8d6bf7b58cb4ae9d42d41885 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 23 May 2026 00:26:35 +0100 Subject: [PATCH 01/10] feat(security): fleet-wide workflow hardening (SHA pinning + permissions) --- .github/workflows/agda.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml index 524f39d..12947a2 100644 --- a/.github/workflows/agda.yml +++ b/.github/workflows/agda.yml @@ -115,7 +115,7 @@ jobs: # source change or absolute-zero bump; restore-keys give a warm # partial cache even when it does. - name: Cache Agda interface files - uses: actions/cache@v4 + uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4 with: path: | ~/agda-stdlib/**/*.agdai From 6373d1d264273eb1cb64fe4c89201de8005e4c03 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 26 May 2026 22:48:32 +0100 Subject: [PATCH 02/10] =?UTF-8?q?docs:=20consolidate=205=20roadmaps=20into?= =?UTF-8?q?=20single=20canonical=20roadmap.adoc;=20promote=20Echo-vs-?= =?UTF-8?q?=CE=A3=20skepticism=20into=20reviewer-facing=20answer?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Roadmap consolidation - Delete 4 overlapping roadmap docs (docs/echo-types/roadmap.md, docs/PRIORITIZED_PROOF_ROADMAP.md, docs/ProofRoadmap.md, docs/WORK_PLAN.md). - Rewrite roadmap.adoc as the single canonical roadmap: 5-lane tracker with falsifiable close-out criteria audited at every rung consolidation, gates summary, pillar status, M1-M13 historical milestone log, R1-R4 deferred research preserved, lane discipline rules, retraction-watch lines per lane. - Lane 1 (load-bearing) = expeditious type-theoretic grounding alongside choreographic / linear / graded modal types. Lane 3 (Ordinal/Buchholz) explicitly parallel-independent: Echo Core does NOT depend on it. README + readme.adoc Status Snapshot restructure - Split into "Echo Core" and "Ordinal / Buchholz" as parallel- independent tracks with explicit non-dependency banner. Buchholz modules marked experimental until unbudgeted wf-<ᵇʳᶠ_ closure lands. Roadmap section points only at roadmap.adoc and its companion docs (roadmap-gates.adoc, establishment-plan.adoc, buchholz-plan.adoc, taxonomy.md, composition.md). Echo-vs-Σ identity claim (Track A) - Promote core/skepticisms/is-this-just-sigma-types.md from 14-line stub into canonical Echo-vs-Σ map. Five sections mirroring the sceptic demands: irreversibility-as-theorem-family, algebra of loss, categorical identity + bridges, abstraction barrier (consumer-side), canonical examples. Each section cross-links Agda lemmas + Smoke pins + adjacency notes. - Add docs/echo-types/sigma-distinctness-map.adoc as reviewer-facing AsciiDoc companion (same 5-section structure, heavier cross-refs to gates and pillars). - Add no-section family and degrade-laws aggregate rows to docs/theorem-index.md. - Cross-link from roadmap-gates.adoc Gate 2 and docs/characteristic.adoc §"Inherited spec". Cross-ref sweep - 17 files redirected from the 4 deleted roadmap docs to roadmap.adoc (or to more specific surviving docs where the original reference was content-specific). Covers CLAUDE.md, READMEs, MAP.adoc, decision docs, Agda module comments, bridge docs. Retraction discipline - All prose stays inside R-2026-05-18 narrowed claims: no full universal property (only funext-relative pointwise mediator), no graded comonad (only thin-poset reindexing modality), no model- independence (only carrier-parametricity over a fixed grade poset), no Reynolds parametricity (only consumer-side free theorem at the affine instance, planned in Track B). Net diffstat: +711 / -1937 across 25 files. Co-Authored-By: Claude Opus 4.7 (1M context) --- CLAUDE.md | 8 +- DOCUMENTATION_STATUS.md | 4 +- README.md | 50 +- core/skepticisms/is-this-just-sigma-types.md | 157 +++- docs/PRIORITIZED_PROOF_ROADMAP.md | 458 --------- docs/ProofRoadmap.md | 184 ---- docs/WORK_PLAN.md | 323 ------- docs/bridges/ECHO-CNO-BRIDGE.adoc | 4 +- docs/bridges/tropical-correspondence.md | 4 +- docs/characteristic.adoc | 7 + docs/echo-types/MAP.adoc | 13 +- .../applications-compiler-analysis.adoc | 2 +- .../decisions/gate1-adjacency-refresh.adoc | 6 +- docs/echo-types/decisions/no-2-cat.adoc | 4 +- .../decisions/presentation-dependence.adoc | 4 +- docs/echo-types/establishment-plan.adoc | 4 +- docs/echo-types/roadmap.md | 431 --------- docs/echo-types/sigma-distinctness-map.adoc | 189 ++++ docs/echo-types/tropical-correspondence.md | 4 +- docs/theorem-index.md | 45 + proofs/agda/EchoLinear.agda | 2 +- proofs/agda/EchoStabilityTests.agda | 2 +- proofs/agda/EchoThermodynamics.agda | 5 +- readme.adoc | 33 +- roadmap-gates.adoc | 10 + roadmap.adoc | 884 ++++++++---------- 26 files changed, 900 insertions(+), 1937 deletions(-) delete mode 100644 docs/PRIORITIZED_PROOF_ROADMAP.md delete mode 100644 docs/ProofRoadmap.md delete mode 100644 docs/WORK_PLAN.md delete mode 100644 docs/echo-types/roadmap.md create mode 100644 docs/echo-types/sigma-distinctness-map.adoc diff --git a/CLAUDE.md b/CLAUDE.md index f973cc7..59f893f 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -176,7 +176,7 @@ work to `main` and refresh all documentation: dependency order. Resolve any conflicts (typically additive, in `Smoke.agda` and `All.agda`). 3. **Update human docs.** `docs/echo-types/composition.md`, - `docs/echo-types/roadmap.md`, `docs/echo-types/overview.md` and + `roadmap.adoc`, `docs/echo-types/overview.md` and `cross-repo-bridge-status.md` get a sweep for stale `(Open)` / `[unblocked]` tags on anything that just landed. Honest labels: `(Landed)`, `(Partial)`, `(Open)`. @@ -503,7 +503,8 @@ coeffects, lens/optic vs the witness-transport leg); (3) evaluation (proof-size/cost table; quantify common-upper-bound idiom vs naive `subst`); (4) ordinal consumer-evidence appendix — GATED on the ordinal track hitting Bachmann–Howard, keep firewalled per -`roadmap.md`. THEN offline/author-driven only (venue+template, +`roadmap.adoc` §Lane 3 (Ordinal track) and `docs/buchholz-plan.adoc`. +THEN offline/author-driven only (venue+template, Zenodo DOI, library packaging, outreach) — flag to the user, do NOT auto-run. Strategy (user decision 2026-05-17): the paper was written now at full narrative strength while fresh; expand the tagged @@ -590,7 +591,8 @@ tags as material becomes available, in this order: 3. Evaluation — proof-size/cost table; quantify common-upper-bound-idiom vs naive `subst`. 4. Ordinal consumer-evidence appendix — gated on that track hitting - its Bachmann–Howard milestone (firewalled per roadmap.md). + its Bachmann–Howard milestone (firewalled per `roadmap.adoc` + §Lane 3 and `docs/buchholz-plan.adoc`). 5. THEN offline/author-driven: venue+template, Zenodo DOI, library packaging, outreach — flag to user, do NOT auto-run. diff --git a/DOCUMENTATION_STATUS.md b/DOCUMENTATION_STATUS.md index 92ee361..886fc66 100644 --- a/DOCUMENTATION_STATUS.md +++ b/DOCUMENTATION_STATUS.md @@ -6,7 +6,7 @@ 1. **Core Bridge Documentation** - `docs/EchoJanusBridge.md` - Comprehensive explanation of echo types → JanusKey bridge - - `docs/ProofRoadmap.md` - Strategic proof development roadmap + - `roadmap.adoc` §"Deferred research track" - Strategic proof development roadmap (consolidated from former `docs/ProofRoadmap.md`) - `docs/COMPREHENSIVE_DOCUMENTATION.md` - Complete 3-2-1 structured documentation 2. **Formal Proofs** @@ -84,7 +84,7 @@ - [x] Create `EchoJanusBridge.agda` with core theorems - [x] Update `All.agda` to include new module - [x] Write `EchoJanusBridge.md` documentation -- [x] Create `ProofRoadmap.md` for future work +- [x] Consolidate `ProofRoadmap.md` into `roadmap.adoc` (single canonical roadmap) - [x] Develop `COMPREHENSIVE_DOCUMENTATION.md` (3-2-1 structure) - [x] Verify Agda proofs compile successfully - [ ] Add architecture diagrams diff --git a/README.md b/README.md index 5381197..9a084b5 100644 --- a/README.md +++ b/README.md @@ -79,7 +79,15 @@ Scope-broadening stages now include: - indexed/relational/categorical packaging (`EchoIndexed`, `EchoRelational`, `EchoCategorical`, `EchoScope`) - cross-ecosystem bridges (`EchoCNOBridge`, `EchoJanusBridge`, `DyadicEchoBridge`, `EchoOrdinal`) -## Current Status Snapshot (2026-04-23) +## Current Status Snapshot + +The repository runs **two parallel, independent tracks**. *Echo Core does +NOT depend on the Ordinal / Buchholz track.* A reader interested only +in echo types as a type-theoretic concept can ignore the Ordinal track +entirely; it lives in `proofs/agda/Ordinal/` and is documented under +`roadmap.adoc` §Lane 3. + +### Echo Core (load-bearing for the identity claim) On `main`, the following are true: @@ -87,8 +95,23 @@ On `main`, the following are true: - core echo/fiber laws are smoke-pinned (`echo-intro`, `map-over`, `map-over-id`, `map-over-comp`, `map-square`) - non-injectivity/no-section family is present (`collapse-non-injective`, `no-section-collapse`, `no-section-visible`, `no-section-collapse-to-residue`, `no-section-weaken`) - distinct-witness and retained-constraint exemplars are present (`echo-true≢echo-false`, `stateA≢stateB`, `visible-constraint`) +- degrade-law family lands across decoration layers (graded, linear/affine, choreographic, access, cost, search); see `docs/theorem-index.md` for the aggregate +- Pillars A–D of the establishment plan are LANDED (with R-2026-05-18 narrowings; see `docs/retractions.adoc`); Pillar E (paper) is in progress + +Per-lane status, close-out criteria, and the identity-claim verdict +per tag are in `roadmap.adoc`. -Ordinal/Buchholz track status: +### Ordinal / Buchholz (parallel-independent, experimental) + +> **Banner.** This track is a separate proof-theoretic research project +> living in the same repository. Echo Core does not depend on it. +> Modules under `proofs/agda/Ordinal/` are treated as **experimental** +> until the unbudgeted `wf-<ᵇʳᶠ_` closure lands. See `roadmap.adoc` +> §Lane 3 for status and close-out criterion; `docs/buchholz-plan.adoc` +> for the full plan. + +Current state (one-line summary; the full per-rung ledger lives in +CLAUDE.md): - `Ordinal.Buchholz.WellFounded` provides `wf-<ᵇ : WellFounded _<ᵇ_` for the currently admitted constructor core - top-marker `bplus` bridges are admitted and inverted: `<ᵇ-+ω`, `<ᵇ-+ψω`, `<ᵇ-inv-+Ωω`, `<ᵇ-inv-+ψω` @@ -131,7 +154,7 @@ Cross-repo status: - Agda-side content-bridge `proofs/agda/EchoCNOBridge.agda` imports `IsCNO` directly from `absolute-zero/proofs/agda/CNO.agda` (the earlier scaffolded-adapter plan `EchoBridgeScaffold.agda` was superseded) - end-to-end conformance against upstream codebases is a separate track and is not yet fully machine-checked here - current bridge ledger: `docs/echo-types/cross-repo-bridge-status.md` -- see `docs/echo-types/roadmap.md` for staged cross-repo verification gates +- see `roadmap.adoc` (Lane 4) for staged cross-repo verification gates ## What Echo Types Are For @@ -187,16 +210,25 @@ agda -i proofs/agda proofs/agda/All.agda ## Roadmap -Proof milestones and decision gates are in: +Single canonical roadmap with lane tracker, gates summary, pillar +status, deferred-research track, and operating rules: - `roadmap.adoc` -- `docs/buchholz-plan.adoc` -Open/gated work and cross-repo follow-ups are tracked in: +Companions (different kinds of doc, not roadmaps): + +- `roadmap-gates.adoc` — identity-claim falsifier gates (Gate 1/2/3) +- `docs/echo-types/establishment-plan.adoc` — five-pillar plan to + recognised type-theoretic standing +- `docs/buchholz-plan.adoc` — Ordinal track plan (parallel-independent + lane; see roadmap.adoc §Lane 3) +- `docs/echo-types/taxonomy.md`, `docs/echo-types/composition.md` — + topical reference -- `docs/echo-types/roadmap.md` -- `docs/echo-types/taxonomy.md` -- `docs/echo-types/composition.md` +As of 2026-05-26 the four previously overlapping roadmap docs +(`docs/echo-types/roadmap.md`, `docs/PRIORITIZED_PROOF_ROADMAP.md`, +`docs/ProofRoadmap.md`, `docs/WORK_PLAN.md`) have been consolidated +into `roadmap.adoc` and removed. ## Licensing diff --git a/core/skepticisms/is-this-just-sigma-types.md b/core/skepticisms/is-this-just-sigma-types.md index 01b36d4..8c77b6d 100644 --- a/core/skepticisms/is-this-just-sigma-types.md +++ b/core/skepticisms/is-this-just-sigma-types.md @@ -1,13 +1,162 @@ # Is this just Sigma Types? ## The Skeptical Position -Yes, at the lowest level of Agda code, this is `Σ (x : A) , (f x ≡ y)`. It relies entirely on the standard dependent pair type and propositional equality. +Yes, at the lowest level of Agda code, this is `Σ (x : A) , (f x ≡ y)`. +It relies entirely on the standard dependent pair type and propositional +equality. ## The Burden of Proof -Any claim of utility must show why working with the `Echo` wrapper is better than directly pattern-matching on the Sigma type. If every proof immediately unpacks the `Echo` and does standard Sigma-type manipulation, the abstraction is leaky and pointless. +Any claim of utility must show why working with the `Echo` wrapper is +better than directly pattern-matching on the Sigma type. If every proof +immediately unpacks the `Echo` and does standard Sigma-type manipulation, +the abstraction is leaky and pointless. ## Collapse Conditions -If the `Echo` interface requires the user to manually manage the underlying `Σ` structure to accomplish basic composition or mapping tasks, the abstraction fails. +If the `Echo` interface requires the user to manually manage the +underlying `Σ` structure to accomplish basic composition or mapping +tasks, the abstraction fails. ## Reinterpretation vs. Novelty -The novelty must reside in the API and the categorical/compositional properties exposed by the wrapper, demonstrating that `Echo` behaves coherently under lossy operations in a way that bare Sigma types do not automatically communicate. +The novelty must reside in the API and the categorical/compositional +properties exposed by the wrapper, demonstrating that `Echo` behaves +coherently under lossy operations in a way that bare Sigma types do not +automatically communicate. + +--- + +## Answer: the in-tree evidence + +This section is the index reviewers can walk to confirm Echo is not +"renamed Σ". It is organised under five demands a sceptic typically +makes. Each item points at a machine-checked Agda artefact (pinned in +`proofs/agda/Smoke.agda`), a doc, or both. Statements stay inside the +*narrowed* claims of `docs/retractions.adoc` R-2026-05-18 — no "full +universal property", no "graded comonad", no "model-independence". + +### 1. Irreversibility is a theorem family, not a property + +A raw `Σ (x : A) (f x ≡ y)` gives `proj₁` trivially; the user can +always extract the original `x`. The Echo programme proves that *no* +section exists once specific lossy interfaces are applied. The witness +is a *family* across five separate decoration layers: + +- `EchoCharacteristic.no-section-collapse` — no section of the + `Bool → ⊤` collapse map. +- `EchoCharacteristic.no-section-visible` — no section recovering the + pre-image from a visible output alone. +- `EchoResidue.no-section-collapse-to-residue` — weakening to a residue + is provably one-way. +- `EchoLinear.no-section-weaken` — the `linear → affine` mode shift is + one-way (defined as the residue lemma). +- `EchoOrdinal.no-section-ordinal-collapse` — ordinal collapse case. +- `EchoEpistemicResidue.no-section-to-epistemic` — epistemic-residue + case. + +All six are pinned in `Smoke.agda`. The family is what carries the +weight: each decoration *separately* refuses the section that a raw Σ +would admit. See also `docs/theorem-index.md` and the prose write-up at +`docs/characteristic.adoc`. + +### 2. Loss is graded, and downgrades cannot be reversed + +A raw Σ has no built-in notion of "degrading from strict to loose". +Echo equips the fibre with a lattice of grades and a monotone reindexing +along it. The two halves of the asymmetry are: + +- *Down-step is admissible.* `EchoGraded.degrade-compose` and + `EchoGraded.degrade-via-join` — the per-decoration composition law + for the loss-grade order. Same recipe lands at: + - `EchoLinear.degradeMode-compose` (linearity-mode order), + - `EchoChoreo.applyChoreo-compose` (role/reachability order), + - `EchoAccess` (graded access modality), + - `EchoCost` (cost-indexed refinement), + - `EchoSearch` (witness-search refinement). +- *Up-step is not.* `no-section-weaken` (item 1) is the same + statement on the other diagonal — once degraded, no inverse exists. + +Honest framing: this is a *thin-poset reindexing modality*, not a +graded comonad. The retraction at `docs/retractions.adoc#R-2026-05-18` +narrowed an earlier "graded comonad" claim. The reindexing modality is +the load-bearing structure and is the right answer to "is Σ enough?": +Σ alone gives neither the monotone reindex nor the no-section dual. + +### 3. Echo is the homotopy fibre; bridges from other "loss-tracker" frameworks exist + +The categorical/identity claim is **deflationary** and owned in +`docs/echo-types/establishment-plan.adoc`: `Echo f y` is *definitionally* +the homotopy fibre `fib f y` (HoTT book Def. 4.2.4). The bridge is +`EchoFiberBridge.echo↔fib`, both round-trips `refl` (Pillar A; pinned +in `Smoke.agda`). + +For the "is this just a pullback" question, `EchoPullback.echo-pullback-univ` +exhibits `Echo f y` as the pullback of `f` along `y : ⊤ → B` with a +*pointwise, funext-relative* mediator property. The retraction note in +that module is loud: this is **not** a full categorical universal +property in the absence of funext. Bridges from named neighbour +frameworks land as separate modules: + +- `EchoFiberBridge.agda` — homotopy fibre identity. +- `EchoJanusBridge.agda` — Janus-style reversible debugger bridge. +- `EchoTropical.agda` / `AntiEchoTropical.agda` — tropical + semiring / argmin decomposition. +- `EchoCNOBridge.agda` — categorical neighbour bridge. +- `EchoFiberCount.agda` + `EchoThermodynamics*.agda` — finite-fibre + Landauer / Bennett correspondence. + +These are independent witnesses, not one universal theorem. The honest +verdict is "Echo is *a* canonical target with concrete bridges in" +rather than "Echo is *the* terminal residue tracker by unique mediator". + +### 4. The abstraction barrier (consumer-side) + +A raw `Σ A (λ x → f x ≡ y)` exposes `proj₁`, so a consumer can always +distinguish two preimages of the same output. The Echo interface at the +affine mode does not export that projection: the residue carrier is +contractible (`EchoLinear.affine-canonical`, `affine-all-equal`), so +any consumer assigns the same value to the weakened images of two +known-distinct linear echoes. + +**Status:** the consumer-side abstraction-barrier theorem is the one +genuine gap relative to the five demands. It is planned as +`proofs/agda/EchoAbstractionBarrier.agda` (Track B in the work plan). +The model-side counterpart — *carrier-parametricity* over a fixed +grade poset — already lands as `EchoRelModel` (Pillar D, narrowed per +R-2026-05-18 from the original "model-independence" wording). + +### 5. Canonical examples — what Σ would let through + +The example modules exhibit echo as the explanatory unit on real +artefacts: + +- `EchoExampleParser` — `(())` vs `()()` are two distinct echoes at the + same `parses ≡ true`. +- `EchoExampleProvenance` — distinct Bool-provenance rows collapse to + the same payload; the echo carries the lost annotation. +- `EchoExampleAbsInt` — `{p1, p2}` collapse to `pos` under sign + analysis; the echo retains which. +- `EchoExampleSignAnalysis`, `EchoExampleTruncation` — further + collapse-with-residue exhibits. +- `EchoFiberCount` + `EchoThermodynamics*` — finite-fibre Landauer + bound for the erasure cost. +- `EchoEpistemicResidue` — observation-discipline residue. + +Each is positive evidence. The matched *negative* — a small raw-Σ +counter-program that would let the bug through — is planned as +`proofs/agda/examples/EchoVsSigma.agda` (Track C). Until that lands, +the "raw Σ would leak" claim is prose, not a checked artefact. + +--- + +## Cross-references + +- Gate 2 audit (closest reviewer touchpoint): + `docs/characteristic.adoc`. +- Theorem-by-theorem ledger: `docs/theorem-index.md`. +- Adjacency notes (per neighbour framework): `docs/adjacency/`. +- Honest scope of the establishment claim: + `docs/echo-types/establishment-plan.adoc` and + `docs/echo-types/paper.adoc` §"Reframing note". +- AsciiDoc reviewer companion to this file: + `docs/echo-types/sigma-distinctness-map.adoc`. +- Companion skepticisms: `is-this-just-fibers.md`, `what-is-actually-new.md`, + `failure-conditions.md`. diff --git a/docs/PRIORITIZED_PROOF_ROADMAP.md b/docs/PRIORITIZED_PROOF_ROADMAP.md deleted file mode 100644 index 6b20a59..0000000 --- a/docs/PRIORITIZED_PROOF_ROADMAP.md +++ /dev/null @@ -1,458 +0,0 @@ -# Echo Types Prioritized Proof Roadmap -# Based on Stability Analysis (April 2025) - -## Executive Summary - -This roadmap prioritizes proof development based on the stability analysis, focusing first on **immediate high-impact proofs** that will elevate echo types from B+ to A- stability, then progressing to **theoretical maturation**, and finally **exploring advanced applications**. - -## 🎯 Immediate Priorities (Next 6 Weeks) - -### Phase 1: JanusKey Integration Validation (Weeks 1-3) -**Objective**: Prove practical correctness of echo types with JanusKey operations - -#### Priority 1: Echo Witness Preservation Proofs -**File**: `proofs/agda/EchoJanusVerification.agda` - -```agda -module EchoJanusVerification where - -open import EchoJanusBridge -open import Echo -open import JanusKeyOperations -- To be created - --- Core theorem: Echo witnesses enable perfect reversal -echo-witness-preservation : ∀ (op : JanusKeyOp) (s : FileSystem) → - Echo (execute-op op) (op s) → - (undo op (op s) ≡ s) - --- Delete operation (HIGHEST PRIORITY) -echo-witness-preservation (Delete path) s (fs , p) = - -- fs contains the original file content - -- p proves that delete-op path fs ≡ s - -- Need to show: undo (delete-op path) s ≡ fs - ? - --- Create operation -echo-witness-preservation (Create path content) s (fs , p) = - -- fs is the original filesystem (without the file) - -- p proves that create-op path content fs ≡ s - -- Need to show: undo (create-op path content) s ≡ fs - ? - --- Modify operation -echo-witness-preservation (Modify path new-content) s (fs , p) = - -- fs contains original content - -- p proves that modify-op path new-content fs ≡ s - -- Need to show: undo (modify-op path new-content) s ≡ fs - ? - --- Move operation -echo-witness-preservation (Move src dest) s (fs , p) = - -- fs has file at original location - -- p proves that move-op src dest fs ≡ s - -- Need to show: undo (move-op src dest) s ≡ fs - ? -``` - -**Action Plan:** -- [ ] Week 1: Complete Delete operation proof -- [ ] Week 1: Complete Create operation proof -- [ ] Week 2: Complete Modify operation proof -- [ ] Week 2: Complete Move operation proof -- [ ] Week 3: Add comprehensive test cases -- [ ] Week 3: Validate with real JanusKey metadata - -**Success Criteria:** -- All four operation proofs completed -- Test suite with 20+ test cases -- Validation against actual JanusKey operations - -#### Priority 2: Transaction Composition Proof -**File**: `proofs/agda/EchoJanusTransactions.agda` - -```agda -module EchoJanusTransactions where - -open import EchoJanusBridge -open import Data.List using (List; []; _∷_) - --- Transaction as sequence of operations -Transaction : Set -Transaction = List JanusKeyOp - --- Execute transaction sequentially -execute-transaction : Transaction → FileSystem → FileSystem -execute-transaction [] s = s -execute-transaction (op ∷ ops) s = execute-transaction ops (execute-op op s) - --- Main theorem: Echo witnesses compose for transactions -transaction-echo-composition : ∀ {ops : Transaction} {s : FileSystem} → - (∀ op → Echo (execute-op op) (op s)) → - Echo (execute-transaction ops) (execute-sequentially ops s) -transaction-echo-composition [] s _ = s , refl -transaction-echo-composition (op ∷ ops) s witnesses = - let op-witness = witnesses op in - let remaining-witness = λ op' → witnesses op' in - ? -- Need to compose op-witness with transaction-echo-composition ops s remaining-witness -``` - -**Action Plan:** -- [ ] Week 2: Prove base case (empty transaction) -- [ ] Week 3: Prove inductive case (operation + remaining) -- [ ] Week 3: Test with 3-5 operation sequences -- [ ] Week 4: Validate with real transaction logs - -**Success Criteria:** -- Complete formal proof -- Test cases for transactions of length 1-5 -- Validation with actual JanusKey transactions - -### Phase 2: Performance Characterization (Weeks 4-6) -**Objective**: Formalize and validate performance guarantees - -#### Priority 3: Witness Generation Bounds -**File**: `proofs/agda/EchoJanusPerformance.agda` - -```agda -module EchoJanusPerformance where - -open import EchoJanusBridge -open import Data.Nat using (ℕ; _≤_) - --- Size measure for operations -Size : JanusKeyOp → ℕ -Size (Delete path) = length path -Size (Create path content) = length path + length content -Size (Modify path new-content) = length path + length new-content -Size (Move src dest) = length src + length dest - --- Size measure for echo witnesses -WitnessSize : ∀ {op s} → Echo (execute-op op) (op s) → ℕ -WitnessSize (fs , p) = Size fs + proof-size p - --- Main theorem: Witness generation is bounded -echo-generation-bound : ∀ (op : JanusKeyOp) (s : FileSystem) → - (w : Echo (execute-op op) (op s)) → - WitnessSize w ≤ 5 * Size op -- Constant factor 5 -``` - -**Action Plan:** -- [ ] Week 4: Define size measures -- [ ] Week 4: Prove for Delete operation -- [ ] Week 5: Prove for Create operation -- [ ] Week 5: Prove for Modify operation -- [ ] Week 6: Prove for Move operation -- [ ] Week 6: Empirical validation - -**Success Criteria:** -- Formal size bounds for all operations -- Constant factor validated empirically -- Performance documentation updated - -#### Priority 4: Verification Time Complexity -**File**: `proofs/agda/EchoJanusPerformance.agda` (continued) - -```agda --- Time measure for verification -VerificationTime : ∀ {op s} → Echo (execute-op op) (op s) → ℕ -VerificationTime w = ? -- To be defined based on witness structure - --- Main theorem: Verification is linear in witness size -verification-linear : ∀ (w : EchoWitness) → - VerificationTime w ≤ 2 * WitnessSize w -- Linear constant 2 -``` - -**Action Plan:** -- [ ] Week 5: Define verification time measure -- [ ] Week 6: Prove linear bound -- [ ] Week 6: Benchmark actual verification times -- [ ] Week 6: Update performance documentation - -**Success Criteria:** -- Formal linear time proof -- Benchmark data collected -- Performance guarantees documented - -## 📅 6-Week Detailed Schedule - -### Week 1: Foundation -``` -✅ Create EchoJanusVerification.agda -✅ Create EchoJanusTransactions.agda -✅ Create EchoJanusPerformance.agda -✅ Complete Delete operation proof -✅ Complete Create operation proof -✅ Set up test infrastructure -``` - -### Week 2: Core Operations -``` -✅ Complete Modify operation proof -✅ Complete Move operation proof -✅ Prove transaction base case -✅ Start transaction inductive case -✅ Add basic test cases -``` - -### Week 3: Transactions -``` -✅ Complete transaction composition proof -✅ Test transaction sequences -✅ Validate with real JanusKey data -✅ Define size measures -✅ Start performance bounds -``` - -### Week 4: Performance Foundations -``` -✅ Complete size measure definitions -✅ Prove Delete operation bounds -✅ Prove Create operation bounds -✅ Set up benchmarking infrastructure -✅ Collect initial performance data -``` - -### Week 5: Performance Proofs -``` -✅ Prove Modify operation bounds -✅ Prove Move operation bounds -✅ Define verification time measure -✅ Start linear time proof -✅ Collect benchmark data -``` - -### Week 6: Validation and Documentation -``` -✅ Complete linear time proof -✅ Finalize all performance proofs -✅ Comprehensive benchmarking -✅ Update all documentation -✅ Create validation report -✅ Prepare for next phase -``` - -## 🎯 Medium-Term Priorities (Next 3-6 Months) - -### Phase 3: Indexed Echo Types Maturation (Months 2-3) -**Objective**: Elevate indexed echo types from B+ to A- stability - -#### Priority 5: Role Separation -**File**: `proofs/agda/EchoIndexedEnhanced.agda` - -```agda -module EchoIndexedEnhanced where - -open import EchoIndexed - --- Theorem: Different roles cannot interfere -role-separation : ∀ {r1 r2 : Role} {s : FileSystem} → - r1 ≢ r2 → - Echoᵢ r1 s → Echoᵢ r2 s → - (proj₁ (echo1) ≢ proj₁ (echo2)) -``` - -**Action Plan:** -- [ ] Formalize role inequality -- [ ] Prove for audit trail example -- [ ] Add to indexed echo types documentation -- [ ] Create practical examples - -#### Priority 6: Permission Preservation -**File**: `proofs/agda/EchoIndexedEnhanced.agda` - -```agda --- Theorem: Operations preserve permission structures -permission-preservation : ∀ (op : JanusKeyOp) (s : FileSystem) → - Echo (execute-op op) (op s) → - (permissions (op s) ≡ permissions s) -``` - -**Action Plan:** -- [ ] Define permission structure -- [ ] Prove for each operation type -- [ ] Test with complex permission scenarios -- [ ] Document permission model - -### Phase 4: Categorical Semantics (Months 4-5) -**Objective**: Elevate categorical semantics from B to B+ - -#### Priority 7: Functor Laws -**File**: `proofs/agda/EchoCategoricalComplete.agda` - -```agda -module EchoCategoricalComplete where - -open import EchoCategorical - --- Theorem: Echo types form a functor -echo-functor-laws : IsFunctor EchoFunctor where - identity = {!!} - composition = {!!} -``` - -**Action Plan:** -- [ ] Prove identity law -- [ ] Prove composition law -- [ ] Add functor examples -- [ ] Document categorical properties - -#### Priority 8: Monad Instance -**File**: `proofs/agda/EchoCategoricalComplete.agda` - -```agda --- Theorem: Echo types form a monad -echo-monad : IsMonad EchoMonad where - return = echo-intro - bind = {!!} -``` - -**Action Plan:** -- [ ] Define bind operation -- [ ] Prove monad laws -- [ ] Add practical monad examples -- [ ] Document monadic usage patterns - -## 🔮 Long-Term Priorities (6-12 Months) - -### Phase 5: Distributed Reversibility (Months 6-8) -**Objective**: Extend echo types to distributed systems - -#### Priority 9: Distributed Echo Consistency -```agda -distributed-echo-consistency : ∀ {N} → (nodes : Fin N → NodeState) → - (op : DistributedOp) → - Echo (distributed-execute op) (final-state nodes) -``` - -#### Priority 10: Network Partition Recovery -```agda -network-partition-recovery : ∀ {op} → - Echo op s → - (∃ s' , recover-from-partition op s ≡ s') -``` - -### Phase 6: Resource-Bounded Reversibility (Months 9-10) -**Objective**: Prove reversibility under constraints - -#### Priority 11: Storage Bounds -```agda -bounded-storage-reversibility : ∀ (quota : ℕ) → - (op : BoundedOp quota) → - Echo (execute-op op) (op s) × - (storage-used (undo op) ≤ quota) -``` - -#### Priority 12: Time Bounds -```agda -time-bounded-reversibility : ∀ (timeout : ℕ) → - (op : BoundedOp timeout) → - Echo (execute-op op) (op s) × - (verification-time (undo op) ≤ timeout) -``` - -### Phase 7: Advanced Applications (Months 11-12) -**Objective**: Explore experimental extensions - -#### Priority 13: CRDT Integration -```agda -crdt-echo-correspondence : ∀ {C : CRDT} → - (op : CRDTOp C) → - Echo (crdt-apply op) (crdt-state-after op) -``` - -#### Priority 14: Transaction Isolation -```agda -serializable-reversibility : ∀ {txn : Transaction} → - Serializable txn → - Echo (execute-txn txn) (final-state txn) -``` - -## 📊 Progress Tracking - -### Current Status (April 2025) -| Priority | Area | Current Stability | Target Stability | Status | -|----------|------|-------------------|-------------------|---------| -| 1-2 | JanusKey Integration | B+ | A- | ⏳ In Progress | -| 3-4 | Performance | C+ | B+ | ⏳ Planned | -| 5-6 | Indexed Types | B+ | A- | ⏳ Planned | -| 7-8 | Categorical | B | B+ | ⏳ Planned | -| 9-10 | Distributed | C | B | ⏳ Future | -| 11-12 | Bounded | C | B | ⏳ Future | -| 13-14 | Advanced | C | B | ⏳ Future | - -### Target Milestones -| Date | Milestone | Stability Target | -|------|-----------|-------------------| -| Jun 2025 | JanusKey integration complete | A- | -| Aug 2025 | Performance proofs complete | B+ | -| Oct 2025 | Indexed types matured | A- | -| Dec 2025 | Categorical semantics complete | B+ | -| Feb 2026 | Distributed proofs started | C+ | -| Apr 2026 | Bounded reversibility proofs | B | -| Jun 2026 | Advanced applications explored | B | - -## 🔧 Implementation Resources - -### Required Files to Create -1. `proofs/agda/EchoJanusVerification.agda` - Core validation proofs -2. `proofs/agda/EchoJanusTransactions.agda` - Transaction composition -3. `proofs/agda/EchoJanusPerformance.agda` - Performance guarantees -4. `proofs/agda/EchoIndexedEnhanced.agda` - Enhanced indexed types -5. `proofs/agda/EchoCategoricalComplete.agda` - Complete categorical semantics - -### Supporting Infrastructure -1. `tests/` - Test suite directory -2. `benchmarks/` - Performance measurement tools -3. `docs/examples/` - Practical examples directory - -### Recommended Tools -- **Agda 2.6.2+** - For proof development -- **agda-stdlib** - Standard library dependencies -- **criterion.rs** - Rust benchmarking (for JanusKey) -- **quickcheck** - Property-based testing - -## 🎯 Strategic Impact - -### Short-Term (6 Weeks) -- **JanusKey Integration**: Production-ready with formal proofs -- **Performance Guarantees**: Documented and validated -- **Stability Rating**: B+ → A- for core applications - -### Medium-Term (6 Months) -- **Theoretical Maturity**: Indexed and categorical semantics at B+/A- -- **Practical Validation**: Real-world tested and benchmarked -- **Ecosystem Readiness**: Ready for broader adoption - -### Long-Term (12 Months) -- **Advanced Applications**: Distributed, bounded, CRDT extensions -- **Unified Theory**: Comprehensive reversibility framework -- **Industry Adoption**: Production use in multiple systems - -## 📋 Getting Started Checklist - -### Week 1 Actions -- [ ] Create `EchoJanusVerification.agda` -- [ ] Implement Delete operation proof -- [ ] Implement Create operation proof -- [ ] Set up test infrastructure -- [ ] Create basic test cases - -### Week 2 Actions -- [ ] Implement Modify operation proof -- [ ] Implement Move operation proof -- [ ] Start transaction composition proof -- [ ] Add transaction test cases -- [ ] Begin performance measure definitions - -### Week 3 Actions -- [ ] Complete transaction composition proof -- [ ] Validate with real JanusKey data -- [ ] Prove Delete operation bounds -- [ ] Prove Create operation bounds -- [ ] Set up benchmarking - -## Conclusion - -This prioritized proof roadmap provides a **clear, actionable plan** to systematically improve echo types' stability from B+ to A- over the next 6 months. By focusing first on **JanusKey integration validation**, then **performance characterization**, and progressing to **theoretical maturation**, we ensure both **practical impact** and **theoretical rigor**. - -The roadmap balances **immediate practical needs** with **long-term theoretical development**, ensuring echo types remain at the forefront of formal reversibility research while delivering real-world value to systems like JanusKey. \ No newline at end of file diff --git a/docs/ProofRoadmap.md b/docs/ProofRoadmap.md deleted file mode 100644 index 87151e8..0000000 --- a/docs/ProofRoadmap.md +++ /dev/null @@ -1,184 +0,0 @@ -# Echo Types - JanusKey Proof Roadmap - -## Strategic Proof Priorities - -### Tier 1: Foundational Proofs (Immediate Impact) - -#### 1. **Formal Verification of JanusKey Rust Implementation** -**Goal**: Prove that JanusKey's Rust code correctly implements the echo type specifications -**Approach**: -- Extract formal specifications from `EchoJanusBridge.agda` -- Create Rust verification targets using formal methods (e.g., Prusti, Creusot) -- Prove correspondence between Rust operations and Agda echo types -**Impact**: Closes the gap between theory and practice, validates real-world implementation - -#### 2. **Distributed Reversibility Proof** -**Goal**: Extend echo types to distributed file systems with network partitions -**Theorems to Prove**: -```agda -distributed-echo-consistency : ∀ {N} → (nodes : Fin N → NodeState) → - (op : DistributedOp) → - Echo (distributed-execute op) (final-state nodes) -distributed-undo-commutativity : ∀ {op1 op2} → - Echo op1 s1 → Echo op2 s2 → - undo op1 ∘ undo op2 ≡ undo op2 ∘ undo op1 -``` -**Impact**: Enables JanusKey distributed mode with mathematical guarantees - -#### 3. **Resource-Bounded Reversibility** -**Goal**: Prove reversibility under storage/memory constraints -**Theorems to Prove**: -```agda -bounded-storage-reversibility : ∀ (quota : ℕ) → - (op : BoundedOp quota) → - (s : FileSystem) → - Echo (execute-op op) (op s) × - (storage-used (undo op) ≤ quota) -``` -**Impact**: Addresses practical concerns about reversal costs - -### Tier 2: Advanced Theoretical Proofs - -#### 4. **Temporal Logic of Reversible Operations** -**Goal**: Develop temporal logic semantics for echo types -**Theorems to Prove**: -```agda -□-reversible : ∀ {op} → (□ (Echo op s)) → (□ (∃ s' , undo op s ≡ s')) -⋄-reversible : ∀ {op} → (⋄ (Echo op s)) → (⋄ (∃ s' , undo op s ≡ s')) -``` -**Impact**: Enables formal reasoning about operation sequences over time - -#### 5. **Categorical Semantics of Echo Types** -**Goal**: Show echo types form a category with reversible operations as morphisms -**Theorems to Prove**: -```agda -echo-category : Category EchoCat where - Ob = FileSystem - Hom A B = Echo (some-op) B -- Morphisms are echo witnesses - id = echo-intro id - _∘_ = map-over -``` -**Impact**: Provides higher-level abstraction for compositional reasoning - -#### 6. **Graded Modal Types for Permissions** -**Goal**: Extend echo types with permission grading (read/write/execute) -**Theorems to Prove**: -```agda -permission-preserving-echo : ∀ {p} {op : PermissionAwareOp p} → - Echo op s → - (permissions (undo op s) ≡ permissions s) -``` -**Impact**: Enables fine-grained access control with reversibility guarantees - -### Tier 3: Applied Proofs - -#### 7. **Transaction Isolation Levels** -**Goal**: Prove reversibility at different isolation levels (Serializable, Repeatable Read, etc.) -**Theorems to Prove**: -```agda -serializable-reversibility : ∀ {txn : Transaction} → - Serializable txn → - Echo (execute-txn txn) (final-state txn) -``` -**Impact**: Enables JanusKey to offer different consistency guarantees - -#### 8. **Conflict-Free Replicated Data Types (CRDTs)** -**Goal**: Show echo types can model CRDT reversibility -**Theorems to Prove**: -```agda -crdt-echo-correspondence : ∀ {C : CRDT} → - (op : CRDTOp C) → - Echo (crdt-apply op) (crdt-state-after op) -``` -**Impact**: Enables collaborative editing with reversibility - -#### 9. **Quantum-Inspired Reversibility** -**Goal**: Explore connections with quantum computing reversibility -**Theorems to Prove**: -```agda -unitary-echo-correspondence : ∀ {U : UnitaryMatrix} → - Echo (quantum-apply U) (quantum-state-after U) -``` -**Impact**: Future-proofs for quantum computing applications - -### Tier 4: Cross-Domain Proofs - -#### 10. **MAA Framework Integration** -**Goal**: Connect echo types with MAA's reversibility proofs -**Theorems to Prove**: -```agda -maa-echo-equivalence : ∀ {p : MAAProgram} → - MAAReversible p → - (∀ σ → Echo (maa-execute p) (p σ)) -``` -**Impact**: Unifies formal verification efforts across the ecosystem - -#### 11. **Absolute Zero CNO Integration** -**Goal**: Show CNOs (Certified Null Operations) are special cases of echo types -**Theorems to Prove**: -```agda -cno-as-echo-subcategory : CNO-Category → Subcategory Echo-Category -``` -**Impact**: Creates unified theory of null/reversible operations - -#### 12. **Homotopy Type Theory Extension** -**Goal**: Develop higher-dimensional echo types -**Theorems to Prove**: -```agda -homotopy-echo : ∀ {A B} (f : A → B) (y : B) → - Echo f y → (x : A) → (f x ≡ y) → (x ≡ proj₁ (echo-witness)) -``` -**Impact**: Enables proof-relevant reversibility reasoning - -## Proof Development Strategy - -### Phase 1: Implementation Verification (3-6 months) -- Focus on Tier 1 proofs #1-3 -- Develop Rust verification infrastructure -- Create test suites linking Agda specs to Rust code - -### Phase 2: Theoretical Deepening (6-12 months) -- Pursue Tier 2 proofs #4-6 -- Develop categorical and temporal semantics -- Publish academic papers on results - -### Phase 3: Applied Extensions (12-18 months) -- Implement Tier 3 proofs #7-9 -- Develop practical applications (distributed systems, CRDTs) -- Create demo applications showing real-world impact - -### Phase 4: Ecosystem Integration (18-24 months) -- Complete Tier 4 proofs #10-12 -- Integrate with MAA Framework and Absolute Zero -- Develop unified theory of reversibility - -## Resource Requirements - -### Human Resources: -- 1-2 formal methods experts (Agda/Coq) -- 1 Rust verification specialist -- 1 category theory expert -- 1 distributed systems researcher - -### Technical Resources: -- Formal verification tools (Agda, Coq, Prusti) -- Theorem prover integration -- Test infrastructure for Rust verification -- Documentation and visualization tools - -## Expected Outcomes - -1. **Theoretical Advancement**: Echo types become recognized framework for reversibility -2. **Practical Validation**: JanusKey achieves formal verification of its core claims -3. **Ecosystem Growth**: Unified approach to reversibility across MAA projects -4. **Academic Impact**: Publications in top PL/verification conferences -5. **Industry Adoption**: Formal methods for reversible systems gain traction - -## Risk Mitigation - -- **Complexity Risk**: Start with simplest proofs first, build complexity gradually -- **Tooling Risk**: Use multiple verification approaches (Agda + Rust verification) -- **Integration Risk**: Develop clear interfaces between components -- **Performance Risk**: Profile verification overhead early - -This roadmap provides a comprehensive strategy for enhancing both echo types' theoretical standing and JanusKey's practical reality through systematic proof development. \ No newline at end of file diff --git a/docs/WORK_PLAN.md b/docs/WORK_PLAN.md deleted file mode 100644 index 662cbed..0000000 --- a/docs/WORK_PLAN.md +++ /dev/null @@ -1,323 +0,0 @@ -# Echo Types Work Plan (Based on Stability Analysis) - -## Guiding Principles - -1. **Stabilize the Core**: Ensure A-rated components remain production-ready -2. **Maturity the Middle**: Elevate B-rated components to A- status -3. **Explore the Edges**: Responsibly develop C-rated experimental areas -4. **Validate in Practice**: Connect theory to real-world implementations - -## Priority Work Areas (3-6 Months) - -### 🔥 High Priority: Stabilize B+ Components - -#### 1. JanusKey Bridge Maturation -**Goal**: Elevate from B+ to A- stability - -**Specific Tasks:** -- [ ] **Integration Testing**: Create comprehensive test suite - ```agda - -- Test echo witness preservation across operations - echo-witness-preservation-test : ∀ (op : JanusKeyOp) → - Echo op s → - (undo op (op s) ≡ s) - ``` -- [ ] **Performance Benchmarking**: Establish baseline metrics - - Measure echo witness generation time - - Profile verification overhead - - Document performance characteristics - -- [ ] **Real-World Validation**: Test with actual JanusKey operations - - Create test corpus of file operations - - Verify echo witnesses match real metadata - - Validate undo operations work correctly - -**Success Criteria:** -- 98% test coverage -- Documented performance profile -- Validated with 100+ real operations - -#### 2. Indexed Echo Types Refinement -**Goal**: Elevate from B+ to A- stability - -**Specific Tasks:** -- [ ] **Additional Examples**: Add practical use cases - ```agda - -- Audit trail example with role separation - audit-trail-example : Echoᵢ Role trace-role trace-visible auditor true - ``` -- [ ] **Generalization Analysis**: Identify potential abstractions -- [ ] **Documentation Expansion**: Add user guide section - -**Success Criteria:** -- 3+ new practical examples -- Clear generalization boundaries identified -- Comprehensive user documentation - -### 🎯 Medium Priority: Strengthen B Components - -#### 3. Categorical Semantics Development -**Goal**: Elevate from B to B+ stability - -**Specific Tasks:** -- [ ] **Functor Laws Verification**: Formal proof of functoriality - ```agda - echo-functor-laws : IsFunctor EchoFunctor - ``` -- [ ] **Monad Instance**: Complete monadic structure - ```agda - echo-monad : IsMonad EchoMonad - ``` -- [ ] **Adjunction Proofs**: Formalize relationships with other categories - -**Success Criteria:** -- Complete functor proof -- Working monad instance -- 2+ adjunction examples - -#### 4. Relational Semantics Enhancement -**Goal**: Elevate from B to B+ stability - -**Specific Tasks:** -- [ ] **Additional Examples**: More step semantics cases -- [ ] **Composition Theorems**: Prove compositional properties - ```agda - relational-composition : ∀ {s1 s2 s3} → - Step s1 s2 → Step s2 s3 → Step s1 s3 - ``` -- [ ] **Integration Guide**: How to use in practice - -**Success Criteria:** -- 5+ new examples -- Composition theorems proven -- Practical integration guide - -### 🧪 Low Priority: Explore C Components - -#### 5. Thermodynamic Models (Research) -**Goal**: Assess feasibility and potential - -**Specific Tasks:** -- [ ] **Literature Review**: Connect with existing thermodynamic computing -- [ ] **Energy Bounds**: Formalize practical limits - ```agda - energy-bound : ∀ (op : Operation) → - Energy op ≤ ThermodynamicLimit op - ``` -- [ ] **Feasibility Assessment**: Determine if worth pursuing - -**Success Criteria:** -- Literature survey completed -- Basic energy bounds formalized -- Go/no-go decision on further development - -## Implementation Strategy - -### Phase 1: Foundation (Weeks 1-4) -**Focus**: Set up infrastructure for validation - -**Tasks:** -1. **Test Infrastructure**: Create Agda test framework -2. **Benchmarking Setup**: Performance measurement tools -3. **Documentation Template**: Standard format for new materials -4. **CI Integration**: Add proof checking to pipeline - -**Deliverables:** -- Working test framework -- Performance benchmarking tools -- Documentation templates -- CI pipeline updates - -### Phase 2: Core Stabilization (Weeks 5-12) -**Focus**: JanusKey bridge and indexed types - -**Tasks:** -1. **JanusKey Integration Tests**: Comprehensive test suite -2. **Performance Profiling**: Baseline metrics -3. **Indexed Type Examples**: Practical use cases -4. **Real-World Validation**: Test with actual operations - -**Deliverables:** -- 98% test coverage for JanusKey bridge -- Performance documentation -- 3+ new indexed type examples -- Validation report - -### Phase 3: Theory Maturation (Weeks 13-20) -**Focus**: Categorical and relational semantics - -**Tasks:** -1. **Functor Laws**: Complete formal proofs -2. **Monad Instance**: Working implementation -3. **Relational Examples**: Expanded case studies -4. **Composition Theorems**: Formal proofs - -**Deliverables:** -- Complete functor proof -- Working monad instance -- 5+ new relational examples -- Composition theorem proofs - -### Phase 4: Exploration (Weeks 21-24) -**Focus**: Experimental areas assessment - -**Tasks:** -1. **Thermodynamic Literature Review**: State of the art -2. **Energy Bound Formalization**: Basic theorems -3. **Feasibility Report**: Recommendations -4. **Roadmap Update**: Based on findings - -**Deliverables:** -- Literature survey document -- Basic energy bound proofs -- Feasibility assessment -- Updated roadmap - -## Resource Allocation - -### Human Resources (3-6 Months) -- **1 Senior Researcher**: Theory development (categorical, relational) -- **1 Formal Methods Engineer**: Testing, verification, CI integration -- **1 Documentation Specialist**: Examples, guides, tutorials -- **0.5 Performance Engineer**: Benchmarking and optimization - -### Time Allocation -- **40%**: JanusKey bridge stabilization (highest priority) -- **30%**: Theory maturation (categorical, relational) -- **20%**: Infrastructure and tooling -- **10%**: Experimental exploration - -## Success Metrics - -### Quantitative Goals -| Metric | Current | Target (6 months) | -|--------|---------|-------------------| -| Test Coverage | 40% | 95% | -| Proof Coverage | 85% | 98% | -| Documentation Completeness | 90% | 99% | -| Performance Data | Limited | Comprehensive | -| Real-World Validation | None | 100+ operations | - -### Qualitative Goals -1. **JanusKey Integration**: Seamless connection between theory and practice -2. **Theory Maturity**: Clear, well-documented mathematical foundations -3. **Developer Experience**: Easy to understand and extend -4. **Ecosystem Readiness**: Prepared for broader adoption - -## Risk Management - -### Risk: Theory-Practice Gap -**Mitigation:** -- Early and frequent validation with real operations -- Continuous feedback from JanusKey developers -- Iterative refinement based on practical findings - -### Risk: Proof Complexity -**Mitigation:** -- Modular proof development -- Clear documentation of proof patterns -- Automated verification where possible - -### Risk: Performance Overhead -**Mitigation:** -- Early benchmarking -- Optimization strategies identified -- Trade-off analysis documented - -### Risk: Scope Creep -**Mitigation:** -- Clear prioritization (A → B → C components) -- Time-boxed exploration phases -- Regular progress reviews - -## Decision Points - -### Month 3: JanusKey Validation -**Decision**: Continue full integration vs. targeted use cases -**Criteria**: Test results, performance metrics, developer feedback - -### Month 5: Theory Maturation -**Decision**: Pursue formal publication vs. internal documentation -**Criteria**: Proof completeness, novelty, academic interest - -### Month 6: Experimental Areas -**Decision**: Invest in thermodynamic models vs. other extensions -**Criteria**: Feasibility, potential impact, resource availability - -## Integration Plan - -### With JanusKey -1. **Immediate**: Use echo types for core operation verification -2. **Short-term**: Integrate into transaction system -3. **Long-term**: Full formal verification of Rust implementation - -### With MAA Framework -1. **Immediate**: Document connection points -2. **Short-term**: Create integration examples -3. **Long-term**: Unified reversibility theory - -### With Absolute Zero -1. **Immediate**: Leverage CNO bridge -2. **Short-term**: Joint proof development -3. **Long-term**: Unified formal methods approach - -## Communication Strategy - -### Internal -- **Weekly**: Progress updates -- **Monthly**: Technical deep dives -- **Quarterly**: Strategy reviews - -### External -- **Blog Posts**: Theory explanations, practical guides -- **Conference Talks**: Academic and industry venues -- **Documentation**: Comprehensive, up-to-date, accessible - -## Timeline - -``` -Month 1: Infrastructure Setup -Month 2: JanusKey Testing Framework -Month 3: Performance Benchmarking -Month 4: Indexed Types Examples -Month 5: Categorical Semantics -Month 6: Relational Enhancements & Assessment -``` - -## Budget Estimate - -### Personnel (6 months) -- Senior Researcher: $60,000 -- Formal Methods Engineer: $45,000 -- Documentation Specialist: $30,000 -- Performance Engineer: $15,000 -- **Total Personnel**: $150,000 - -### Tools & Infrastructure -- Agda/Coq licenses: $5,000 -- CI/CD pipeline: $3,000 -- Benchmarking tools: $2,000 -- **Total Tools**: $10,000 - -### Travel & Conferences -- Conference presentations: $7,000 -- Team workshops: $3,000 -- **Total Travel**: $10,000 - -### Contingency (15%) -- **Contingency**: $25,500 - -### **Total Budget**: $195,500 - -## Conclusion - -This work plan provides a **clear, prioritized approach** to maturing echo types based on the stability analysis. By focusing first on **stabilizing the B+ components** (especially JanusKey integration), then **strengthening the B components**, and finally **exploring the C components**, we can systematically improve the overall stability rating from B+ to A-. - -The plan balances **theoretical rigor** with **practical validation**, ensuring that echo types remain both **mathematically sound** and **practically useful**. Regular checkpoints and decision points allow for **adaptive management** while maintaining focus on the highest-impact areas. - -**Expected Outcome**: In 6 months, echo types will have: -- Production-ready JanusKey integration (A- stability) -- Matured theoretical extensions (B+ stability) -- Clear path forward for experimental areas -- Comprehensive documentation and validation -- Strong foundation for broader ecosystem adoption \ No newline at end of file diff --git a/docs/bridges/ECHO-CNO-BRIDGE.adoc b/docs/bridges/ECHO-CNO-BRIDGE.adoc index 70cc7c3..a339f8e 100644 --- a/docs/bridges/ECHO-CNO-BRIDGE.adoc +++ b/docs/bridges/ECHO-CNO-BRIDGE.adoc @@ -110,7 +110,7 @@ but that is a witness-presence statement, not an information-preservation statement. A real Shannon-entropy / mutual-information formalisation is open -work; see `docs/echo-types/roadmap.md` under the thermodynamic +work; see `roadmap.adoc` under the deferred research / thermodynamic items. ### Theorem 6: Universal CNO Definition (NEW) @@ -413,7 +413,7 @@ kill condition**: a mechanised proof that clauses (i)∧(ii) ⊢ ⊥. (`collapse-cost-impossible`), a settled boundary, no open obligation remains for this Direction. 3. **Information Theory**: not bridged. Open work — see - `docs/echo-types/roadmap.md`. + `roadmap.adoc` (deferred research track). ## Practical Implications diff --git a/docs/bridges/tropical-correspondence.md b/docs/bridges/tropical-correspondence.md index 472235f..664a1b4 100644 --- a/docs/bridges/tropical-correspondence.md +++ b/docs/bridges/tropical-correspondence.md @@ -84,8 +84,8 @@ not constitute a unified verification artefact. It closes the grading* (`grade : Session → Tropical` in Lean), which is the symmetric Agda-exclusive direction. - **Long-game alignment target.** When the echo-types ordinal track - reaches Bachmann–Howard (ψ₀(Ω_ω); see `docs/echo-types/roadmap.md` - and `buchholz-plan.adoc`), the adjacent repo's + reaches Bachmann–Howard (ψ₀(Ω_ω); see `roadmap.adoc` §Lane 3 and + `docs/buchholz-plan.adoc`), the adjacent repo's `Tropical_Ordinal_Bridge.thy` becomes the natural cross-repo alignment target (Agda Buchholz BT ↔ Isabelle `tropO` carrier). This target is **firewalled** until the ordinal track lands the diff --git a/docs/characteristic.adoc b/docs/characteristic.adoc index 0ae6b56..64980cf 100644 --- a/docs/characteristic.adoc +++ b/docs/characteristic.adoc @@ -29,6 +29,13 @@ at integration time. == Inherited spec +For the sceptic-facing evidence map ("is this just renamed Σ?", +organised under five demands and cross-linked to every in-tree +artefact), see `docs/echo-types/sigma-distinctness-map.adoc` and its +internal companion `core/skepticisms/is-this-just-sigma-types.md`. +That doc is an evidence index; this file is the per-nominee Gate 2 +audit and remains the authoritative gate artefact. + `roadmap-gates.adoc` Gate 2: .Claim diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index dd3665a..32735c3 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -83,7 +83,7 @@ the standing B- freeze lifted because O-THERMO-∞ is now discharged `proofs/agda/EchoThermodynamicsArbitrary.agda`, `proofs/agda/EchoThermoCollapseImpossible.agda`. * Docs: `docs/ECHO-CNO-BRIDGE.adoc` §"Thermodynamic Bridge", - `docs/STABILITY_ANALYSIS.md` §3.3, `docs/WORK_PLAN.md` §5, + `docs/STABILITY_ANALYSIS.md` §3.3, `docs/adjacency/hott-fibers.adoc`. * Build: `just test-thermo`. @@ -141,7 +141,7 @@ Connect echo types with MAA's reversibility proofs (`maa-echo-equivalence`). absolute-zero lives under `…/verification-ecosystem/maa-framework/`. Planned, not built. -* Docs: `docs/ProofRoadmap.md` §10, `docs/EchoJanusBridge.md`. +* Docs: `roadmap.adoc` §"Deferred research track", `docs/EchoJanusBridge.md`. === Shannon / information theory `[OPEN]` Explicitly *not bridged*. The Transport / Nyquist sampling work @@ -197,10 +197,11 @@ are kept for history and **may overclaim** (pre-retraction). | `INDEX.adoc` is the *audit* index (different role; keep) | Proof status / roadmap -| `docs/echo-types/earn-back-plan.adoc` + `docs/retractions.adoc` -| `ProofRoadmap.md`, `PRIORITIZED_PROOF_ROADMAP.md`, `WORK_PLAN.md`, - `roadmap.adoc`, `roadmap-gates.adoc`, `docs/echo-types/roadmap.md` - (pre-R-2026-05-18 — historical) +| `roadmap.adoc` (single canonical roadmap; lanes, gates, deferred + research) + `docs/echo-types/earn-back-plan.adoc` + + `docs/retractions.adoc` +| `roadmap-gates.adoc` (pre-R-2026-05-18 — historical; folded into + `roadmap.adoc`) | Concept / definition | `docs/echo-types/overview.md`, `docs/echo-types/paper.adoc` diff --git a/docs/echo-types/applications-compiler-analysis.adoc b/docs/echo-types/applications-compiler-analysis.adoc index c66f59b..237e6bf 100644 --- a/docs/echo-types/applications-compiler-analysis.adoc +++ b/docs/echo-types/applications-compiler-analysis.adoc @@ -318,5 +318,5 @@ be expanded to a fully worked Agda exhibit: exhibiting tolerance accumulation through `echo-approx-compose`. -Both are tracked as `[unblocked]` items in `roadmap.md` +Both are tracked in `roadmap.adoc` as deferred examples-library work (`Add example-library Agda files matching examples.md`). diff --git a/docs/echo-types/decisions/gate1-adjacency-refresh.adoc b/docs/echo-types/decisions/gate1-adjacency-refresh.adoc index dcdc897..488583b 100644 --- a/docs/echo-types/decisions/gate1-adjacency-refresh.adoc +++ b/docs/echo-types/decisions/gate1-adjacency-refresh.adoc @@ -6,7 +6,7 @@ :icons: font [.lead] -Coherence pass requested by `roadmap.md` § "Theory work" item +Coherence pass requested by the legacy `roadmap.md` (now consolidated into `roadmap.adoc`) § "Theory work" item "Gate 1 adjacency refresh: the five existing adjacency notes predate the taxonomy. Cross-check each against the current axes and flag any neighbour whose identity claim should be @@ -291,12 +291,12 @@ are coherence-flavoured and can be batched: * No content rewrites scheduled in this PR; the coherence follow-ups (per-note one-liner, README refresh) are listed above as separate optional moves. -* `roadmap.md` § "Theory work" entry updated from `[unblocked]` +* the legacy `roadmap.md` (now consolidated into `roadmap.adoc`) § "Theory work" entry updated from `[unblocked]` to `[refreshed — see decisions/gate1-adjacency-refresh.adoc]`. == Cross-references -* `docs/echo-types/roadmap.md` — Theory-work entry updated to +* `roadmap.adoc` (legacy `docs/echo-types/roadmap.md` consolidated 2026-05-26) — Theory-work entry updated to `[refreshed]`. * `docs/echo-types/taxonomy.md` — the eight-axis post-2026-05 taxonomy this refresh cross-checks against. diff --git a/docs/echo-types/decisions/no-2-cat.adoc b/docs/echo-types/decisions/no-2-cat.adoc index 60c69e3..df3839a 100644 --- a/docs/echo-types/decisions/no-2-cat.adoc +++ b/docs/echo-types/decisions/no-2-cat.adoc @@ -6,7 +6,7 @@ :icons: font [.lead] -Closure note for the `roadmap.md` entry +Closure note for the `roadmap.adoc` entry "2-categorical shape: commit to a 2-category or rule it out" and for `composition.md` §Q1 / §Q6. The verdict is *rule out*, on argued grounds against the landed Pillars A–D evidence. The @@ -115,7 +115,7 @@ None is on the active roadmap. The verdict stands. == Cross-references -* `docs/echo-types/roadmap.md` — Theory-work entry updated to +* `roadmap.adoc` — Theory-work entry updated to `[ruled out]`. * `docs/echo-types/composition.md` §Q1 / §Q4 / §Q6 — open framings folded into this closure. diff --git a/docs/echo-types/decisions/presentation-dependence.adoc b/docs/echo-types/decisions/presentation-dependence.adoc index 029dc00..66ce29e 100644 --- a/docs/echo-types/decisions/presentation-dependence.adoc +++ b/docs/echo-types/decisions/presentation-dependence.adoc @@ -6,7 +6,7 @@ :icons: font [.lead] -Closure note for the `roadmap.md` entry +Closure note for the the legacy `roadmap.md` (now consolidated into `roadmap.adoc`) entry "Presentation-dependence sub-theory: examples 5, 9, 10 cluster here; write up the common pattern". The verdict is *meta-pattern only — no new Agda module needed*: presentation-dependence is the existing @@ -196,7 +196,7 @@ Concretely: == Cross-references -* `docs/echo-types/roadmap.md` — Theory-work entry updated to +* `roadmap.adoc` (legacy `docs/echo-types/roadmap.md` consolidated 2026-05-26) — Theory-work entry updated to `[landed — see decisions/presentation-dependence.adoc]`. * `docs/echo-types/taxonomy.md` §Axis 4 — the existing axis this cluster instantiates; its "Open question" is sharpened (not diff --git a/docs/echo-types/establishment-plan.adoc b/docs/echo-types/establishment-plan.adoc index bdab053..24ad45b 100644 --- a/docs/echo-types/establishment-plan.adoc +++ b/docs/echo-types/establishment-plan.adoc @@ -8,7 +8,7 @@ [.lead] This document sets out the path by which "echo types" can acquire *recognised type-theoretic standing*. It is deliberately separate from -`roadmap.md` (work partitioned by bottleneck) and `roadmap-gates.adoc` +`roadmap.adoc` (work partitioned by lane) and `roadmap-gates.adoc` (the falsifiable identity claim). This document answers a different question: _given_ the gated identity claim, what makes a construction like this *established* in the sense that linear, dependent, or graded @@ -223,7 +223,7 @@ programme is done; only Pillar E (external validation) remains.* A–C were the credibility core and needed no external unblocker. The ordinal / Buchholz track is impressive _consumer evidence_, not foundation — keep it -firewalled from the identity claim exactly as `roadmap.md` already does. +firewalled from the identity claim exactly as `roadmap.adoc` already does. *Hard guardrails (credibility hazards):* diff --git a/docs/echo-types/roadmap.md b/docs/echo-types/roadmap.md deleted file mode 100644 index 9a81d7e..0000000 --- a/docs/echo-types/roadmap.md +++ /dev/null @@ -1,431 +0,0 @@ -# Echo Types — Roadmap - -**Status:** planning document. Partitions work by dependency on the -two identified bottlenecks: - -For current cross-repo progress snapshots, see -`cross-repo-bridge-status.md`. - -- **Bottleneck B1 (RECAST 2026-05-20).** The remaining gap between - the closed Veblen/current-core route and the full intended - Buchholz order: the historically blocked shared-binder shapes in - `_<ᵇ_`. `wf-<ᵇ` is landed for the currently admitted core; the - shared-binder shapes (`<ᵇ⁺-ψα`, `<ᵇ⁺-+2`) now have a *budgeted* - WF carrier in `Ordinal.Buchholz.OrderExtendedBudget.wf-<ᵇ⁺ᵇ` - (mirroring the existing `wf-<ᵇʳᶠᵇ` for the recursive surface). - **The unbudgeted promotion is structurally impossible** for the - current `_<ᵇ_` — see `buchholz-rank-obstruction.adoc`. The - Echidna-SA-recommended rank-into-Brouwer route fails on the - ordinally-unsound `<ᵇ-+Ω` constructor; all four alternative - routes (direct mutual structural recursion, tower-stratification, - lex measure into ℕ, inverse-image into the budgeted relation) are - also walled. Recovering unbudgeted WF requires either restricting - `_<ᵇ_` to a `WellFormed` subset (2–3 weeks of constructor-by- - constructor rework) or providing a non-additive denotational - measure (essentially solving Buchholz WF "from the model up"). - The "B1" framing is therefore now: *accept the budgeted forms as - canonical*, or *commit to one of the two substantial paths*. -- **Bottleneck B2.** Tool-scope limitations on adjacent repos - (`maa-framework/absolute-zero`, `januskey`, - `tropical-resource-typing`). Blocks end-to-end bridge audits. - -Paths marked **[unblocked]** can proceed today. Paths marked -**[gated on B1]** or **[gated on B2]** cannot. - ---- - -## Theory work — no proof assistant needed - -- **[landed]** Axis 2 (approximate echoes): formal definition, - distinguishing test, examples, and composition theorem all in - `taxonomy.md` §2 (lines 38–64). `EchoApprox.agda` ships - `EchoR ε f y`, three headline lemmas (`echo-approx-intro`, - `echo-approx-relax`, `echo-approx-compose`). Pinned in - `Smoke.agda`. Compiler-analysis widening application worked in - `applications-compiler-analysis.adoc` example 2. -- **[landed]** Axis 8 (information-theoretic vs computational - access): promoted from the candidates list to a numbered axis. - Every candidate refinement is now mechanised. Decidability- - respecting: `proofs/agda/EchoDecidable.agda`. Cost-indexed (over - an abstract `CostAlgebra`): `EchoCost.agda` + `EchoCostInstance.agda` - (PR #85). Graded access modality: `EchoAccess.agda` (PRs #68 + - #75). Witness-search abstract machine: `EchoSearch.agda` + - `EchoSearchInstance.agda` (PR #80). See `taxonomy.md` §8. -- **[landed]** Negative / co-echoes: `AntiEcho f y := Σ A (λ x → f x ≢ y)` - shipped as `proofs/agda/AntiEcho.agda` (PR #69) with - `antiecho-{intro, disjoint, map-over}`, plus per-element - classification `antiecho-partition-dec` (PR #90, closes - `coecho.md` §5 obligation 5). Distinct from `EchoFiberTriangulation.CoEcho` - (which is the trivial opposite-orientation fibre); see naming - rationale in `AntiEcho.agda`'s preamble. The tropical decomposition - `TropEcho y ↔ Echo score y × (∀ z → y ≤ score z)` lands at the - concrete ℕ-scored level in `AntiEchoTropical.agda` (PR #72) and at - an abstract `OrderedCodomain` interface in `AntiEchoTropicalGeneric.agda` - (PR #91, closes `coecho.md` §5 obligation 6). -- **[ruled out — see docs/echo-types/decisions/no-2-cat.adoc]** - 2-categorical shape. Every would-be 2-cell in the landed code - is `refl` or forced trivial by propositionality (`≤g-prop`, - `⊑-prop`, `Echo-comp-iso` round-trips, pentagon projections, - `SliceHom`↔cone, `bridge-natural`); see - `decisions/no-2-cat.adoc` for the full verdict. -- **[landed — see docs/echo-types/decisions/presentation-dependence.adoc]** - Presentation-dependence sub-theory: examples 5, 9, 10 cluster - here. Common pattern is Σ-over-presentation-parameter `R`; cluster - instantiates the existing Axis 4 without motivating a new axis. - Verdict: meta-pattern only — no `EchoPresentation.agda` module - needed; landed `EchoIndexed`/`EchoChoreo`/`EchoEpistemic` already - carry the per-decoration composition recipe. Axis 4's - "canonical-form operator" open question sharpens but stays open. - See `decisions/presentation-dependence.adoc` for the full verdict. -- **[refreshed — see decisions/gate1-adjacency-refresh.adoc]** - Gate 1 adjacency refresh: the five existing adjacency notes - predate the taxonomy. Cross-check each against the current axes - and flag any neighbour whose identity claim should be - re-evaluated. Verdict: 5/5 REFINED, 0 RE-EVALUATE; every - distinctness claim survives, all five benefit from being - re-stated in terms of the now-numbered axes (axis 8 sharpens - four of five). No content rewrites scheduled; coherence - follow-ups listed in the closure note. - ---- - -## Formalisation work — Agda, no bottleneck - -- **[landed]** `Echo-comp-iso` in `Echo.agda`: the accumulation - isomorphism `Echo(g ∘ f) y ≃ Σ B (λ b → Echo(f) b × (g b ≡ y))`. - Shipped as `Echo-comp-iso-{to, from, from-to, to-from}`; both - round-trips are definitional. See `composition.md` §1. -- **[landed]** `cancel-iso-to` / `cancel-iso-from` / - `cancel-iso-from-to` / `cancel-iso-to-from` in `Echo.agda`, - packaged as `Echo.cancel-iso : ... → Echo (g ∘ f) y ↔ Echo f (s y)` - via stdlib's `Function.Bundles._↔_` and `mk↔ₛ′`. Both round-trips - parameterised by their respective triangle identities (one - triangle implies the other in HoTT but the adjustment is - non-trivial path algebra, so both stay explicit). Companion - `Echo.Echo-comp-iso` packages the unconditional accumulation iso - the same way. See `composition.md` §3 + §4. -- **[landed]** Pentagon coherence for three-fold composition. - Projection lemmas `Echo-comp-iso-pent-B` and `Echo-comp-iso-pent-echo` - both `refl` in `Echo.agda`. The full Σ-associativity iso between the - two nested Σ-shapes (outer-first carries an extra intermediate - `c : C` with `g b ≡ c`; inner-first absorbs it) now ships as - `Echo-comp-pent-Σ-assoc-{to, from, from-to, to-from}`. The forward - map collapses `c` against `g b ≡ c` and transports the outer - h-equation; the backward map sets `c := g b` with `refl`. Both - round-trips reduce definitionally once the `g b ≡ c` has been pinned, - so this is a strict iso (no transport coherence required) and lives - inside `--safe --without-K`. All four pinned in `Smoke.agda`. -- **[landed]** Budgeted recursive-surface WF on the ordinal track. - `Ordinal/Buchholz/RecursiveSurfaceBudget.agda` ships - `BudgetedBT = ℕ × BT`, the budgeted relation `_<ᵇʳᶠᵇ_` with its - `spend` constructor, `wf-<ᵇʳᶠᵇ : WellFounded _<ᵇʳᶠᵇ_` (via - subrelation on ℕ), and `<ᵇʳᶠᵇ⇒lifted` transporting each budgeted - step into the iterated-wrapper tower (`IteratedExtendedOrder`). -- **[landed, 2026-05-20]** Budgeted shared-binder WF for the - K-restricted extended order. - `Ordinal/Buchholz/OrderExtendedBudget.agda` ships - `BudgetedBT⁺ = ℕ × BT`, the budgeted relation `_<ᵇ⁺ᵇ_` with its - `spend` constructor, and `wf-<ᵇ⁺ᵇ : WellFounded _<ᵇ⁺ᵇ_`. Mirrors - the recursive-surface pattern but for the depth-1 shared-binder - cases (`<ᵇ⁺-ψα`, `<ᵇ⁺-+2`). -- **[closed-impossible, 2026-05-20]** The unbudgeted global - theorem — eliminate the explicit ℕ budget from `wf-<ᵇʳᶠᵇ` to get - `WellFounded _<ᵇʳᶠ_`, or analogously for `_<ᵇ⁺_` — is - structurally impossible for the current `_<ᵇ_`. The - Echidna-SA-recommended rank-into-Brouwer route in - `RankBrouwer.agda` was refuted by a worked counterexample on - `<ᵇ-+Ω`. All four alternative routes also walled. See - `buchholz-rank-obstruction.adoc` for the full analysis and the - two substantial-work paths that could re-open the question - (WF-restricted `_<ᵇ_` or non-additive denotational measure). -- **[landed]** `EchoApprox.agda`: new module for ε-indexed echoes - over a metric codomain. First-class taxonomy axis 2 artifact. - Ships `EchoR ε f y = Σ A (λ x → dist (f x) y ≤ ε)` parametric over - a `Tolerance` monoid and a `PseudoMetric`, with three headline - lemmas: `echo-approx-intro` (exact ⇒ zero-ε), `echo-approx-relax` - (monotone in ε), and `echo-approx-compose` (additive composition - under a non-expansive outer leg, realising the taxonomy §2 - conjecture). Wired into `All.agda` and `Smoke.agda`. -- **[landed]** Composition rung first slice (Axis 2): the §Q3 - retract-shape. `EchoApprox.agda` now also ships - `echo-strict→approx` (general strict ⇒ zero-tolerance, generalises - `echo-approx-intro` from own-fibre to arbitrary `y` via the - codomain equation), `echo-approx-comp-sound` (RHS-Σ → LHS via - `echo-approx-compose`), `echo-approx-comp-retract-to` - (canonical-split LHS → RHS-Σ section, picking `b := f x`, - `ε₁ := zero`, `ε₂ := ε`), and `echo-approx-comp-retract-A` (the - A-component round-trip `proj₁ ∘ sound ∘ retract-to ≡ proj₁`, - proved by `refl`). The retraction direction on the A-witness holds - definitionally as the design note (§5) predicts. The B-component - and tolerance-budget round-trips are deferred to a subsequent - rung — they need a `+`-left-identity axiom on `Tolerance` - (`zero + ε ≡ ε`) which the current record does not supply. - §7 obligations 7 (separated zero-collapse) and 8 (axis-1 shadow - agreement) likewise deferred. -- **[landed]** Per-decoration composition lemmas across the - five-decoration family — **sweep complete** (2026-04-28): - `EchoGraded.degrade-compose`, `EchoLinear.degradeMode-compose`, - `EchoIndexed.map-role-indexed-comp`, - `EchoChoreo.applyChoreo-{comp, compose, via-join}` along the - choreographic-reachability order `_⊑c_`, and - `EchoEpistemic.knowledge-monotone-{comp, id}`. Each follows the - same recipe (decoration order → propositionality → join → - factoring-free compose → via-join restatement). All headlines - pinned in `Smoke.agda`. -- **[landed]** Honest finite-domain Landauer/Bennett bounds - (2026-04-28). `EchoFiberCount.agda` provides the actual fiber - count `FiberSize-fin : (Fin n → B) → B → DecEq → ℕ` plus four - headline lemmas (`FiberSize-fin-id-zero`, `FiberSize-fin-const`, - bidirectional `FiberSize-fin ≡ 0 ⟺ ¬ Echo`). - `EchoThermodynamics.agda` rewritten against - `Data.Nat.Logarithm.⌊log₂_⌋`: `bennett-reversible`, - `bennett-reversible-id-zero`, `landauer-collapse`. Replaces the - earlier `FiberSize = 1` hardcode that rendered the prior - CNO-zero-energy claims vacuous. Infinite-domain - (`ProgramState = ℕ → ℕ`) case explicitly out of scope. - `docs/ECHO-CNO-BRIDGE.adoc` swept to remove four overclaim sites. -- **[partial]** Buchholz extended order `_<ᵇ⁺_` (2026-04-28, - updated 2026-05-20). `Ordinal.Buchholz.OrderExtended.agda` adds - the two K-restricted shared-binder lex constructors (`<ᵇ⁺-ψα`, - `<ᵇ⁺-+2`) on top of the K-free core `_<ᵇ_`, with explicit - equality witnesses to keep implicits pairwise distinct. - `<ᵇ⁺-irrefl` and `<ᵇ⁺-trans` proved (mixed cases via four - `extend-{lhs, rhs}` helpers). - Well-foundedness in **budgeted form** for `_<ᵇ⁺_` landed - 2026-05-20: `Ordinal.Buchholz.OrderExtendedBudget` ships - `wf-<ᵇ⁺ᵇ` (mirrors `wf-<ᵇʳᶠᵇ`). The **unbudgeted** form is - CLOSED-IMPOSSIBLE for the current `_<ᵇ_` — see - `docs/echo-types/buchholz-rank-obstruction.adoc` for the - structural impossibility (`<ᵇ-+Ω` ordinal unsoundness) - refuting all five plausible routes. The historical "Route A / - Route B" framing in `buchholz-extended-wf.md` is now - superseded. -- **[unblocked]** Add example-library Agda files matching - `examples.md`: start with examples 1–4 already in-suite, then - example 7 (ordinal collapse is in `EchoOrdinal`); examples 5, 6, - 9, 10 are new Agda candidates. - ---- - -## Example work — mostly writing, some coding - -- **[unblocked]** Complete worked numeric example (ex. 6) with the - approximate-echo shape, once the definition lands. -- **[landed]** Parser residue example (ex. 9) — `EchoExampleParser.agda` - (PR #83): balanced parens, Boolean shadow `parses : List Token → - Bool` non-injective on `(())` vs `()()`, echo retains the token - stream. -- **[landed]** Abstract-interpretation example (ex. 10) — - `EchoExampleAbsInt.agda` (PR #82): Sign lattice `{neg, zero, pos}` - over a hand-rolled five-element integer carrier; collapses - `{m1, m2} ↦ neg`, `{z} ↦ zero`, `{p1, p2} ↦ pos`. -- **[landed]** Database provenance example (ex. 5) — - `EchoExampleProvenance.agda` (PR #81): K-provenance semiring, - distinct Bool-provenance rows projecting to the same payload. -- **[unblocked]** Extend `EchoExamples.agda` with further canonical - entries (post-#81/#82/#83 the cluster has good coverage; only - ex. 6 remains). - ---- - -## Application work — no proof assistant needed for first-pass prose - -- **[unblocked]** **Compiler-analysis residue.** Write up how Echo - Types names the residue produced by abstract interpretation, - register allocation, SSA conversion, and constant folding. - Cross-reference existing literature (e.g. Cousot/Cousot for AI, - various works on "explainable compilation"). -- **[unblocked]** **Database provenance.** Tie to K-provenance and - the `Bag`-semiring tradition. The adjacency note already exists; - extend into a discipline-specific Echo Types chapter. -- **[unblocked]** **Verification / refinement.** Relate Echo Types - to refinement types and to proof-carrying code. The intensional - witness is a "refinement that survives erasure". -- **[unblocked]** **ML interpretability / AI abstraction.** The most - speculative. Echo Types could name the residue of information- - losing layers in neural networks (pooling, attention heads, - embedding projections). Write as a *speculative* chapter with - explicit open questions; do not overclaim. -- **[unblocked]** **Concurrency / choreography.** `EchoChoreo.agda` - already models role-observation echoes. Extend to a distributed- - systems residue discipline. - ---- - -## Proof-assistant-dependent work — gated - -- **[partial]** Internalize the missing shared-binder shapes as - actual constructors of the Buchholz order. **Done** for the - irrefl + trans layer in `Ordinal.Buchholz.OrderExtended._<ᵇ⁺_` - with `<ᵇ⁺-ψα` and `<ᵇ⁺-+2` (2026-04-28). Well-foundedness for - the enlarged order is open — see the gated entry below. -- **[gated on `_<ᵇ⁺_` WF]** Re-close well-foundedness for the - enlarged order. Two design routes documented in - `docs/echo-types/buchholz-extended-wf.md`: single-mutual block - with widened bundle (Route A — attempted, blocked on Agda - termination) or rank-embedding into Brouwer ordinals (Route B - — recommended next-attempt; scaffolded by - `Ordinal.Buchholz.RankBrouwer.agda` from the parallel session). -- **[gated on B1]** Ordinal semantics of BT terms: denotation - `BT → Ordinal` preserving order. Requires a formal `Ordinal` type - as a prerequisite, which is itself downstream of WF. -- **[partial]** Landauer / Shannon rigorous bridge. **Done** for - the finite-domain Landauer/Bennett shape in - `EchoThermodynamics.agda` (rewritten 2026-04-28 against - `EchoFiberCount.FiberSize-fin` and `Data.Nat.Logarithm.⌊log₂_⌋`). - Open: infinite-domain `ProgramState = ℕ → ℕ` extension (needs a - capacity / measure / equivalence-class-quotient framework); - Shannon-entropy formalisation (no probability-monad in stdlib v2 - at the level needed); physical heat-dissipation realisation - (the bound is information-theoretic, not a physical claim). -- **[landed]** CNO content-bridge across echo-types and - `absolute-zero`. `proofs/agda/EchoCNOBridge.agda` imports `IsCNO` - directly from `absolute-zero/proofs/agda/CNO.agda`; both files - build clean under `--safe --without-K`. Cross-prover (Coq/Lean4) - theorem-statement alignment is now documented in - `docs/echo-types/cross-repo-bridge-status.md` (correspondence - table + structural blockers around the relational/functional - `eval` split and the 3 Coq axioms forbidden by `--safe`). -- **[partial]** Janus reversible-file-operations bridge against - `januskey`'s actual API. Agda side is still a 4-variant name-bridge; - decision recorded to structural-mirror the canonical 8-variant - Idris2 `OpKind` (`januskey/src/abi/Types.idr`). Content-bridge - remains gated on `januskey/PROOF-NEEDS.md`. -- **[partial]** Tropical-resource-typing alignment. Adjacent repo - audited 2026-05-20 (remote `hyperpolymath/tropical-resource-typing` - active; 9 `.thy` + `TropicalSessionTypes.lean`). First alignable - theorem pair identified: Agda `⊕-idem` ↔ Isabelle `trop_add_idem` - ↔ Lean `add_comm_trop`+`add_assoc_trop`. Alignment is - citation-level (no Agda↔Isabelle/Lean import surface). -- **[gated on B2]** `maa-framework` integration. Out of scope for - the current tooling; needs scope expansion or file export. - ---- - -## Suggested immediate ordering - -This is my honest suggested ordering, conservative about what's -tractable today: - -1. ~~**Theory: axis 2 formal definition**~~ — **landed**. - Formal definition + composition theorem in `taxonomy.md` §2; - `EchoApprox.agda` artifact with three headline lemmas; example 10 - (abstract interpretation widening) worked in - `applications-compiler-analysis.adoc`. -2. ~~**Agda: `Echo-comp-iso` + cancellation**~~ — **fully landed**. - Accumulation iso (`Echo-comp-iso`), both cancellation maps, plus - **full cancellation iso with round-trips** (`cancel-iso-{to, from, - from-to, to-from}` + packaging `Echo.cancel-iso : ... ↔ ...` - parameterised by `s-left`, `s-right`, and both triangle - identities) live in `Echo.agda`. All five pinned in `Smoke.agda`. -3. ~~**Agda: pentagon coherence for `Echo-comp-iso`**~~ — - **fully landed**. Projection pentagon (`Echo-comp-iso-pent-{B, - echo}`) and the full Σ-associativity iso between the two nested - Σ-shapes (`Echo-comp-pent-Σ-assoc-{to, from, from-to, to-from}` + - equivalence-record packaging `Echo-comp-pent-Σ-assoc : ... ↔ ...`) - are both in `Echo.agda`. All pinned in `Smoke.agda`. -4. **Agda: unbudgeted `_<ᵇʳᶠ_` WF on the ordinal track** — - **VERDICT NARROWED 2026-05-20 evening.** The "closed impossible" - framing held for *unrestricted* `_<ᵇ_`. Under the WfCNF - restriction `_<ᵇ⁻_` together with a limit-shaped *ω-power* rank - (`Ordinal.Brouwer.OmegaPow` + `Ordinal.Buchholz.RankPow`), the - path-1 closure is now **10 of 13 constructors** via - relation-agnostic rank-mono primitives (PR #87). The umbrella - theorem `rank-pow-mono-<ᵇ⁰ : x <ᵇ⁰ y → rank-pow x <′ rank-pow y` - lives in `Ordinal.Buchholz.RankMonoUmbrella`; consumers - (whether `_<ᵇ⁻_` or `_<ᵇʳᶠ_` based) construct `_<ᵇ⁰_` - derivations and apply the umbrella. - - **3 cases remain open** under documented structural blockers - (see `buchholz-rank-obstruction.adoc` for the per-constructor - verdict table): - * `<ᵇ-ψα`, `<ᵇ-ψΩ≤` — ψ-admissibility predicate carrier landed - (`Ordinal.Buchholz.WellFormedAdmissible.WfAdm`); rank-refinement - for the discharge is a follow-on slice with a `<ᵇ-+ψ` - cross-case to manage. - * `<ᵇ-+1` joint-bplus — `rank-pow (bplus z₁ z₂)` is not additive - principal in general. Needs a coarser dominator (e.g., - `leading-Ω-index : BT → OmegaIndex`). - - The keystone is the **additive-principal lemma at ω^(suc n)** - (`Ordinal.Brouwer.OmegaPow.additive-principal`). Budgeted forms - (`_<ᵇʳᶠᵇ_`, `_<ᵇ⁺ᵇ_`) remain the canonical well-founded - carriers until the 3-case gap closes. -5. **Gate 1 adjacency refresh against the new taxonomy** — 1 day. - Cheap coherence pass on existing docs. Cross-check each of the - 13 notes in `docs/adjacency/` against the 8 axes in `taxonomy.md` - and flag any neighbour whose identity claim should be re-evaluated. -6. **Theory: pick one axis-8 refinement and formalise it** — 1–2 - days. Four candidates in `taxonomy.md` §8 (cost-indexed echo, - graded access modality, decidability-respecting echo, witness- - search abstract machine). Choosing commits the repo to one - formal handle on computational vs information-theoretic access. -7. ~~**Agda: `EchoApprox.agda`**~~ — **landed**. - First artifact of axis 2. Ships `EchoR ε f y = Σ A (λ x → dist - (f x) y ≤ ε)` parametric over a `Tolerance` monoid and a - `PseudoMetric`, with three headline lemmas: `echo-approx-intro` - (exact ⇒ zero-ε), `echo-approx-relax` (monotone in ε), - `echo-approx-compose` (additive composition under a non-expansive - outer leg). Wired into `All.agda` + pinned in `Smoke.agda`. -8. ~~**Applications chapter: compiler-analysis residue**~~ — - **first draft landed 2026-05-20**. - `docs/echo-types/applications-compiler-analysis.adoc` with two - worked examples (parser error recovery on axis 4; - abstract-interpretation widening on axis 2), all four axis-8 - refinements applied to source-mapping, pipeline composition, - scope demarcation, and cross-references to every relevant - adjacency note. Follow-up: full Agda exhibits for each example - (tracked as `[unblocked]` example-library items below). -9. ~~**Per-decoration composition lemmas**~~ — **sweep complete** - (2026-04-28). All five decorations landed: - `EchoGraded.degrade-compose`, `EchoLinear.degradeMode-compose`, - `EchoIndexed.map-role-indexed-comp`, - `EchoChoreo.applyChoreo-{comp, compose, via-join}` along the - choreographic-reachability order `_⊑c_`, and - `EchoEpistemic.knowledge-monotone-{comp, id}`. Each follows the - same recipe (decoration order → propositionality → join → - factoring-free compose → via-join restatement). All headlines - pinned in `Smoke.agda`. - -The remaining open work in this list is **steps 1, 5, 6, 8**. Steps 1 -and 5–6 are ~3–4 days of honest work that require nothing from proof -assistants, external repos, or the blocked Buchholz path. Step 5 is -the natural next coherence pass; steps 6 and 8 extend into Agda or -prose but depend only on infrastructure we already have in-suite. - -Everything **[gated]** waits for its unblocker. The pack above gives -3–4 weeks of disciplined parallel work without touching the remaining -full-order Buchholz gap. - ---- - -## What this roadmap deliberately does not include - -- No week-by-week date estimates beyond the rough "days" above. - These are order-of-magnitude guides, not commitments. -- No claim about which application area will yield the largest - payoff — ML interpretability, compiler analysis, and database - provenance are all plausible; that decision should come from the - consumer, not the theory. -- No tie to any release tag. `v0.2.0` should be decided on the basis - of actual landed content, not on this roadmap. -- No gating on `docs/buchholz-plan.adoc`'s own milestones (E4, E5, - etc.) — those are a parallel workstream that can advance or stall - without affecting the Echo Types theory development here. - ---- - -## Revision policy for this document - -This roadmap should be updated when: - -- A **[gated]** item becomes unblocked (e.g. Agda upgrade, repo - access granted). -- A new axis is added to `taxonomy.md`. -- An example in `examples.md` gets promoted to formalised Agda. -- The composition laws in `composition.md` get confirmed or refuted. - -Keep the revision history in-file (append-only), and annotate each -update with the trigger. The roadmap is a living document; the -stable content lives in `overview.md`, `taxonomy.md`, and -`composition.md`. diff --git a/docs/echo-types/sigma-distinctness-map.adoc b/docs/echo-types/sigma-distinctness-map.adoc new file mode 100644 index 0000000..4bd4b7f --- /dev/null +++ b/docs/echo-types/sigma-distinctness-map.adoc @@ -0,0 +1,189 @@ += Echo vs. Sigma: distinctness evidence map +:toc: macro +:toclevels: 2 +:sectnums: +:sectnumlevels: 2 +:icons: font + +[.lead] +This file is the reviewer-facing companion to +`core/skepticisms/is-this-just-sigma-types.md`. Its job is one thing: +collect, in one place, the in-repo evidence that `Echo f y` is not +"renamed `Σ A (λ x → f x ≡ y)`" and to organise that evidence under the +five demands a sceptic typically makes. + +[IMPORTANT] +==== +Statements below stay inside the *narrowed* claims of +`docs/retractions.adoc` R-2026-05-18. In particular: no "full +categorical universal property" (the pullback is funext-relative and +pointwise), no "graded comonad" (the loss structure is a thin-poset +reindexing modality), no "model-independence" (the abstract model +interface is carrier-parametricity over a fixed grade poset). +==== + +toc::[] + +== Five demands, five answers + +Each subsection states the demand, names the in-tree artefact(s) that +answer it, and notes any narrowing relative to the stronger statement a +sceptic might want. + +=== Demand 1 — Irreversibility as a theorem family + +[cols="1,3", options="header"] +|=== +| Claim | Echo proves that no section of the loss-map exists, across multiple decoration layers. Raw `Σ` gives `proj₁` trivially. + +| Agda | +`EchoCharacteristic.no-section-collapse`, +`EchoCharacteristic.no-section-visible`, +`EchoResidue.no-section-collapse-to-residue`, +`EchoLinear.no-section-weaken`, +`EchoOrdinal.no-section-ordinal-collapse`, +`EchoEpistemicResidue.no-section-to-epistemic`. All pinned in +`proofs/agda/Smoke.agda`. + +| Prose | `docs/characteristic.adoc`, +`docs/proof-obligations.md` §"No-section" entries, +`readme.adoc` §"Characteristic family". + +| Narrowing | None. The family lemmas are clean negative results under +`--safe --without-K`. +|=== + +=== Demand 2 — Algebra of loss (down-admissible, up-blocked) + +[cols="1,3", options="header"] +|=== +| Claim | The fibre carries a loss-grade lattice with a monotone +reindexing modality. Down-step is admissible; up-step is provably not. + +| Down-step (Agda) | +`EchoGraded.degrade-compose` and `EchoGraded.degrade-via-join` are the +per-decoration composition laws. The same recipe lands at +`EchoLinear.degradeMode-compose`, `EchoChoreo.applyChoreo-compose`, +`EchoAccess` (graded access), `EchoCost` (cost-indexed), +`EchoSearch` (witness-search). + +| Up-step blocked (Agda) | `EchoLinear.no-section-weaken` (= +`EchoResidue.no-section-collapse-to-residue`). + +| Separating model | `EchoSeparating.sep-degrade-compose-fails` — +removing `≤g-prop` (the only load-bearing hypothesis) breaks +`degrade-compose` at a checked `true ≢ false`. This locates the +reduction. + +| Prose | `docs/characteristic.adoc` (Gate 2 audit), N1–N4 nominees. + +| Narrowing | Per R-2026-05-18, this is a *thin-poset reindexing +modality*, not a graded comonad. No nested `D_r D_s` is formed. +|=== + +=== Demand 3 — Categorical identity and bridges + +[cols="1,3", options="header"] +|=== +| Claim | Echo is a recognisable categorical object (the homotopy +fibre) and other "loss-tracking" frameworks bridge into it. + +| Identity (Agda) | `EchoFiberBridge.echo↔fib` — definitional fibre +identity with `refl` round-trips (Pillar A, landed 2026-05-17). + +| Pullback (Agda) | `EchoPullback.echo-pullback-univ` — pullback of +`f` along `y : ⊤ → B` with *pointwise, funext-relative* mediator +property. See retraction note at the head of the module. + +| Bridges (Agda) | `EchoJanusBridge.agda` (reversible debugger), +`EchoTropical.agda` + `AntiEchoTropical.agda` (tropical / argmin), +`EchoCNOBridge.agda`, `DyadicEchoBridge.agda`, +`EchoFiberCount.agda` + `EchoThermodynamicsFinite.agda` (finite-fibre +Landauer / Bennett). + +| Prose | `docs/echo-types/establishment-plan.adoc` §"Pillar A", +`docs/adjacency/`. + +| Narrowing | The bridges are independent witnesses, not a single +"every loss-tracker maps uniquely into Echo" theorem. Such a uniqueness +result would require either funext or an axiom and is therefore *not* +in scope under the no-postulate invariant. +|=== + +=== Demand 4 — Abstraction barrier (consumer-side) + +[cols="1,3", options="header"] +|=== +| Claim | The Echo interface at the affine mode forbids the consumer +from distinguishing two preimages of the same output. Raw `Σ` does +not, via `proj₁`. + +| In-tree precursor (Agda) | `EchoLinear.affine-canonical`, +`EchoLinear.affine-all-equal` — the affine residue carrier is +contractible. + +| Planned (Agda) | `proofs/agda/EchoAbstractionBarrier.agda` — Track B +in the work plan. Headline lemmas: +`affine-consumer-cannot-distinguish` (positive) and +`sigma-distinguishes` (the raw-`Σ` counter-program, as a checked +exhibit of what the barrier blocks). + +| Model-side counterpart (Agda) | `EchoRelModel.GradedLossModel` + +generic `GCLaws` — carrier-parametricity over a fixed grade poset +(Pillar D, narrowed per R-2026-05-18). + +| Narrowing | The planned consumer-side theorem is a *free theorem at +the headline affine instance*, not full Reynolds parametricity (Agda +has no parametricity primitive; a fully general statement would need +an axiom). +|=== + +=== Demand 5 — Canonical examples + +[cols="1,3", options="header"] +|=== +| Claim | Echo is the right explanatory unit on real artefacts, not +just decorative wrapping. + +| Agda | +`EchoExampleParser` (`(())` vs `()()` at `parses ≡ true`), +`EchoExampleProvenance` (collapsed Bool-provenance), +`EchoExampleAbsInt` (`{p1,p2}` ↦ `pos`), +`EchoExampleSignAnalysis`, `EchoExampleTruncation`, +`EchoFiberCount` + `EchoThermodynamics*` (finite-fibre Landauer), +`EchoEpistemicResidue` (observation discipline). + +| Planned matched-negative (Agda) | +`proofs/agda/examples/EchoVsSigma.agda` — Track C in the work plan. +Pairs each headline example with the small raw-`Σ` counter-program +that would let the corresponding bug through. + +| Prose | `docs/echo-types/examples.md`, +`roadmap-gates.adoc` Gate 3. + +| Narrowing | Until Track C lands, the "raw `Σ` would leak" half is +prose, not a checked artefact. +|=== + +== What this file does NOT claim + +The five sections above are an *evidence map*, not a re-litigation of +the gate decisions. In particular: + +* This file does not claim Gate 1, Gate 2, or Gate 3 is passed. That + is the job of `roadmap-gates.adoc`, `docs/characteristic.adoc`, and + the example modules themselves. +* This file does not claim the planned Track B / Track C work is + landed. Where a row mentions "Planned (Agda)", the artefact does not + yet exist on `main`; check `git log` before relying on it. +* This file does not introduce new theorems. It cross-references + artefacts that already live elsewhere in the tree. + +== See also + +* `core/skepticisms/is-this-just-sigma-types.md` — internal devil's + advocate ledger this file is the AsciiDoc companion to. +* `core/skepticisms/is-this-just-fibers.md` — adjacent skepticism. +* `core/skepticisms/what-is-actually-new.md` — the broader question. +* `docs/retractions.adoc` — the R-2026-05-18 narrowing that governs + the prose discipline here. diff --git a/docs/echo-types/tropical-correspondence.md b/docs/echo-types/tropical-correspondence.md index 472235f..664a1b4 100644 --- a/docs/echo-types/tropical-correspondence.md +++ b/docs/echo-types/tropical-correspondence.md @@ -84,8 +84,8 @@ not constitute a unified verification artefact. It closes the grading* (`grade : Session → Tropical` in Lean), which is the symmetric Agda-exclusive direction. - **Long-game alignment target.** When the echo-types ordinal track - reaches Bachmann–Howard (ψ₀(Ω_ω); see `docs/echo-types/roadmap.md` - and `buchholz-plan.adoc`), the adjacent repo's + reaches Bachmann–Howard (ψ₀(Ω_ω); see `roadmap.adoc` §Lane 3 and + `docs/buchholz-plan.adoc`), the adjacent repo's `Tropical_Ordinal_Bridge.thy` becomes the natural cross-repo alignment target (Agda Buchholz BT ↔ Isabelle `tropO` carrier). This target is **firewalled** until the ordinal track lands the diff --git a/docs/theorem-index.md b/docs/theorem-index.md index 2fc369b..7fc5cf1 100644 --- a/docs/theorem-index.md +++ b/docs/theorem-index.md @@ -22,4 +22,49 @@ This document maps foundational theorems and characteristic results to their exa | `visible-constraint` | PROVED | `Echo/Characteristic.agda` | Projection-style loss retains a provable constraint on the source. | | `no-section-collapse-to-residue` | PROVED | `Echo/Residue.agda` | Weakening an echo to a residue discards irrecoverable information. | +## Degrade-law family (aggregate) + +The "degrade" results are the per-decoration composition + join laws +demonstrating that loss has *direction* (down-step admissible, up-step +not — the no-section family below is the matching diagonal). All sites +PROVED and pinned in `proofs/agda/Smoke.agda`. + +| Site | Module Path | +|------|-------------| +| `degrade-comp`, `degrade-compose`, `degrade-via-join` | `EchoGraded.agda` | +| `degradeMode-comp`, `degradeMode-compose`, `degradeMode-via-join` | `EchoLinear.agda` | +| `applyChoreo-compose` | `EchoChoreo.agda` | +| `degrade-access-comp`, `degrade-access-compose`, `degrade-access-via-join` | `EchoAccess.agda` | +| `degrade-cost-compose` (and family) | `EchoCost.agda` | +| `degrade-search-compose` (and family) | `EchoSearch.agda` | + +Separating model (locates the reduction): `EchoSeparating.sep-degrade-compose-fails` +exhibits a checked `true ≢ false` failure when the single load-bearing +hypothesis `≤g-prop` is removed. + +See `core/skepticisms/is-this-just-sigma-types.md` §2 and +`docs/echo-types/sigma-distinctness-map.adoc` §"Demand 2" for the +sceptic-facing framing. Honest framing per +`docs/retractions.adoc` R-2026-05-18: this is a *thin-poset reindexing +modality*, not a graded comonad. + +## No-section family (aggregate) + +The "no-section" results land at six sites across the decoration layers +and are collectively the answer to "raw `Σ` would give `proj₁` for +free". All are pinned in `proofs/agda/Smoke.agda`. + +| Site | Module Path | +|------|-------------| +| `no-section-collapse` | `EchoCharacteristic.agda` | +| `no-section-visible` | `EchoCharacteristic.agda` | +| `no-section-collapse-to-residue` | `EchoResidue.agda` | +| `no-section-weaken` | `EchoLinear.agda` | +| `no-section-ordinal-collapse` | `EchoOrdinal.agda` | +| `no-section-to-epistemic` | `EchoEpistemicResidue.agda` | + +See `core/skepticisms/is-this-just-sigma-types.md` §1 and +`docs/echo-types/sigma-distinctness-map.adoc` §"Demand 1" for the +sceptic-facing framing. + *Note: For experimental bridges or retracted claims, refer to the [Proof Obligation Ledger](proof-obligations.md) and [Bridge Status](bridge-status.md).* diff --git a/proofs/agda/EchoLinear.agda b/proofs/agda/EchoLinear.agda index ba7419d..1fcb6a5 100644 --- a/proofs/agda/EchoLinear.agda +++ b/proofs/agda/EchoLinear.agda @@ -63,7 +63,7 @@ affine-all-equal e1 e2 = trans (affine-canonical e1) (sym (affine-canonical e2)) -- linearity decoration: weakening between modes commutes with -- transitive composition of the mode-ordering. See -- docs/echo-types/composition.md §6 (decoration commuting) and --- docs/echo-types/roadmap.md "Per-decoration composition lemmas". +-- the degrade-law family aggregate row in docs/theorem-index.md. -- -- The mode ordering is the smallest reflexive-and-`linear≤affine` -- relation: linear ⊑ linear, linear ⊑ affine, affine ⊑ affine. The diff --git a/proofs/agda/EchoStabilityTests.agda b/proofs/agda/EchoStabilityTests.agda index 5b93966..2330193 100644 --- a/proofs/agda/EchoStabilityTests.agda +++ b/proofs/agda/EchoStabilityTests.agda @@ -126,4 +126,4 @@ bennett-corollary-check T = -- `FiberSize-fin` is finite-domain only; the infinite case -- needs measure-theoretic or capacity arguments and is open. -- * Shannon-entropy / mutual-information formalisations: not yet --- present in the repo. See `docs/echo-types/roadmap.md`. +-- present in the repo. See `roadmap.adoc` §"Deferred research track". diff --git a/proofs/agda/EchoThermodynamics.agda b/proofs/agda/EchoThermodynamics.agda index c454d11..2baf606 100644 --- a/proofs/agda/EchoThermodynamics.agda +++ b/proofs/agda/EchoThermodynamics.agda @@ -212,6 +212,7 @@ landauer-collapse f y _≟_ T h = -- extension of `FiberSize-fin` to a measure-theoretic count -- on infinite types, neither of which is available here; -- * that Shannon-entropy / informational arguments are --- formalised — they are not. See `docs/echo-types/roadmap.md` --- for the open thermodynamic items. +-- formalised — they are not. See `roadmap.adoc` §Lane 3 +-- (Ordinal track / deferred research) for the open +-- thermodynamic / information-theory items (not yet formalised). ---------------------------------------------------------------------- diff --git a/readme.adoc b/readme.adoc index 5fc03a5..eaffb30 100644 --- a/readme.adoc +++ b/readme.adoc @@ -65,7 +65,15 @@ Scope-broadening stages now include: * indexed / relational / categorical packaging (`EchoIndexed`, `EchoRelational`, `EchoCategorical`, `EchoScope`) * cross-ecosystem bridges (`EchoCNOBridge`, `EchoJanusBridge`, `DyadicEchoBridge`, `EchoOrdinal`) -== Current Status Snapshot (2026-04-23) +== Current Status Snapshot + +The repository runs *two parallel, independent tracks*. _Echo Core does +NOT depend on the Ordinal / Buchholz track._ A reader interested only +in echo types as a type-theoretic concept can ignore the Ordinal track +entirely; it lives in `proofs/agda/Ordinal/` and is documented under +`roadmap.adoc` §Lane 3. + +=== Echo Core (load-bearing for the identity claim) On `main`, the following are true right now: @@ -73,8 +81,25 @@ On `main`, the following are true right now: * Core echo/fiber theorems are present and smoke-pinned (`echo-intro`, `map-over`, `map-over-id`, `map-over-comp`, `map-square`). * Characteristic non-injectivity/no-section family is present (`collapse-non-injective`, `no-section-collapse`, `no-section-visible`, `no-section-collapse-to-residue`, `no-section-weaken`). * Distinct-witness and retained-constraint exemplars are present (`echo-true≢echo-false`, `stateA≢stateB`, `visible-constraint`). +* Degrade-law family lands across decoration layers (graded, linear/affine, choreographic, access, cost, search); see `docs/theorem-index.md` for the aggregate. +* Pillars A–D of the establishment plan are LANDED (with R-2026-05-18 narrowings; see `docs/retractions.adoc`); Pillar E (paper) is in progress. + +Per-lane status, close-out criteria, and the identity-claim verdict +per tag are in `roadmap.adoc`. -Ordinal/Buchholz track status: +=== Ordinal / Buchholz (parallel-independent, experimental) + +[NOTE] +==== +*Banner.* This track is a separate proof-theoretic research project +living in the same repository. Echo Core does not depend on it. +Modules under `proofs/agda/Ordinal/` are treated as *experimental* +until the unbudgeted `wf-<ᵇʳᶠ_` closure lands. See `roadmap.adoc` +§Lane 3 for status and close-out criterion; `docs/buchholz-plan.adoc` +for the full plan. +==== + +Current state (the full per-rung ledger lives in CLAUDE.md): * `Ordinal.Buchholz.WellFounded` provides `wf-<ᵇ : WellFounded _<ᵇ_` for the currently admitted constructor core. * Top-marker `bplus` bridges are now admitted and inverted: @@ -128,7 +153,7 @@ Cross-repo status: * Agda-side content-bridge `proofs/agda/EchoCNOBridge.agda` imports `IsCNO` directly from `absolute-zero/proofs/agda/CNO.agda` (the earlier scaffolded-adapter plan `EchoBridgeScaffold.agda` was superseded). * End-to-end conformance against upstream codebases is a separate track and is not yet fully machine-checked here. * Current bridge ledger: `docs/echo-types/cross-repo-bridge-status.md`. -* See `docs/echo-types/roadmap.md` for staged cross-repo verification gates. +* See `roadmap.adoc` (Lane 4) for staged cross-repo verification gates. == What Echo Types Are For @@ -193,7 +218,7 @@ Proof milestones and decision gates are in: Open/gated work and cross-repo follow-ups are tracked in: -* `docs/echo-types/roadmap.md` +* `roadmap.adoc` * `docs/echo-types/taxonomy.md` * `docs/echo-types/composition.md` diff --git a/roadmap-gates.adoc b/roadmap-gates.adoc index 93bce4b..5e65e6d 100644 --- a/roadmap-gates.adoc +++ b/roadmap-gates.adoc @@ -103,6 +103,16 @@ There exist theorems whose statements are naturally echo-shaped and are not reducible to generic sigma/fiber lemmas. **** +[NOTE] +==== +The reviewer-facing evidence map answering "is this just renamed Σ?" — +organised under five sceptic demands — lives at +`docs/echo-types/sigma-distinctness-map.adoc` (companion to +`core/skepticisms/is-this-just-sigma-types.md`). It is an *evidence +index*, not a substitute for the per-nominee audit below or for the +Gate 2 decision itself. +==== + === Test Nominate at least three theorems from the development as characteristic. diff --git a/roadmap.adoc b/roadmap.adoc index c93a238..fcf37b0 100644 --- a/roadmap.adoc +++ b/roadmap.adoc @@ -1,514 +1,412 @@ -= echo-types Proof Roadmap += echo-types Roadmap +:toc: macro +:toclevels: 3 +:sectnums: +:sectnumlevels: 3 +:icons: font + +[.lead] +Single canonical roadmap for the echo-types project. As of 2026-05-26 +this file replaces the previously fragmented set of overlapping +roadmaps (`docs/echo-types/roadmap.md`, `docs/PRIORITIZED_PROOF_ROADMAP.md`, +`docs/ProofRoadmap.md`, `docs/WORK_PLAN.md` — all deleted in this +sweep; CLAUDE.md retains the per-session rung-consolidation ledger, +`roadmap-gates.adoc` retains the identity-claim gates, +`docs/echo-types/establishment-plan.adoc` retains the five-pillar +plan). + +[IMPORTANT] +==== +*Reading order.* This file tracks **lanes** — which lane is currently +load-bearing, what closes each one, what is parked. The gates +(`roadmap-gates.adoc`) define the identity claim's falsifier. The +pillars (`docs/echo-types/establishment-plan.adoc`) define the path to +type-theoretic standing. CLAUDE.md is the session-level rung ledger. + +*Retraction discipline.* The single most credible thing about this +project is `docs/retractions.adoc` R-2026-05-18: under adversarial +review, four headline claims were narrowed (full universal property → +funext-relative pointwise mediator; graded comonad → thin-poset +reindexing modality; model-independence → carrier-parametricity over a +fixed grade poset; conservativity metatheorem → postulate-free build +that is evidence-for, not proof-of, conservativity). Narrowing is a +feature, not a defect. Every lane below carries an explicit +*retraction-watch* line to prevent re-overclaim. +==== + +toc::[] == Mission -Establish whether echo types are a genuine proof-theoretic concept, not merely a naming layer over fibers. +Establish whether echo types are a genuine type-theoretic concept +comparable to choreographic, linear, and graded modal type systems — +not merely a naming layer over fibres. Guiding claim: -*echo types formalize irreversible computation with retained constraints on what was lost.* +*echo types formalise irreversible computation with retained +constraints on what was lost, occupying the same conceptual +neighbourhood as graded modalities (Granule / QTT), choreographic +types (Hirsch et al.), and substructural disciplines (Linear Haskell / +Atkey QTT).* Decision policy: -* If the claim can be established with precise theorems and examples, continue and scale. -* If it cannot be established, document failure clearly and stop the identity claim. - -Document map (to keep status/docs aligned): - -* `README.md` / `readme.adoc`: current snapshot and build entry points. -* `roadmap.adoc` (this file): canonical milestone log for the echo-theory track. -* `docs/buchholz-plan.adoc`: canonical status for the ordinal/Buchholz WF track. -* `docs/echo-types/roadmap.md`: gated and cross-repo follow-up queue. - -== Current Foundation (Established) - -File: `proofs/agda/Echo.agda` - -Already proved: - -* `Echo` definition via sigma/fiber -* `echo-intro` -* `map-over` -* `map-over-id` -* `map-over-comp` -* `map-square` - -These are the minimal structural laws for functorial behavior over fixed codomain and commuting-square transport. - -== Workstream A: Characteristic Echo Theorems - -Goal: prove results that express *structured loss*, not only generic sigma manipulation. - -Target theorem family: - -1. Non-injective with retained witness: - prove explicit examples where `x₁ ≠ x₂` and `f x₁ ≡ f x₂`, but echoes retain distinguishing constraints. -2. Irreversible but not forgetful: - formalize that plain output `y : B` underdetermines source while `Echo f y` remains proof-relevant. -3. Collapse with constrained preimage: - model collapse maps and prove retained witness class constraints. -4. Distinct echoes over same visible result: - for fixed `y`, exhibit non-identical echo inhabitants carrying different source constraints. - -Pass condition: - -* at least 3 nontrivial theorems above compile and are phrased without ad hoc postulates. - -Fail condition: - -* all attempted statements reduce to tautological repackaging with no additional inferential content. - -== Workstream B: Weakened Echo / Residue Types - -Goal: formalize “not full witness, but certified residue”. - -Planned form: - -[source] ----- -EchoR f R y := Σ (r : R y) , Certifies r ----- - -where `R y` captures residue-level evidence and `Certifies` links it to preimages. - -Pass condition: - -* at least one residue construction that is strictly weaker than full fiber witness and still supports useful inference. - -Fail condition: - -* residue variants collapse either to full fibers or to vacuous annotations. - -== Workstream C: Canonical Examples - -Goal: show echo types solve examples better than nearby notions. - -Priority examples: - -1. Squaring `x ↦ x²`: visible `9`, hidden sign provenance. -2. Structured projection: state projection with retained constraints on forgotten fields. -3. Quotient-like map: identify equivalence classes while retaining certified class-level residue. -4. Scar/collapse examples: retained witness under collapse transformations. - -Pass condition: - -* examples are executable as Agda definitions/lemmas, not prose only. - -== Workstream D: Semantic Bridge - -Goal: connect DTT construction to categorical semantics without overcommitting to HoTT. - -Deliverables: - -* slice-over-fixed-codomain reading of `map-over` -* commuting-square transport reading of `map-square` -* explicit statement of assumptions used (intensional equality only unless otherwise stated) - -Pass condition: - -* semantics map cleanly onto existing proofs, with no hidden extensionality assumptions. - -== Milestones - -M1. Foundation complete (DONE): core echo/fiber functoriality module compiles. - -M2. Characteristic theorem pack: - -* add `proofs/agda/EchoCharacteristic.agda` (or similar) -* compile cleanly - -Status: DONE (2026-04-18) - -Delivered in `proofs/agda/EchoCharacteristic.agda`: - -* `collapse-non-injective` -* `no-section-collapse` -* `echo-true≢echo-false` -* `visible-constraint` -* `state₁≢state₂` -* `no-section-visible` -* `transport-visible-not` - -M3. Residue formalization: - -* add `proofs/agda/EchoResidue.agda` -* prove at least one strict weakening result - -Status: DONE (2026-04-18) - -Delivered in `proofs/agda/EchoResidue.agda`: - -* generic residue echo `EchoR` -* generic lowering map `echo-to-residue` -* collapse-instance lowering `collapse-to-residue` -* strict weakening witness `strict-weakening-collapse` -* non-recoverability theorem `no-section-collapse-to-residue` - -M4. Example suite: - -* add `proofs/agda/EchoExamples.agda` -* encode and prove at least 3 canonical cases - -Status: DONE (2026-04-18) - -Delivered in `proofs/agda/EchoExamples.agda`: - -* squaring/sign-loss model (`square9`, `echo-plus3`, `echo-minus3`) -* structured projection model (`visible`, `visible-constraint`, `stateA≢stateB`) -* quotient/collapse model (`quot`, `quot-echo-classification`) -* collapse residue identification (`collapse-residue-identifies`) - -M5. Assessment report: - -* add `docs/assessment.adoc` with binary conclusion: - * established as distinct concept - * not established (end-of-story) - -Status: DONE (2026-04-18) - -Delivered in `docs/assessment.adoc` with binary verdict. - -M6. Choreographic bridge: - -* add `proofs/agda/EchoChoreo.agda` -* define role-indexed echoes via global-to-local projections -* prove transport along commuting squares - -Status: DONE (2026-04-18) - -Delivered in `proofs/agda/EchoChoreo.agda`: - -* `RoleEcho` -* `client-non-injective`, `server-non-injective` -* `client-to-server` -* `client-stability` -* `client-preimage-class` - -M7. Epistemic bridge: - -* add `proofs/agda/EchoEpistemic.agda` -* define indistinguishability and echo-indexed knowledge -* prove non-trivial non-knowledge examples - -Status: DONE (2026-04-18) - -Delivered in `proofs/agda/EchoEpistemic.agda`: - -* `Indist` -* `Knows` -* `knowledge-monotone` -* `not-knows-server-true-at-client-true` -* `shared-echo-from-indist` -* `indist-from-two-echoes` - -M8. Linear/affine bridge: - -* add `proofs/agda/EchoLinear.agda` -* formalize strict weakening from full witness to affine residue - -Status: DONE (2026-04-18) - -Delivered in `proofs/agda/EchoLinear.agda`: - -* `Mode`, `LEcho` -* `weaken` -* `strict-linear-example` -* `no-section-weaken` - -M9. Graded bridge: - -* add `proofs/agda/EchoGraded.agda` -* define grade order and compositional degradation - -Status: DONE (2026-04-18) - -Delivered in `proofs/agda/EchoGraded.agda`: - -* `Grade`, `_≤g_` -* `degrade` -* `degrade-comp` -* `⊔g-assoc` - -M10. Tropical bridge: - -* add `proofs/agda/EchoTropical.agda` -* prove distinct candidates can share visible tropical value but retain distinct echoes - -Status: DONE (2026-04-18) - -Delivered in `proofs/agda/EchoTropical.agda`: - -* `score` -* `tropical-non-injective` -* `IsArgmin`, `TropEcho` -* `distinct-candidates-same-visible-distinct-echo` - -== Controlled Scope Broadening (A-D) - -Status: DONE (2026-04-18) - -Phase A (`proofs/agda/EchoIndexed.agda`): - -* role-indexed echoes `Echoᵢ` -* `echoᵢ-intro`, indexed transport `map-role-indexed` -* trace-level provenance examples (`echo-user-ok`, `echo-auditor-ok`) - -Phase B (`proofs/agda/EchoEpistemicResidue.agda`): - -* residue-based epistemic echoes via `EchoR` -* lowering `to-epistemic` from full echo to residue -* strict weakening witness (`no-section-to-epistemic`, `strict-epistemic-weakening`) - -Phase C (`proofs/agda/EchoRelational.agda`): - -* relational semantics `EchoStep Step o = Σ s , Step s o` -* relational transport (`map-rel`, `map-rel-id`, `map-rel-comp`, `map-rel-square`) -* nondeterministic fiber example (`StepND`, distinct echoes over `true`) - -Phase D (`proofs/agda/EchoCategorical.agda`): - -* slice packaging (`SliceHom`, `slice-act`, `slice-act-comp`) -* relational/fibration packaging (`Fiber`, `Total`, `π`) -* projection-fiber bridge (`fiber-to-echo`, `echo-to-fiber`) - -Cross-phase coherence (`proofs/agda/EchoScope.agda`): - -* graph roundtrips (`graph-roundtrip₁`, `graph-roundtrip₂`) -* indexed-to-relational bridge (`indexed-to-graph`) -* relational-to-residue bridge (`rel-to-residue`) -* slice/fibration coherence (`slice-act-via-relmap`, `fiber-echo-to-residue`) - -Single-shot build entrypoint (`proofs/agda/All.agda`): - -* imports the full proof suite for one-command checking - -M11. Full-suite gate: - -* compile every module under `proofs/agda` from a clean `_build` cache -* ensure no residual failing module after scope broadening - -Status: DONE (2026-04-18) - -Gate command: - -[source,bash] ----- -cd /var/mnt/eclipse/repos/echo-types -find _build/2.8.0/agda/proofs/agda -type f -name '*.agdai' -delete 2>/dev/null || true -cd proofs/agda -for f in *.agda; do agda -i . "$f"; done ----- - -M12. Cross-bridge integration: - -* add `proofs/agda/EchoIntegration.agda` -* prove a theorem combining choreographic knowledge preservation with graded - controlled degradation behavior - -Status: DONE (2026-04-18) - -Delivered in `proofs/agda/EchoIntegration.agda`: - -* `knowledge-preserved-under-choreo` -* `merged-at-residue` -* `no-recovery-after-residue-degrade` -* `knowledge-and-controlled-degradation` - -== Workstream E: Ordinal / Buchholz Infrastructure - -Goal: stand up a syntactic Buchholz-style collapsing notation system -that is *separate from* the echo/fiber core, staged so that each -milestone compiles before the next is attempted. This is the layer -that must exist before any claim about `ψ(Ω_Ω)` is even stateable. - -Full plan: `docs/buchholz-plan.adoc`. - -E1. Ordinal syntax core (M1-equivalent for this workstream): - -* add `proofs/agda/Ordinal/Base.agda` — toy ordinal-term type `OT` - with constructors `zero`, `omega`, `plus`, `psi` -* no semantics asserted; structural inequalities only - -Status: DONE (2026-04-22) - -Delivered in `proofs/agda/Ordinal/Base.agda`: - -* `OT`, `zero`, `omega`, `plus`, `psi` -* `one`, `ω^ω` -* `zero≢omega`, `zero≢one`, `omega≢one` -* `psi-injective`, `plus-injective` - -E2. ℕ-staged closure discipline: - -* add `proofs/agda/Ordinal/Closure.agda` — staged closure family - `C : ℕ → OT → Set` with the Buchholz-style backward-referencing - `c-psi` rule -* prove the headline lemma *before any ψ-value is defined*: - `C-monotone : ∀ {m n t} → m ≤ n → C m t → C n t` -* pin `C-monotone` in `Smoke.agda` - -Status: DONE (2026-04-22) - -Delivered in `proofs/agda/Ordinal/Closure.agda`: - -* `C` with constructors `c-zero`, `c-omega`, `c-plus`, `c-psi` -* `C-monotone` — closure monotonicity under stage increase -* `C-refl-stage` — immediate corollary via `≤-refl` -* `psi-omega-at-1`, `psi-omega-at-2` — worked instances - -Pass condition for E2: - -* `C-monotone` compiles without postulates -* full-suite and smoke CI jobs both still pass - -E3. Cantor normal form: - -* add `proofs/agda/Ordinal/CNF.agda` — CNF fragment below ε₀ -* prove trichotomy of the CNF strict order - -Status: DONE (2026-04-24) - -Delivered in `proofs/agda/Ordinal/CNF.agda`: - -* `CNF`, `_<ᶜ_` -* `<ᶜ-irrefl`, `<ᶜ-trans` -* `cnf-trichotomy` -* worked witnesses `one<ᶜtwo`, `two<ᶜω`, `one<ᶜω` - -E4. Pedagogical ψ: - -* add `proofs/agda/Ordinal/PsiSimple.agda` -* prove `psi-notin-C` and `psi-least` on the ℕ-staged closure - -Status: DONE (2026-04-24) - -Delivered in `proofs/agda/Ordinal/PsiSimple.agda`: - -* `psi-notin-C` -* `psi-at-1` -* `psi-least` - -E5. Buchholz fragment (ν ≤ ω): - -* add `proofs/agda/Ordinal/Buchholz/{Syntax,Closure,Psi}.agda` -* prove `Cν-monotone`, `psiν-notin-Cν`, `psiν-least-gap` - -Status: DONE (2026-04-24) - -Delivered in `proofs/agda/Ordinal/Buchholz/{Closure, Psi}.agda`: - -* `Cν-monotone`, `Cν-index-monotone`, `Cν-monotone-both` -* `psiν-notin-Cν`, `psiν-stage-lb`, `psiν-index-bound` -* `psiν-at-succ` — constructive entry at stage `suc k` from `Cν ν k β` -* `psiν-least-gap` — least-gap decomposition `(k, suc k ≤ m, Cν ν k β)` - -E6. Target expressibility: - -* add `proofs/agda/Ordinal/Buchholz/Examples.agda` -* formalise the first named milestones in order: - `ψ_0(0)`, `ψ_0(1)`, `ψ_0(Ω)`, `ψ_0(Ω_ω)` (Bachmann–Howard), - then the term corresponding to `ψ(Ω_Ω)` under the chosen reading - -Status: DONE (2026-04-24) - -Delivered in `proofs/agda/Ordinal/Buchholz/Examples.agda` + `WellFormed.agda`: - -* `bh-psi0-omega1`, `bh-psi0-omegaω` (Bachmann–Howard target term) -* `psi0-expands`, `psi0-Omega1-target` -* `BH`, `BH-wf` -* `psi-OmegaOmega`, `psi-OmegaOmega-wf` (intended `ψ(Ω_Ω)` reading) - -E7. Echo bridge: - -* add `proofs/agda/EchoOrdinal.agda` — collapse-step as non-injective - map, echo-indexed retention of pre-collapse provenance -* prove `ordinal-collapse-non-injective`, - `distinct-provenances-same-visible`, and a `no-section`-style - theorem over collapse - -Status: DONE (2026-04-24) - -Delivered in `proofs/agda/EchoOrdinal.agda`: - -* `ordinal-collapse : BT → OmegaIndex` — syntactic visible-level map -* `ordinal-collapse-non-injective` -* `ordinal-echo-left`, `ordinal-echo-right`, - `ordinal-echo-left≢ordinal-echo-right` - (aliased as `distinct-provenances-same-visible`) -* sharper same-Ω-index ψ-argument collapse: - `ordinal-psi-arg-bzero`, `ordinal-psi-arg-omega1`, - `ordinal-psi-args-distinct`, `ordinal-psi-arg-collapse-agree`, - `ordinal-echo-psi-distinct` -* `no-section-ordinal-collapse` — no right-inverse to collapse -* `IsZeroSource`, `ordinal-collapse-classification` — - Omega0-preimage classification into the four BT heads - -M13. Headline-theorem smoke gate: - -* add `proofs/agda/Smoke.agda` pinning load-bearing names per bridge module - via `using` clauses -* wire it into `All.agda` and a dedicated CI step so silent renames or - deletions fail CI fast even if the rest of the suite still typechecks -* harden `.github/workflows/agda.yml`: SHA-pin checkout, add SPDX header, - set workflow-level `permissions: read-all` - -Status: DONE (2026-04-19) - -== Deferred Research Track - -These are open synthesis problems graduated from `docs/next-questions.adoc`. -They are dissertation-scale or require extensions beyond the current -`--safe --without-K` core, so they sit on the roadmap rather than on the -near-term backlog. Each entry records the gap, what would close it, and -why it is parked. - -R1. Unified dependent linear + choreographic + epistemic calculus - -* Gap: bridges exist pairwise but not as one typed calculus enforcing - usage discipline + role projection + knowledge operators simultaneously. -* Closure: a core syntax/judgment layer with preservation/progress-style +* If the claim is established at recognised type-theoretic standing, + continue and scale into broader research directions. +* If it is refuted, narrow honestly (per the existing retraction + discipline) and either continue under the narrowed claim or stop the + identity claim and retain the suite as Agda exposition. + +== Identity claim verdict (per tag) + +The gates are reassessed at each tagged release. Verdict below is +current as of `main` HEAD; check `docs/retractions.adoc` for the +narrowing history and `roadmap-gates.adoc` for the test discipline. + +[cols="2,1,3", options="header"] +|=== +| Gate | Status | Anchor + +| Gate 1: Distinct phenomenon +| PROVISIONAL +| `docs/adjacency/` — 5/5 REFINED adjacency notes per `docs/echo-types/decisions/gate1-adjacency-refresh.adoc`. + +| Gate 2: Characteristic theorem family +| PASSED (narrowed) +| `docs/characteristic.adoc` — 4 nominees, 3 survive threshold. Aggregate degrade-law family pinned in `docs/theorem-index.md`. + +| Gate 3: Canonical examples +| PROVISIONAL +| Positive examples landed (`EchoExample*.agda`); matched-negative companions planned (Track C, Lane 2). +|=== + +No gate is currently FAILED. No gate is currently STABLE-ESTABLISHED; +re-assessment cadence is per tagged release. + +== Lanes + +*Cap = 5 open lanes.* Adding a 6th requires closing or parking an +existing one. Each lane carries a falsifiable close-out criterion +audited at every rung consolidation per CLAUDE.md §"Rung-consolidation +policy". Closed lanes move to §"Closed lanes" with the closing artefact +named. + +Priority ordering reflects the load-bearing question as of 2026-05-26: +*expeditious type-theoretic grounding alongside choreographic, linear, +and graded modal types*. Lanes are not equally important; Lane 1 +gates the project's external standing and gets the time. + +=== Lane 1 [LOAD-BEARING] — Type-theoretic grounding + +*Load-bearing question.* Does Echo land, externally, in the same +conceptual neighbourhood as Granule (graded modal), Atkey QTT, the +Hirsch et al. choreographic types, and substructural Linear Haskell — +and is that landing both *visible* (paper-form, citable) and +*defensible* (survives a referee pass)? + +*Bottleneck.* Pillar E (the paper) has `[EXPAND]` tags blocking +submission. The consumer-side abstraction-barrier proof (Track B, +under Lane 2) is the one new Agda artefact that materially strengthens +the paper's narrowed-but-honest claim against the "is this just Σ?" +objection. + +*Close-out criterion (falsifiable).* All three hold: + +. `docs/echo-types/paper.adoc` `[EXPAND]` tags 1 (background primer) + and 2 (related-work pass — Granule / QTT, Uustalu–Vene comonads, + coeffects, choreographic types, lens/optic vs witness-transport leg) + cleared. +. `proofs/agda/EchoAbstractionBarrier.agda` lands with the + consumer-side free theorem at the affine instance + the raw-Σ + counter-program. Pinned in `Smoke.agda`, wired into `All.agda`, + cross-linked from `paper.adoc` §"Carrier-parametricity, and the + limits of the conservativity claim". +. A concise comparison artefact (single-page table in + `docs/echo-types/comparators.adoc`) ships, mapping Echo's narrowed + claims onto the Granule / QTT / choreographic / linear neighbourhood + axis-by-axis. Honest about what Echo does NOT do (no graded comonad, + no full universal property, no general parametricity). + +*Artefacts (existing).* Pillars A–D landed (`EchoFiberBridge`, +`EchoPullback`, `EchoSeparating`, `EchoGradedComonad`, `EchoRelModel`). +`paper.adoc` and `types-abstract.adoc` exist as LIVING DRAFT and +submission-ready abstract respectively. + +*Retraction-watch.* Pillar B's pullback is *pointwise, funext-relative* +— never describe it as a categorical universal property. Pillar D is +*carrier-parametricity over a fixed grade poset* — never +"model-independence". The graded structure is a *thin-poset reindexing +modality* — never "graded comonad". These three narrowings are the +load-bearing R-2026-05-18 commitments. + +*Owner / cadence.* Claude session work + author-driven write-up. +Re-checked at every rung consolidation. + +=== Lane 2 [ACTIVE] — Echo-vs-Σ identity claim + +*Load-bearing question.* Can a sceptic, walking the repo cold, +convince themselves that Echo is not just renamed Σ within one +sitting? + +*Bottleneck.* Today's session opened this lane; Track A (synthesis +doc + reviewer-facing AsciiDoc companion + theorem-index aggregates + +gate cross-links) landed in-session. Tracks B + C remain. + +*Close-out criterion (falsifiable).* All three hold: + +. Track B (consumer-side abstraction barrier) — same artefact named in + Lane 1's close-out. (Lane 1 and Lane 2 share this artefact; that is + intentional, not duplication.) +. Track C (per-example raw-Σ counter-programs) lands as + `proofs/agda/examples/EchoVsSigma.agda`, pairing each headline + example with the small Σ-misuse it blocks. Pinned in Smoke. +. The Gate 2 nominee list is re-audited and crosses the *comfortable* + threshold (≥ 3 of 4 surviving), not merely the honest minimum. + +*Artefacts (landed today).* `core/skepticisms/is-this-just-sigma-types.md` +(canonical answer doc, 5-section structure mirroring the demands); +`docs/echo-types/sigma-distinctness-map.adoc` (AsciiDoc reviewer +companion); `docs/theorem-index.md` (no-section and degrade-law +aggregate rows); cross-link from `roadmap-gates.adoc` Gate 2 and +`docs/characteristic.adoc` §"Inherited spec". + +*Retraction-watch.* Demand 3 ("categorical universality") must stay +narrowed — no unique-mediator claim. Demand 4 ("parametricity") must +be *consumer-side at the affine instance*, not full Reynolds. See +respective §s in the synthesis doc. + +=== Lane 3 [PARALLEL, NOT LOAD-BEARING] — Ordinal / Buchholz + +*Echo Core does NOT depend on this lane.* This is a separate +proof-theoretic research project that happens to share the +repository. Treat as parallel-independent; Lane 1 progress is never +gated on Lane 3 progress, and the README + roadmap surface the two as +separate branches. + +*Bottleneck.* Unbudgeted `_<ᵇʳᶠ_` global well-foundedness; 10/13 +constructors closed via the budgeted route + `_<ᵇ⁰_` umbrella per the +2026-05-20 evening session; 3 constructor cases (`<ᵇ-ψα`, `<ᵇ-ψΩ≤`, +`<ᵇ-+1` joint-bplus) remain open under documented structural blockers +(see `docs/echo-types/buchholz-rank-obstruction.adoc`). + +*Close-out criterion.* Either: + +* the three open constructor cases close via ψ-admissibility rank + refinement + leading-Ω-index domination (planned closure work; ~3 + follow-on slices), unblocking full `rank-pow-mono-<ᵇ⁻` umbrella and + thereby `wf-<ᵇʳᶠ`; OR +* a falsifiable verdict lands stating that the unbudgeted promotion + cannot close under `--safe --without-K` for the current `_<ᵇ_`, + with the WfCNF-restricted `_<ᵇ⁻_` accepted as the final form. + +*Artefacts.* See `docs/buchholz-plan.adoc` and the `Ordinal/Buchholz/` +subtree. Per-session ledger in CLAUDE.md §"Session arc 2026-05-20". + +*Status.* Continue on parallel branches. Lane 1 does not wait. + +=== Lane 4 [PARKED] — Bridges-CI + +*Unblocking condition.* Lane 1 closes. + +*Scope question to resolve when unparking.* End-to-end verified +bridges to Janus, Tropical, CNO, etc. currently sit as in-tree +modules (`EchoJanusBridge.agda`, `EchoTropical.agda`, `EchoCNOBridge.agda`, +`DyadicEchoBridge.agda`) without CI-verified round-trips against the +target codebases. Two architectural options when unparking: + +* A separate `echo-bridges-ci` repository pulling echo-types and each + target as submodules; runs the verified-translation lemmas in its + own CI. Preserves `--safe --without-K` here. +* In-tree submodules of the target repos. Tighter coupling but + degrades the safety invariants this repo currently maintains. + +The first option is preferred unless the user's broader-research-plan +priorities (per 2026-05-26) explicitly favour tighter integration. + +=== Lane 5 [PARKED] — Tutorial / pedagogy + +*Unblocking condition.* Lane 1 closes, OR a single "killer +application" example emerges that justifies a tutorial track on its +own merit. + +*Candidate killer example (suggested 2026-05-26).* A certified +region-exit audit, modelled on ephapax L3's region-based memory +discipline, where every `S_Region_Exit` produces a *consumed* Linear +Echo with a machine-checked audit guarantee. Concrete, ties to an +adjacent active project, demonstrates the affine-mode discipline at +a real audit boundary. + +*Scope-when-unparking.* `tutorial/` directory with 3 walkthroughs: +(1) the certified region-exit audit; (2) epistemic erasure (with +explicit framing: Echo proves no section recovers the key, NOT that +in-memory bytes are zeroed — conflating these is a category error a +sceptic will catch); (3) provenance / debugging echo over a small +state-reconstruction example. + +== Closed lanes + +(none yet — populated when a lane closes per its close-out criterion). + +== Gates summary + +Pointer-only; see `roadmap-gates.adoc` for the full statements, +adjacency tests, and failure actions. + +* *Gate 1.* Distinct phenomenon. Artefact: `docs/adjacency/`. + Failure action: drop identity claim; retain as Agda exposition. +* *Gate 2.* Characteristic theorem family. Artefact: + `docs/characteristic.adoc`. Failure action: drop claim of a distinct + theorem family; modules remain. +* *Gate 3.* Canonical examples. Artefact: `proofs/agda/examples/`. + Failure action: reframe as theoretical scaffolding awaiting + application. + +== Pillar status (establishment plan) + +Pointer summary; see `docs/echo-types/establishment-plan.adoc` for the +five-pillar plan and `docs/retractions.adoc` R-2026-05-18 for the +narrowings. + +[cols="1,2,4", options="header"] +|=== +| Pillar | Status | Artefact / note + +| A — Pin the identity +| LANDED (2026-05-17) +| `EchoFiberBridge.echo↔fib` — definitional homotopy fibre identity, `refl` round-trips. + +| B — Universal property +| LANDED, NARROWED +| `EchoPullback.echo-pullback-univ` — *pointwise, funext-relative* mediator (not full universal property; see R-2026-05-18). `EchoGradedComonad` — three laws under thin-poset reindexing (not a graded comonad). + +| C — Separating model +| LANDED (2026-05-17) +| `EchoSeparating.sep-degrade-compose-fails` — characteristic law refuted at `true ≢ false` when `≤g-prop` removed. + +| D — Second model + carrier-parametricity +| LANDED, NARROWED +| `EchoRelModel.GradedLossModel` + generic `GCLaws` — *carrier-parametricity over a fixed grade poset* (not model-independence; see R-2026-05-18). `conservativity.adoc` — evidence-for, not proof-of, conservativity. + +| E — External validation (paper + outreach) +| IN PROGRESS +| `docs/echo-types/paper.adoc` LIVING DRAFT with `[EXPAND]` tags; `types-abstract.adoc` submission-ready. Lane 1's close-out criterion governs. +|=== + +== Historical milestone log (M1–M13) + +The structural milestones that built the suite. Retained for +provenance; not load-bearing for ongoing lane planning. + +[cols="1,3,2", options="header"] +|=== +| ID | Milestone | Status + +| M1 | Foundation: core `Echo.agda` functoriality | DONE +| M2 | Characteristic theorem pack (`EchoCharacteristic.agda`) | DONE (2026-04-18) +| M3 | Residue formalisation (`EchoResidue.agda`) | DONE (2026-04-18) +| M4 | Example suite (`EchoExamples.agda`) | DONE (2026-04-18) +| M5 | Assessment report (`docs/assessment.adoc`) | DONE (2026-04-18) +| M6 | Choreographic bridge (`EchoChoreo.agda`) | DONE (2026-04-18) +| M7 | Epistemic bridge (`EchoEpistemic.agda`) | DONE (2026-04-18) +| M8 | Linear/affine bridge (`EchoLinear.agda`) | DONE (2026-04-18) +| M9 | Graded bridge (`EchoGraded.agda`) | DONE (2026-04-18) +| M10 | Tropical bridge (`EchoTropical.agda`) | DONE (2026-04-18) +| M11 | Full-suite gate (`All.agda` + clean build) | DONE (2026-04-18) +| M12 | Cross-bridge integration (`EchoIntegration.agda`) | DONE (2026-04-18) +| M13 | Headline-theorem smoke gate (`Smoke.agda`) | DONE (2026-04-19) +|=== + +Per-rung session ledger lives in CLAUDE.md §"Current rung state". The +ordinal-track E-series milestones (E1–E7) live there. + +== Deferred research track + +Open synthesis problems graduated from `docs/next-questions.adoc`. +Dissertation-scale or requiring extensions beyond the current +`--safe --without-K` core. Each entry records the gap, what would +close it, and why it is parked. + +=== R1 — Unified dependent linear + choreographic + epistemic calculus + +* *Gap.* Bridges exist pairwise but not as one typed calculus + enforcing usage discipline + role projection + knowledge operators + simultaneously. +* *Closure.* A core syntax/judgment layer with preservation/progress metatheory tying the three disciplines together. -* Difficulty: extremely hard. Parked: this is the main synthesis target; - not advanced in single sessions. - -R2. Cubical or quotient treatment of indistinguishability - -* Gap: indistinguishability is currently set-level/propositional; rich - observational equivalence classes need first-class identity handling. -* Closure: a quotient-aware or cubical extension with proofs that echo - constructions commute with equivalence-class semantics. -* Difficulty: very hard. Parked: requires moving off plain - `--safe --without-K` into cubical agda or a heavy quotient layer. -* Current tooling stance (2026-04-23): -** active development remains plain Agda with the standard library -** if `R2` is activated, the first extension to try is Agda's - `--cubical` mode plus the separate Cubical Agda library -** `RedPRL`, `redtt`, and `cooltt` are tracked as adjacent cubical - systems, not as primary tooling for this roadmap; see - `docs/adjacency/cubical-systems.adoc` - -R3. Probabilistic epistemic echoes - -* Gap: no probability/distribution layer over echoes; evidence is +* *Difficulty.* Extremely hard. The main synthesis target; not + advanced in single sessions. Closely aligned with Lane 1's + external-recognition goal — if R1 ever opens as an active lane, it + would likely subsume Lane 1. + +=== R2 — Cubical or quotient treatment of indistinguishability + +* *Gap.* Indistinguishability is currently set-level / propositional; + rich observational equivalence classes need first-class identity + handling. +* *Closure.* A quotient-aware or cubical extension with proofs that + echo constructions commute with equivalence-class semantics. +* *Difficulty.* Very hard. Parked: requires moving off plain + `--safe --without-K` into cubical Agda or a heavy quotient layer. +* *Current tooling stance (2026-04-23).* Active development remains + plain Agda with the standard library. If R2 activates, the first + extension to try is Agda's `--cubical` mode plus the separate + Cubical Agda library. `RedPRL`, `redtt`, and `cooltt` are tracked + as adjacent cubical systems, not as primary tooling; see + `docs/adjacency/cubical-systems.adoc`. + +=== R3 — Probabilistic epistemic echoes + +* *Gap.* No probability/distribution layer over echoes; evidence is binary, not weighted. -* Closure: distribution-valued observation semantics, posterior-style +* *Closure.* Distribution-valued observation semantics, posterior-style residue objects, plus stability/transport theorems. -* Difficulty: very hard. Parked: needs a measure/distribution - formalisation that the current core deliberately avoids. +* *Difficulty.* Very hard. Parked: needs a measure/distribution + formalisation the current core deliberately avoids. -R4. Tropical optimization beyond toy candidate sets +=== R4 — Tropical optimisation beyond toy candidate sets -* Gap: tropical development is finite/toy-level (3-element `Candidate` - set, hand-built `IsArgmin`). -* Closure: scalable tropical witness/certificate framework with - composition laws and integration with graded degradation, generalised - over arbitrary finite candidate sets. -* Difficulty: hard. Smallest-step start: lift `IsArgmin` over an +* *Gap.* Tropical development is finite/toy-level (3-element + `Candidate` set, hand-built `IsArgmin`). +* *Closure.* Scalable tropical witness/certificate framework with + composition laws and integration with graded degradation, + generalised over arbitrary finite candidate sets. +* *Difficulty.* Hard. Smallest-step start: lift `IsArgmin` over an arbitrary `Fin n`-indexed score family; compose with `degrade`. -== Operating Rules +== Lane discipline rules + +. *Cap.* 5 open lanes maximum. Opening a 6th requires closing or + parking another. +. *Close-out upfront.* Every lane row carries a falsifiable + close-out criterion when opened. Vague criteria are rejected. +. *Audit cadence.* Each lane is reviewed at every rung consolidation + (CLAUDE.md §"Rung-consolidation policy"). Closed lanes move to + §"Closed lanes" with the closing artefact named. +. *Parking discipline.* A parked lane keeps its number and gets a + `[PARKED]` tag with the explicit unblocking condition. Parked + lanes still count against the cap. +. *Retraction discipline.* Any lane that touches a R-2026-05-18 + narrowed claim must carry a *retraction-watch* line listing the + narrowings it must respect. Re-opening a retracted claim requires + a new audit recorded in `docs/retractions.adoc`. +. *Load-bearing ordering.* Lanes are not equal. Lane 1 is the + load-bearing lane as of 2026-05-26 (expeditious type-theoretic + grounding); other lanes do not gate Lane 1 unless explicitly + marked as dependencies. + +== Operating rules * No postulates unless explicitly isolated and justified. +* `--safe --without-K` throughout the core; cubical / `--cubical` + reserved for R2 if activated. * Keep universe levels explicit where needed. * Keep proofs minimal and computationally meaningful. * Every edit ends with an Agda compile command and captured output. +* Every headline theorem is pinned in `Smoke.agda` via `using` clause. +* Every new module goes into `All.agda` as an `open import` so the + verified suite covers it. Orphan modules that compile but are not + in `All.agda` are treated as dead code. +* Per-module Smoke pins use their own `using` block with a header + comment, not shared paren-blocks (cuts merge-conflict noise in + swarm-merge sequences). From 13837ccad8f6864d4f02a9d31df5820ff5a01d08 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 26 May 2026 23:02:31 +0100 Subject: [PATCH 03/10] feat(echo-abstraction-barrier): Track B + comparators + Lane 1 close-out updates (#119) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Stacked on top of #118 (consolidation). Closes 2 of 3 Lane 1 close-out items from the new `roadmap.adoc`. The third (paper.adoc `[EXPAND]` tag 2 — related-work pass) remains open; the background-primer tag was confirmed already cleared by PR #73 (2026-05-20). ## Track B — Consumer-side abstraction barrier New `proofs/agda/EchoAbstractionBarrier.agda` with two theorems: - **`affine-consumer-cannot-distinguish`** (positive): any consumer at affine mode assigns the same value to weakened images of the two known-distinct linear echoes. Direct corollary of `affine-all-equal` (the affine residue carrier is contractible). - **`sigma-distinguishes`** (negative companion): the raw Σ-projection `proj₁` IS a consumer that distinguishes `echo-true` from `echo-false`. Exhibits the concrete behaviour the affine interface refuses to export. Together: hiding `proj₁` at affine mode is a structural guarantee, not a convention. Original sketch's Theorem 1 dropped as degenerate. **Build verification:** `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` both exit 0 under `--safe --without-K`, zero postulates, zero funext. Pinned in `Smoke.agda` under own `using` block; wired into `All.agda`. Companion essay `docs/echo-types/abstraction-barrier.adoc` explains the narrow scope: consumer-side free theorem at the headline affine instance — **NOT** general Reynolds parametricity, **NOT** higher-order, **NOT** a categorical universal property. ## Comparators New `docs/echo-types/comparators.adoc` — single-page axis-by-axis comparison of Echo (narrowed) vs four neighbours: Granule, Atkey QTT, Hirsch et al. choreographic types, Linear Haskell. Six axes (primary discipline / judgmental level / categorical anchor / composition law shape / what enforced / what NOT enforced) plus per-comparator subsections plus explicit "What Echo does NOT do" section foregrounding the R-2026-05-18 narrowings. ## Roadmap Lane 1 close-out updates Items 2 (EchoAbstractionBarrier) and 3 (comparators) marked **LANDED 2026-05-26**. Item 1 (paper.adoc tag 2 — related-work) remains the sole open requirement for Lane 1 close-out. ## Retraction discipline R-2026-05-18 respected throughout: no new prose introduces graded-comonad, full-universal-property, model-independence, or general-parametricity claims. EAB essay foregrounds the three narrowings; comparators.adoc "What Echo does NOT do" lists all four retracted framings. ## ⚠️ Separate P0 issue flagged (NOT addressed here) `docs/echo-types/paper.adoc` has **unresolved git merge-conflict markers** at lines 557, 1137, 1156 from merge commit `cab99f1`, with the `== Reframing note (2026-05-18)` section duplicated at lines 1158-1194 and 1207-1243. Currently broken on `main`. Needs its own scoped PR with owner-decision on which chunk to keep (HEAD vs `docs/rule-out-2cat-and-roadmap-correction`). ## Test plan - [x] `agda proofs/agda/EchoAbstractionBarrier.agda` exits 0 under `--safe --without-K` - [x] `agda proofs/agda/Smoke.agda` exits 0 (pin verified) - [x] `agda proofs/agda/All.agda` exits 0 (wire verified) - [ ] AsciiDoc rendering of `docs/echo-types/abstraction-barrier.adoc` and `docs/echo-types/comparators.adoc` is well-formed - [ ] No new postulates introduced (grep) Net diffstat: +585 / -14 across 6 files. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) --- docs/echo-types/abstraction-barrier.adoc | 184 +++++++++++++++ docs/echo-types/comparators.adoc | 270 +++++++++++++++++++++++ proofs/agda/All.agda | 1 + proofs/agda/EchoAbstractionBarrier.agda | 101 +++++++++ proofs/agda/Smoke.agda | 9 + roadmap.adoc | 34 +-- 6 files changed, 585 insertions(+), 14 deletions(-) create mode 100644 docs/echo-types/abstraction-barrier.adoc create mode 100644 docs/echo-types/comparators.adoc create mode 100644 proofs/agda/EchoAbstractionBarrier.agda diff --git a/docs/echo-types/abstraction-barrier.adoc b/docs/echo-types/abstraction-barrier.adoc new file mode 100644 index 0000000..56d95a5 --- /dev/null +++ b/docs/echo-types/abstraction-barrier.adoc @@ -0,0 +1,184 @@ += The Echo abstraction barrier (consumer-side, narrow scope) +:toc: macro +:toclevels: 2 +:sectnums: +:sectnumlevels: 2 +:icons: font + +[.lead] +Companion essay to `proofs/agda/EchoAbstractionBarrier.agda`. The +module ships two theorems and a deliberately narrow scope. This file +explains the narrowness — what the abstraction barrier is, what it +guarantees, what it does *not* guarantee, and why the narrow form is +the strongest honest statement available under +`--safe --without-K`. + +[IMPORTANT] +==== +This is Track B of the "Echo ≠ Σ" identity-claim consolidation +(`roadmap.adoc` §Lane 2; sceptic-facing map at +`core/skepticisms/is-this-just-sigma-types.md` §4). The theorems below +respect the R-2026-05-18 retraction discipline: the claim is a +*consumer-side free theorem at the headline affine instance*, NOT a +general Reynolds-style parametricity result. The scope narrowness is +load-bearing. +==== + +toc::[] + +== What an abstraction barrier means here + +A raw dependent pair `Σ A (λ x → f x ≡ y)` exposes `proj₁`. A consumer +of such a pair can always recover the original `x`. That makes the +"forgetting" half of any loss-grade story a *convention*, not a +guarantee — nothing in the type stops the consumer from looking. + +The Echo interface, at the affine mode, refuses to export `proj₁`. +But "refuses to export" is meaningless prose without a checked +artefact: a sceptic reasonably asks "what stops me writing +`proj₁ ∘ to-sigma`?" The abstraction barrier is the answer. It is +the pair of theorems that, together, say: + +. *At the affine instance, no consumer can do what the Σ-projection + does.* (Theorem `affine-consumer-cannot-distinguish`.) +. *The Σ-projection does it.* (Theorem `sigma-distinguishes`.) + +The first is the guarantee. The second is the negative companion that +makes the guarantee non-trivial: it exhibits the concrete behaviour +the affine interface is designed to prevent. + +== The two theorems + +=== `affine-consumer-cannot-distinguish` + +[source,agda] +---- +affine-consumer-cannot-distinguish : + {X : Set ℓ} (g : LEcho affine → X) → + g (weaken echo-true) ≡ g (weaken echo-false) +affine-consumer-cannot-distinguish g = + cong g (affine-all-equal (weaken echo-true) (weaken echo-false)) +---- + +Any consumer `g` at the affine mode produces the same result on the +two known-distinct linear echoes (`echo-true` and `echo-false`) after +they have been weakened. This holds *for every consumer type* `X` and +*every function* `g : LEcho affine → X`, because the affine residue +carrier is contractible — `EchoLinear.affine-canonical` and +`affine-all-equal` discharge it in one `cong`. + +The reason this is non-trivial: the underlying linear echoes ARE +distinguishable. `EchoCharacteristic.echo-true≢echo-false` is a +theorem. The barrier is that crossing from linear to affine via +`weaken` collapses the distinction *structurally*, and no affine +consumer can recover it. The Σ-projection on the linear side would +recover it; the Σ-projection on the affine side cannot, because the +affine carrier has only one inhabitant up to definitional equality. + +=== `sigma-distinguishes` + +[source,agda] +---- +sigma-distinguishes : + Σ (Echo collapse tt → Bool) + (λ g → g echo-true ≢ g echo-false) +sigma-distinguishes = proj₁ , true≢false +---- + +The Σ-projection `proj₁ : Echo collapse tt → Bool` IS a consumer that +distinguishes `echo-true` from `echo-false`. The proof is `true≢false` +directly, because `proj₁ (echo-intro collapse true)` reduces +definitionally to `true` (via `echo-intro f x = x , refl`) and the +mirror case reduces to `false`. + +This is the load-bearing artefact. Without it, the claim "the affine +interface refuses `proj₁`" is content-free — what would `proj₁` even +do? The negative companion answers exactly that question, and the +answer is "distinguish the two linear echoes". The affine interface +deliberately refuses to export it. + +== What this is NOT + +The scope guardrail in the module preamble lists three narrowings. +They are repeated here in essay form because external readers tend to +read essays before module headers, and the narrowings are the most +load-bearing thing about this module. + +=== Not full Reynolds parametricity + +A general Reynolds-style result would say: for every consumer type +`X`, every echo carrier `A`, every map `f : A → B`, every output +`y : B`, and every function `g : Echo f y → X` *at the appropriate +interface*, `g` cannot inspect `x` beyond what the interface allows. +Agda has no parametricity primitive. Stating this requires either an +axiom or a paper-level metatheorem. Both violate the no-postulate +invariant. + +The narrow form here — consumer-side at the headline affine instance +— is what survives `--safe --without-K`. It says the right thing at +the one instance where the carrier is contractible and the +quantification over consumers (`{X : Set ℓ}`) is non-vacuous because +*every* consumer satisfies the equation. + +=== Not a higher-order parametricity claim + +`affine-consumer-cannot-distinguish` does not claim that consumers +*cannot detect the difference between two linear preimages*. It +claims that consumers *of weakened linear preimages* assign them the +same value. The detection happens on the linear side (and is the +content of `echo-true≢echo-false`); the barrier is at the +linear→affine boundary, and the theorem is what survives crossing it. + +=== Not a categorical universal property + +The Echo interface is not characterised in this module as a terminal +cone over anything. The pullback characterisation lives in +`EchoPullback.agda` and is itself narrowed (per R-2026-05-18) to a +funext-relative pointwise mediator property. The abstraction barrier +here is a separate, narrower claim that does not depend on the +pullback machinery. + +== Why two theorems and not one + +A single positive theorem (`cannot-distinguish`) is a wish without +the negative companion. The reader can always ask: "but couldn't some +other consumer, written cleverly, distinguish them anyway?" The +answer at the affine instance is *no*, and the reason is structural +(`affine-canonical`). But the reader's question deserves a checked +answer, not a structural argument. The negative companion provides +it: the only consumer that distinguishes the two linear echoes is +`proj₁` or a function of `proj₁`, and that is *exactly* the function +the affine interface refuses to export. + +The pair is the artefact. Either alone is half the story. + +== Honest comparison to neighbour disciplines + +* *Granule / QTT.* Stronger general parametricity available via the + language's quantitative judgments. Echo's claim here is narrower + (instance-level, consumer-side, in Agda without a parametricity + primitive). See `docs/echo-types/comparators.adoc` for the + axis-by-axis breakdown. +* *Linear Haskell.* The linearity-mode information is at the type + level but Haskell consumers can still inspect linear values via + `seq` and other escape hatches. Echo's contractibility argument + closes that gap at the affine carrier specifically, because the + carrier *is* a singleton up to definitional equality. +* *Lens / optic laws.* The witness-transport leg of `map-over` looks + optic-shaped but the affine-mode contractibility argument has no + optic analogue: lenses can inspect their source via `view`. Echo's + refusal of `proj₁` at affine mode is the structural difference. + +== Cross-references + +* Agda module: `proofs/agda/EchoAbstractionBarrier.agda` (this file's + companion). +* Sceptic-facing map: `core/skepticisms/is-this-just-sigma-types.md` + §4 and `docs/echo-types/sigma-distinctness-map.adoc` §"Demand 4". +* The retraction governing the narrowing discipline: + `docs/retractions.adoc` R-2026-05-18. +* Carrier-parametricity (model side): `EchoRelModel.agda` and + `docs/echo-types/conservativity.adoc`. That work is at the *model* + level (Pillar D); this module is at the *consumer* level — the two + are not the same statement. +* Comparator framing: `docs/echo-types/comparators.adoc`. diff --git a/docs/echo-types/comparators.adoc b/docs/echo-types/comparators.adoc new file mode 100644 index 0000000..39ab9b1 --- /dev/null +++ b/docs/echo-types/comparators.adoc @@ -0,0 +1,270 @@ += Echo Types vs. Adjacent Type Systems: Axis-by-Axis Comparison +:toc: macro +:toclevels: 2 +:sectnums: +:sectnumlevels: 2 +:icons: font + +[.lead] +Single-page comparison of Echo Types (narrowed per R-2026-05-18) +against the four nearest neighbouring type systems: Granule (graded +modalities), Atkey QTT (Quantitative Type Theory), Hirsch et al. +choreographic types, and Linear Haskell. This is Lane 1 close-out +artefact #3 per `roadmap.adoc`. The discipline below is *no +overclaim*: where Echo is weaker than a comparator, that is stated +plainly. + +[IMPORTANT] +==== +*Honest framing.* This doc does NOT claim Echo subsumes any of these +systems. It claims Echo *occupies an adjacent niche* on the +information-loss axis, that its narrowed claims are concrete and +checkable, and that the per-comparator differences are mostly +*structural* (different judgmental level, different categorical +anchor) rather than competitive. The R-2026-05-18 narrowings apply +throughout: Echo is a thin-poset reindexing modality (not a graded +comonad), with a funext-relative pointwise mediator (not a full +universal property) and carrier-parametricity over a fixed grade +poset (not model-independence). +==== + +toc::[] + +== Side-by-side axis table + +[cols="2,2,2,2,2,2", options="header"] +|=== +| Axis | Granule | Atkey QTT | Choreographic (Hirsch et al.) | Linear Haskell | Echo (narrowed) + +| Primary discipline +| Graded modality `□_r A` +| Quantity `0 / 1 / ω` on bindings +| Role-projected processes +| Linearity on function arrows +| Information loss along non-injective maps + +| Judgmental level +| New judgment (coeffect) +| New judgment (resource use count) +| New projection / endpoint judgment +| New arrow type (`%1 →`) +| *Derived Σ-type* — no new judgment + +| Categorical anchor +| Graded comonad on a coeffect category +| LCC with quantitative semiring action +| Symmetric monoidal endpoint categories / projection +| Symmetric monoidal closed (linearity fragment) +| *Homotopy fibre + thin-poset reindexing* (definitional; pointwise pullback) + +| Composition law shape +| `□_r (□_s A) → □_{r·s} A` (graded comonad multiplication) +| Quantity addition + scaling on binders +| Choreographic transport along role morphisms +| Multiplicity tracking through `let`/`case` +| `degrade : ≤g → GEcho → GEcho` (single thin-poset reindex; *no* nested `D_r D_s`) + +| What is enforced +| Quantitative resource use; coeffect-graded function purity +| Use-count of every binding at compile time +| Role-consistent communication; deadlock-freedom +| Single-use of linear values; resource discipline +| At affine mode: consumer cannot distinguish two preimages of the same output (`affine-consumer-cannot-distinguish`) + +| What is NOT enforced (relevant to comparison) +| — +| — +| — +| Linearity is *erasable*; affine mode not standard +| General parametricity (Agda has no primitive); full universal property; nested `D_r D_s`; sectionability of `weaken` +|=== + +== Per-comparator subsections + +=== Granule (Orchard, Liepelt, Eades et al.) + +*Closest similarity.* Both Granule and Echo carry a grade lattice and +a monotone reindexing operation. Granule's `□_r A` is a graded +modality with a coeffect algebra; Echo's `GEcho g` carries a +loss-grade `g` with a `degrade : ≤g → GEcho → GEcho` reindex. + +*Key difference.* Granule ships a *full graded comonad*: counit, +duplication into `□_{r·s} (□_s A)`, the multiplication law, the +coassociativity diagram. Echo originally claimed this and *walked it +back* (R-2026-05-18). Echo's current honest structure is a *thin-poset +reindexing modality* — the grade order is propositional (`≤g-prop`), +so the would-be coassociativity transport `subst GEcho (⊔g-assoc …)` +is forced to vanish via the common-upper-bound idiom. No nested +`D_r D_s` is ever formed. The separating model +(`EchoSeparating.agda`) makes this precise: removing the single +hypothesis `≤g-prop` breaks the composition law at a checked +`true ≢ false`. + +*Honest verdict.* Granule is stronger on the modality axis — it is a +real graded comonad with a real coeffect algebra. Echo is weaker on +that axis *by deliberate retraction*: the path-independence law holds +*for exactly one reason*, and that reason is propositional. Echo's +contribution is on a different axis (information loss with a +no-section dual), not in competition with Granule's coeffect track. + +=== Atkey QTT (Quantitative Type Theory) + +*Closest similarity.* Both QTT and Echo are *derived* type systems — +QTT adds quantity annotations to a dependent type theory without +changing its judgmental structure beyond the resource semiring; Echo +is *definitionally* the homotopy fibre `Σ A (λ x → f x ≡ y)` and adds +no new judgment at all. + +*Key difference.* QTT enforces *use-count* at compile time: a binding +declared at quantity `0` is irrelevant, at `1` is linear, at `ω` is +unrestricted. The discipline is quantitative. Echo enforces +*non-distinguishability at affine mode* via contractibility of the +affine carrier (`affine-canonical`, `affine-all-equal`). The +discipline is informational: the residue is structurally +indistinguishable, not just counted. + +*Honest verdict.* QTT is the closer relative on the +"derived-type-theory" axis. It is stronger on quantitative use +tracking; Echo is stronger on the *consumer-side abstraction barrier* +at the affine instance — see `EchoAbstractionBarrier.sigma-distinguishes` +for the negative companion that makes Echo's affine guarantee +non-trivial. Neither subsumes the other; they decorate the same +fibration with different information. + +=== Choreographic types (Hirsch et al.) + +*Closest similarity.* Both choreographic types and Echo's choreographic +bridge (`EchoChoreo.agda`) carry a notion of role-projected +transport. Echo ships `applyChoreo-compose` — the per-decoration +composition law on the role-reachability order — as one of the +characteristic theorem nominees (`docs/characteristic.adoc`). + +*Key difference.* Choreographic types are a *programming-language +discipline* on distributed processes: the global type projects to +local endpoint types, and well-typedness guarantees deadlock-freedom +under appropriate operational semantics. Echo's role decoration is +*one of five* equivalent decoration layers (graded, linear, +choreographic, access, cost, search) — all instantiations of the same +thin-poset reindexing recipe. Echo does not ship operational +semantics, projection algorithms, or endpoint extraction; it ships +the *information-flow shape* that all five decorations share. + +*Honest verdict.* Choreographic types are dramatically stronger on the +programming-language axis (operational semantics, projection, +implementation). Echo is on a different layer: it shows that the +choreographic *composition* law has the same algebraic shape as the +graded, linear, access, cost, and search composition laws. The +contribution is *abstraction-level*, not language-level. + +=== Linear Haskell + +*Closest similarity.* Both Linear Haskell and Echo's linear bridge +(`EchoLinear.agda`) distinguish linear from non-linear (affine in +Echo's case) consumption. Both ship a degrade operation +(`weaken` in Echo; the implicit linear-to-unrestricted promotion in +Linear Haskell where allowed). + +*Key difference, structural.* Linear Haskell's linearity lives on the +function arrow (`%1 →`) and is *erasable at runtime*. The linearity +discipline is a compile-time check against multiplicity tracking +through `let` and `case`; nothing structural in the runtime +representation prevents `seq` or other inspection. Echo's +contractibility argument (`affine-canonical`) is *structural at the +type level*: the affine carrier has exactly one inhabitant up to +definitional equality, so even at the value level no consumer can +distinguish two preimages. + +*Key difference, scope.* Linear Haskell does not ship a no-section +family. Echo's `no-section-weaken` (which is `no-section-collapse-to-residue`) +proves that *no* function `LEcho affine → LEcho linear` is a section +of `weaken` — the up-step is provably not just unavailable but +non-existent. + +*Honest verdict.* Linear Haskell is the more useful programming tool; +Echo's affine layer is the more rigorous proof-theoretic object. They +sit in different problem spaces. + +== What Echo does NOT do + +The most credibility-relevant section. Reviewers should not expect +any of the following from Echo: + +* *No graded comonad.* `degrade-via-join` and `degrade-compose` are + thin-poset reindexing laws under a propositional order. No nested + `D_r D_s` is ever formed; no comonad multiplication exists. The + retracted "graded comonad" framing is documented at + `docs/retractions.adoc` R-2026-05-18. + +* *No full universal property.* `EchoPullback.echo-pullback-univ` + proves only a *pointwise, funext-relative* mediator property + (`∀ v → m' v ≡ m v`), not the full categorical statement + (`m' ≡ m`). The funext-free statement is the strongest form + available under `--safe --without-K`. + +* *No model-independence.* Pillar D's `EchoRelModel.GradedLossModel` + provides *carrier-parametricity over a fixed grade poset* — the + comonad laws (in the narrowed-to-reindexing sense) are proved once + for any model. This is one structure parametric in the carrier, not + multiple independent models agreeing semantically. + +* *No general Reynolds parametricity.* Agda has no parametricity + primitive. `EchoAbstractionBarrier.affine-consumer-cannot-distinguish` + is a *consumer-side free theorem at the headline affine instance*, + not a quantified statement over all consumer types and all echo + carriers. The instance is non-trivial precisely because the affine + carrier is contractible. + +* *No conservativity metatheorem.* `docs/echo-types/conservativity.adoc` + ships a *postulate-free build that is evidence for*, not a + *proof of*, conservativity. The original "irreducibility + metatheorem" framing was retracted in R-2026-05-18. + +* *No unique-mediator universality for bridges.* The bridges + (`EchoJanusBridge`, `EchoTropical`, `EchoCNOBridge`, + `DyadicEchoBridge`, `EchoFiberCount`/`EchoThermodynamics*`) are + *independent witnesses* of Echo as a canonical loss target, not a + single "every loss-tracker maps uniquely into Echo" theorem. Such a + uniqueness result would require funext or an axiom and is out of + scope. + +== What Echo DOES claim + +For balance — the affirmative side of the same discipline: + +* *Definitional homotopy-fibre identity.* `EchoFiberBridge.echo↔fib` + pins `Echo f y` as definitionally equal to `fib f y`, both + round-trips `refl`. Owning the deflationary admission is a + credibility asset. + +* *No-section family across 5 decoration layers.* See the aggregate + row in `docs/theorem-index.md`. Each decoration *separately* + refuses the section that a raw Σ would admit. + +* *Per-decoration composition law lands by the same recipe in + 6 layers.* graded, linear/affine, choreographic, access, cost, + search. See `degrade-laws` aggregate row in `theorem-index.md`. + +* *Consumer-side abstraction barrier at the affine instance.* The + Echo interface at affine mode does not export `proj₁`, and that + refusal is structurally enforced by the contractibility of the + affine carrier. The Σ-projection counter-program in + `EchoAbstractionBarrier.sigma-distinguishes` is the concrete + artefact that makes the refusal non-trivial. + +* *Five-pillar establishment programme.* Pillars A–D landed (with + narrowings); E in progress. See `docs/echo-types/establishment-plan.adoc`. + +== Cross-references + +* The retraction discipline that governs the narrowed claims here: + `docs/retractions.adoc` R-2026-05-18. +* Sceptic-facing answer to the "is this just Σ?" question, organised + under five demands: `core/skepticisms/is-this-just-sigma-types.md` + and `docs/echo-types/sigma-distinctness-map.adoc`. +* The abstraction-barrier theorems referenced above: + `proofs/agda/EchoAbstractionBarrier.agda` + + `docs/echo-types/abstraction-barrier.adoc`. +* Establishment-plan thesis and the five pillars: + `docs/echo-types/establishment-plan.adoc`. +* Lane 1 close-out criterion: `roadmap.adoc` §Lane 1. This + comparator artefact is item #3 of three. diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 34f270f..e3777ff 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -15,6 +15,7 @@ open import EchoExamples open import EchoChoreo open import EchoEpistemic open import EchoLinear +open import EchoAbstractionBarrier open import EchoGraded open import EchoTropical open import AntiEchoTropical diff --git a/proofs/agda/EchoAbstractionBarrier.agda b/proofs/agda/EchoAbstractionBarrier.agda new file mode 100644 index 0000000..ab6ba8b --- /dev/null +++ b/proofs/agda/EchoAbstractionBarrier.agda @@ -0,0 +1,101 @@ +{-# OPTIONS --safe --without-K #-} + +-- Track B of the "Echo ≠ Σ" identity-claim consolidation +-- (`roadmap.adoc` §Lane 2; sketch at +-- `core/skepticisms/is-this-just-sigma-types.md` §4 and +-- `docs/echo-types/sigma-distinctness-map.adoc` §"Demand 4"). +-- +-- Scope guardrail (load-bearing — read before any prose claim about +-- this module). This module ships a CONSUMER-SIDE FREE THEOREM AT THE +-- HEADLINE AFFINE INSTANCE (`LEcho affine = EchoR ⊤ TrivialCert tt`). +-- It is NOT a general Reynolds-style parametricity result. Agda has +-- no parametricity primitive, and a statement quantifying over all +-- consumer types `X` and all echo carriers would require either an +-- axiom or a paper-only proof — both violate the no-postulate +-- invariant. The honest claim is: at the affine instance the residue +-- carrier is contractible (`EchoLinear.affine-canonical`), so every +-- consumer factors through that contraction and provably cannot +-- distinguish two known-distinct linear preimages. This is the +-- strongest statement available inside `--safe --without-K` without +-- funext. +-- +-- The module ships two theorems: +-- +-- `affine-consumer-cannot-distinguish` — POSITIVE: any +-- `g : LEcho affine → X` assigns the same value to the weakened +-- images of `echo-true` and `echo-false`. Direct corollary of +-- `affine-all-equal`. This is what the Echo interface GUARANTEES +-- that raw Σ does not. +-- +-- `sigma-distinguishes` — NEGATIVE: the raw Σ-projection `proj₁` +-- IS a consumer that distinguishes `echo-true` from `echo-false`. +-- Exhibiting this concrete counter-program makes the abstraction +-- barrier a checked artefact, not a wish: the Echo interface +-- refuses to export `proj₁` *exactly because* `sigma-distinguishes` +-- shows what would happen if it did. +-- +-- Together they say: hiding `proj₁` is a guarantee, not a convention. +-- +-- Honest framing notes: +-- * "Theorem 1" (consumer factorisation) from the original sketch was +-- dropped — its only statable form was `g (weaken e) ≡ g (weaken e)`, +-- degenerate. The real content lives in T2 + T3. +-- * The R-2026-05-18 narrowing applies. The graded structure is a +-- thin-poset reindexing modality, not a graded comonad. The +-- abstraction here is consumer-side at the affine instance, not +-- relational parametricity over the model. + +module EchoAbstractionBarrier where + +open import Echo using (Echo) +open import EchoCharacteristic + using (collapse; echo-true; echo-false; true≢false) +open import EchoLinear + using ( Mode; linear; affine; LEcho + ; weaken + ; affine-all-equal + ) + +open import Data.Bool.Base using (Bool) +open import Data.Product.Base using (Σ; _,_; proj₁) +open import Data.Unit.Base using (⊤; tt) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl; cong) +open import Relation.Nullary using (¬_) +open import Level using (Level) + +private variable + ℓ : Level + +---------------------------------------------------------------------- +-- Theorem 2 (positive). Any consumer at the affine mode assigns the +-- same value to the weakened images of the two known-distinct linear +-- echoes. +-- +-- Direct corollary of `affine-all-equal` (`EchoLinear.agda:57-58`), +-- which is itself a corollary of `affine-canonical` — the affine +-- residue carrier is contractible. Hence `cong g` of the canonical +-- equality discharges the theorem in one line. + +affine-consumer-cannot-distinguish : + {X : Set ℓ} (g : LEcho affine → X) → + g (weaken echo-true) ≡ g (weaken echo-false) +affine-consumer-cannot-distinguish g = + cong g (affine-all-equal (weaken echo-true) (weaken echo-false)) + +---------------------------------------------------------------------- +-- Theorem 3 (negative companion — the raw-Σ counter-program). +-- `proj₁ : Echo collapse tt → Bool` is a consumer over the *raw* Σ +-- encoding that distinguishes the two linear echoes. Its existence is +-- what the Echo interface (at affine mode) is designed to prevent +-- exporting: T2 above guarantees no affine-mode consumer can match +-- this behaviour. +-- +-- The proof is `true≢false` directly, because `proj₁ echo-true` +-- reduces definitionally to `true` (via `echo-intro f x = x , refl`) +-- and `proj₁ echo-false` reduces to `false`. + +sigma-distinguishes : + Σ (Echo collapse tt → Bool) + (λ g → g echo-true ≢ g echo-false) +sigma-distinguishes = proj₁ , true≢false diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 3b280d5..97780ae 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -369,6 +369,15 @@ open import EchoLinear using ; degradeMode-via-join ) +-- EchoAbstractionBarrier — Track B of the Echo-vs-Σ identity claim. +-- Consumer-side free theorem at the affine instance + raw-Σ +-- counter-program. See `roadmap.adoc` §Lane 2 and +-- `core/skepticisms/is-this-just-sigma-types.md` §4. +open import EchoAbstractionBarrier using + ( affine-consumer-cannot-distinguish + ; sigma-distinguishes + ) + open import EchoGraded using ( Grade ; degrade diff --git a/roadmap.adoc b/roadmap.adoc index fcf37b0..c0689ea 100644 --- a/roadmap.adoc +++ b/roadmap.adoc @@ -113,20 +113,26 @@ objection. *Close-out criterion (falsifiable).* All three hold: -. `docs/echo-types/paper.adoc` `[EXPAND]` tags 1 (background primer) - and 2 (related-work pass — Granule / QTT, Uustalu–Vene comonads, - coeffects, choreographic types, lens/optic vs witness-transport leg) - cleared. -. `proofs/agda/EchoAbstractionBarrier.agda` lands with the - consumer-side free theorem at the affine instance + the raw-Σ - counter-program. Pinned in `Smoke.agda`, wired into `All.agda`, - cross-linked from `paper.adoc` §"Carrier-parametricity, and the - limits of the conservativity claim". -. A concise comparison artefact (single-page table in - `docs/echo-types/comparators.adoc`) ships, mapping Echo's narrowed - claims onto the Granule / QTT / choreographic / linear neighbourhood - axis-by-axis. Honest about what Echo does NOT do (no graded comonad, - no full universal property, no general parametricity). +. `docs/echo-types/paper.adoc` `[EXPAND]` tag 2 (related-work pass — + Granule / QTT, Uustalu–Vene comonads, coeffects, choreographic types, + lens/optic vs witness-transport leg) cleared. *(Tag 1, background / + notation primer, cleared 2026-05-20 via PR #73 — section "Background + and notation" in `paper.adoc`, covering type-theoretic setting + + HoTT fibres + coeffect / graded-modality lineage + thin-poset + reindexing modality + notation table, all within the R-2026-05-18 + narrowing.)* +. *LANDED 2026-05-26.* `proofs/agda/EchoAbstractionBarrier.agda` + ships the consumer-side free theorem at the affine instance + (`affine-consumer-cannot-distinguish`) + the raw-Σ counter-program + (`sigma-distinguishes`). Pinned in `Smoke.agda` under own + `using` block; wired into `All.agda`. Full suite exits 0 under + `--safe --without-K`. Companion essay + `docs/echo-types/abstraction-barrier.adoc`. +. *LANDED 2026-05-26.* `docs/echo-types/comparators.adoc` ships the + single-page axis-by-axis comparison of Echo (narrowed) vs Granule, + Atkey QTT, Hirsch et al. choreographic types, and Linear Haskell. + Honest "What Echo does NOT do" section foregrounds the + R-2026-05-18 narrowings. *Artefacts (existing).* Pillars A–D landed (`EchoFiberBridge`, `EchoPullback`, `EchoSeparating`, `EchoGradedComonad`, `EchoRelModel`). From 7234a8b265f7e2898c351360738695e0ed02e167 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 26 May 2026 23:21:00 +0100 Subject: [PATCH 04/10] fix+feat: paper.adoc conflict resolution + related-work [EXPAND] cleared + Track C land (#120) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Stacked on #118. Closes the three remaining session items from the user-prioritised batch: 1. **🔴 P0 — `paper.adoc` merge-conflict resolution** 2. **Lane 1 close-out item 1** — `paper.adoc` `[EXPAND]` tag 2 (related-work pass) cleared 3. **Lane 2 close-out item 2** — Track C (per-example raw-Σ counter-programs) landed ## 1. P0 conflict resolution Three unresolved git conflict markers at `paper.adoc:557,1137,1156` from merge commit `cab99f1` (`reframe/retraction-2026-05-18`). Resolution: - **HEAD chunk** (579 lines, lines 558-1136): substantive proof-size + threats-to-validity + related-work analysis. **Kept verbatim.** - **Incoming chunk** (17 lines, lines 1138-1155): `[EXPAND]` note + 2-cat ruleout note. **Kept verbatim.** - **Conflict markers stripped**, no content lost. - **Duplicate `== Reframing note (2026-05-18)`** at lines 1207-1243 deleted; single canonical copy at lines 1158-1194 retained. Net: paper.adoc 1278 → 1238 lines. Now well-formed AsciiDoc on `main`. ## 2. Related-work `[EXPAND]` tag 2 cleared Discovered both stale TODO notes (related-work expansion + 2-cat ruleout fold-in) had their content **silently delivered** in substantive subsections of `== Related work`: - `=== HoTT homotopy fibres` - `=== Graded comonads, coeffects, and QTT (the lineage we are motivated by, but explicitly not an instance of)` - `=== Lenses and optics (the witness-transport leg)` — already contains the 2-categorical rule-out at lines 948-953 Replaced both stale notes with a single explanatory NOTE pointing at the delivered subsections + `docs/echo-types/comparators.adoc` companion. Lane 1 close-out: only the ordinal-appendix `[EXPAND]` (tag 4) remains, correctly gated on the Bachmann-Howard milestone per design. ## 3. Track C — `proofs/agda/examples/EchoVsSigma.agda` Three lemmas pairing each headline example with the small raw-Σ counter-program the Echo interface refuses to export at affine mode: | Lemma | Distinguishes | |---|---| | `parser-sigma-distinguishes` | `echo-parse-nested` vs `echo-parse-pair` at `parses ≡ true` (via `proj₁` + `paren-nested≢paren-pair`) | | `provenance-sigma-distinguishes` | `echo-prov-true` vs `echo-prov-false` at `project ≡ 0` (via `prov ∘ proj₁` + `true≢false`) | | `absint-sigma-distinguishes` | `echo-pos-p1` vs `echo-pos-p2` at `α ≡ pos` (via `proj₁` + `p1≢p2`) | Mirrors `EchoAbstractionBarrier.sigma-distinguishes` at the per-example level. Together with `EchoAbstractionBarrier.affine-consumer-cannot-distinguish`, establishes the Gate 3 matched-positive + matched-negative pair discipline ("raw Σ would leak; Echo blocks it"). **Build verification:** `agda proofs/agda/All.agda`, `proofs/agda/Smoke.agda`, `proofs/agda/examples/All.agda` all exit 0 under `--safe --without-K`, zero postulates. Wired into `examples/All.agda`; pinned in `Smoke.agda` under own `using` block. ## Roadmap updates - Lane 1: item 1 (related-work) now LANDED; only ordinal-appendix EXPAND tag remains (correctly out-of-scope). - Lane 2: item 2 (Track C) now LANDED. Only item 3 (Gate-2 nominee re-audit ≥3/4 surviving) remains for full Lane 2 close-out. ## Retraction discipline (R-2026-05-18) respected throughout No new prose introduces graded-comonad, full-universal-property, model-independence, or general-parametricity claims. ## Test plan - [x] `agda proofs/agda/All.agda` exits 0 under `--safe --without-K` - [x] `agda proofs/agda/Smoke.agda` exits 0 (new Track C pins verified) - [x] `agda proofs/agda/examples/All.agda` exits 0 (new EchoVsSigma wired) - [x] `agda proofs/agda/examples/EchoVsSigma.agda` typechecks in isolation - [x] Zero conflict markers remain in paper.adoc (`grep -nE '^<<<<<<<|^=======|^>>>>>>>'`) - [x] Single `== Reframing note` section (no duplicate) - [ ] AsciiDoc rendering of paper.adoc + roadmap.adoc is well-formed Net diffstat: +140 / -65 across 5 files. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) --- docs/echo-types/paper.adoc | 74 ++++-------------- proofs/agda/Smoke.agda | 11 +++ proofs/agda/examples/All.agda | 1 + proofs/agda/examples/EchoVsSigma.agda | 104 ++++++++++++++++++++++++++ roadmap.adoc | 15 ++-- 5 files changed, 140 insertions(+), 65 deletions(-) create mode 100644 proofs/agda/examples/EchoVsSigma.agda diff --git a/docs/echo-types/paper.adoc b/docs/echo-types/paper.adoc index a1bbeb0..fd002f7 100644 --- a/docs/echo-types/paper.adoc +++ b/docs/echo-types/paper.adoc @@ -554,7 +554,6 @@ mechanised strength, neither less nor more. === Proof size per pillar -<<<<<<< HEAD The four pillars together occupy ~930 lines across six modules, with zero postulates and three `rewrite` sites (one in the foundational `degrade-compose`; one in its `rel-model` lift; one in @@ -1134,26 +1133,21 @@ Swamy et al. "Dependent types and multi-monadic effects in F\*" (POPL 2016); Vazou–Seidel–Jhala–Vytiniotis–Peyton Jones "Refinement types for Haskell" (ICFP 2014, Liquid Haskell). -======= -NOTE: *[EXPAND]* — detailed positioning against: Granule / QTT graded -modalities; comonadic notions of computation (Uustalu–Vene); -coeffects (Petriček–Orchard–Mycroft); HoTT fibrewise constructions; -lens / optic literature (the witness-transport leg of -`echo-pullback-univ` resembles the very-well-behaved *1-lens* laws — -no 2-cell-equipped optic, see below). Make the novelty crisp: not a -new object, but a fully mechanised characterisation package with a -falsifiable-gate methodology. - -NOTE: *[2-cat ruled out, see `decisions/no-2-cat.adoc`]* — when the -related-work pass expands the lens/optic comparison and the -graded-modality positioning, fold in the 2-categorical rule-out: a -"bicategorical echo" reading was considered and ruled out on the -landed evidence (every would-be 2-cell appears as `refl` or is -prop-forced trivial by `≤g-prop` / `⊑-prop`); the construction -resembles a very-well-behaved *1-lens*, not a 2-cell-equipped optic. -The closure note in `decisions/no-2-cat.adoc` is the load-bearing -artifact; this paragraph should cite it rather than re-argue. ->>>>>>> docs/rule-out-2cat-and-roadmap-correction + +NOTE: *Related-work `[EXPAND]` cleared 2026-05-26.* The original +`[EXPAND]` TODO requested detailed positioning against Granule / QTT +graded modalities, Uustalu–Vene comonads, Petriček–Orchard–Mycroft +coeffects, HoTT fibrewise constructions, and the lens / optic +literature with the 1-lens-vs-2-cell-optic clarification. That work +has been delivered above in §"HoTT homotopy fibres", §"Graded comonads, +coeffects, and QTT", and §"Lenses and optics (the witness-transport +leg)" — including the explicit 2-categorical rule-out at the end of +the lens/optic subsection (`docs/echo-types/decisions/no-2-cat.adoc` +is the load-bearing closure note). A companion single-page comparator +table at `docs/echo-types/comparators.adoc` (Echo vs Granule / QTT / +choreographic / Linear Haskell) ships the axis-by-axis summary form +for reviewers who want the at-a-glance positioning rather than the +prose narrative above. [#reframing-note] == Reframing note (2026-05-18) @@ -1204,44 +1198,6 @@ via a genuine non-graph `StepND` model (§6 NOTE, `EchoStepNDModelF2.agda`). The graded-comonad, modality-level model-independence, and conservativity rows remain fully retracted. -[#reframing-note] -== Reframing note (2026-05-18) - -This draft was reframed after an adversarial three-reviewer review -(graded-modality, semantics, and proof-assistant skeptics) found that -the codebase contains no defense for five central claims, and that -two were contradicted by the repository's own Gate-2 audit. The -following claims were retracted, not weakened cosmetically: - -[cols="2,3", options="header"] -|=== -| Retracted claim | Replaced by - -| "graded comonad" (counit/comultiplication, three comonad laws) -| loss-graded *reindexing modality*; no nested `D_r D_s` is formed; - the equations hold by thinness of the grade order - -| "terminal-cone universal property"; "a category theorist accepts - echo as the limit of a cospan" -| a *pointwise, funext-relative* mediator property; full terminality - is unstatable here without funext - -| "model independence across two agreeing models" -| carrier-parametricity over a *fixed* grade poset; the second model - is the first with a `⊤` component, agreeing by `refl` - -| "conservativity metatheorem, discharged operationally by the build" -| a *postulate-free build*: evidence for, not a proof of, - conservativity over MLTT+Σ - -| "funext quarantined behind an isolated module; no result crosses it" -| no funext anywhere; the real funext-relativity is the pointwise - mediator property, now disclosed as the boundary -|=== - -The full per-attack analysis and the codebase pressure-test are in -`docs/retractions.adoc`. - == Conclusion Echo is the homotopy fibre equipped with a loss-grade lattice, diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 97780ae..1847ed8 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -378,6 +378,17 @@ open import EchoAbstractionBarrier using ; sigma-distinguishes ) +-- examples.EchoVsSigma — Track C of the Echo-vs-Σ identity claim. +-- Per-example raw-Σ counter-programs paired with each headline +-- example (parser, provenance, absint) — the matched-negative +-- companions for Gate 3. See `roadmap.adoc` §Lane 2 close-out +-- item 2. +open import examples.EchoVsSigma using + ( parser-sigma-distinguishes + ; provenance-sigma-distinguishes + ; absint-sigma-distinguishes + ) + open import EchoGraded using ( Grade ; degrade diff --git a/proofs/agda/examples/All.agda b/proofs/agda/examples/All.agda index 2bf668e..7af859b 100644 --- a/proofs/agda/examples/All.agda +++ b/proofs/agda/examples/All.agda @@ -15,3 +15,4 @@ import examples.TropicalArgmin import examples.EpistemicUpdate import examples.LinearErasure import examples.Transport +import examples.EchoVsSigma diff --git a/proofs/agda/examples/EchoVsSigma.agda b/proofs/agda/examples/EchoVsSigma.agda new file mode 100644 index 0000000..c637c01 --- /dev/null +++ b/proofs/agda/examples/EchoVsSigma.agda @@ -0,0 +1,104 @@ +{-# OPTIONS --safe --without-K #-} + +-- Track C of the Echo-vs-Σ identity claim consolidation +-- (`roadmap.adoc` §Lane 2 close-out item 2; companion to +-- `core/skepticisms/is-this-just-sigma-types.md` §5 and +-- `docs/echo-types/sigma-distinctness-map.adoc` §"Demand 5"). +-- +-- For each headline example (parser, provenance, absint), exhibit the +-- small raw-Σ counter-program that the Echo interface refuses to +-- export at affine mode. Each `*-sigma-distinguishes` is the +-- *negative companion* to the positive distinct-echoes-same-y theorem +-- already in the example module: it shows the concrete consumer that +-- would let the bug through if `proj₁` (or anything that factors +-- through it) were exposed. +-- +-- The pattern mirrors `EchoAbstractionBarrier.sigma-distinguishes` at +-- the per-example level. Together with the affine-side guarantee in +-- `EchoAbstractionBarrier.affine-consumer-cannot-distinguish`, these +-- per-example negatives establish the Gate 3 "matched-positive + +-- matched-negative pair" discipline ("raw Σ would leak; Echo blocks +-- it") for each headline example. +-- +-- Scope guardrail: each lemma is a *concrete instance* of the raw-Σ +-- distinguish pattern at the linear-side echo, exhibiting what an +-- unprotected Σ-projection would do with the example's distinct +-- preimages. The corresponding affine-side guarantee that nothing of +-- this shape can exist is the general `affine-consumer-cannot-distinguish`, +-- not re-proven here per-example. + +module examples.EchoVsSigma where + +open import Echo using (Echo) + +open import EchoExampleParser + using ( Token + ; parses + ; paren-pair; paren-nested + ; echo-parse-pair; echo-parse-nested + ; paren-nested≢paren-pair + ) +open import EchoExampleProvenance + using ( Row; project + ; echo-prov-true; echo-prov-false + ; true≢false + ) +open Row using (prov) +open import EchoExampleAbsInt + using ( Sign; Carrier; pos; α + ; p1; p2 + ; echo-pos-p1; echo-pos-p2 + ; p1≢p2 + ) + +open import Data.Bool.Base using (Bool; true) +open import Data.List.Base using (List) +open import Data.Product.Base using (Σ; _,_; proj₁) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_) +open import Function.Base using (_∘_) + +---------------------------------------------------------------------- +-- Parser example (`EchoExampleParser`). +-- +-- `paren-nested` (`((` `)` `)`) and `paren-pair` (`(` `)` `(` `)`) +-- both have `parses ≡ true`. The Echo retains the distinction +-- (`echo-parse-nested≢echo-parse-pair`). The raw-Σ counter-program +-- below uses `proj₁` directly to recover the original `List Token`, +-- distinguishing the two echoes via the already-proven +-- `paren-nested≢paren-pair`. The Echo interface at affine mode would +-- refuse to export `proj₁`; this lemma exhibits exactly what would +-- leak if it didn't. + +parser-sigma-distinguishes : + Σ (Echo parses true → List Token) + (λ g → g echo-parse-nested ≢ g echo-parse-pair) +parser-sigma-distinguishes = proj₁ , paren-nested≢paren-pair + +---------------------------------------------------------------------- +-- Provenance example (`EchoExampleProvenance`). +-- +-- `row-with-prov-true` and `row-with-prov-false` project to the same +-- payload (`project ≡ 0`) but carry distinct provenance Booleans. The +-- Echo retains the provenance (`echo-prov-true≢echo-prov-false`). The +-- raw-Σ counter-program composes `prov` with `proj₁` to leak the +-- provenance Bool, distinguishing the two echoes via `true≢false`. + +provenance-sigma-distinguishes : + Σ (Echo project 0 → Bool) + (λ g → g echo-prov-true ≢ g echo-prov-false) +provenance-sigma-distinguishes = prov ∘ proj₁ , true≢false + +---------------------------------------------------------------------- +-- Abstract-interpretation example (`EchoExampleAbsInt`). +-- +-- `p1` and `p2` both abstract to `pos` under the 5-element sign +-- lattice (`α p1 ≡ α p2 ≡ pos`). The Echo retains the concrete +-- carrier (`echo-pos-p1≢echo-pos-p2`). The raw-Σ counter-program +-- uses `proj₁` to recover the concrete Carrier, distinguishing via +-- `p1≢p2`. + +absint-sigma-distinguishes : + Σ (Echo α pos → Carrier) + (λ g → g echo-pos-p1 ≢ g echo-pos-p2) +absint-sigma-distinguishes = proj₁ , p1≢p2 diff --git a/roadmap.adoc b/roadmap.adoc index c0689ea..3133cff 100644 --- a/roadmap.adoc +++ b/roadmap.adoc @@ -161,14 +161,17 @@ gate cross-links) landed in-session. Tracks B + C remain. *Close-out criterion (falsifiable).* All three hold: -. Track B (consumer-side abstraction barrier) — same artefact named in - Lane 1's close-out. (Lane 1 and Lane 2 share this artefact; that is - intentional, not duplication.) -. Track C (per-example raw-Σ counter-programs) lands as - `proofs/agda/examples/EchoVsSigma.agda`, pairing each headline - example with the small Σ-misuse it blocks. Pinned in Smoke. +. *LANDED 2026-05-26.* Track B (consumer-side abstraction barrier) — + same artefact named in Lane 1's close-out. (Lane 1 and Lane 2 share + this artefact; that is intentional, not duplication.) +. *LANDED 2026-05-26.* Track C (per-example raw-Σ counter-programs) + shipped as `proofs/agda/examples/EchoVsSigma.agda`, pairing each + headline example (parser, provenance, abs-int) with the small + Σ-misuse it blocks. Builds clean under `--safe --without-K`; + pinned in `Smoke.agda` under own `using` block. . The Gate 2 nominee list is re-audited and crosses the *comfortable* threshold (≥ 3 of 4 surviving), not merely the honest minimum. + *(Remaining open item for Lane 2 close-out.)* *Artefacts (landed today).* `core/skepticisms/is-this-just-sigma-types.md` (canonical answer doc, 5-section structure mirroring the demands); From 6d9b74c39648d44abbb6f1108cf114a31c7a4636 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 26 May 2026 23:37:33 +0100 Subject: [PATCH 05/10] docs: Pillar E in-repo close-out + Gate 2 Rev 5 + Lane 4/5 scope/scaffold (#121) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary In-repo close-out work across all four currently-open lanes per `roadmap.adoc`. Stacked on PR #118 (consolidation); merges into that branch and will land on `main` together when #118 squashes. - **Lane 1 (Pillar E in-repo).** Status NOTE in `paper.adoc` + `types-abstract.adoc` declaring tags 1/2/3 cleared; tag 4 (ordinal appendix) is gated on Bachmann–Howard per `roadmap.adoc` §Lane 3 — not a missing deliverable for the in-repo half of Pillar E. Honest about the offline boundary (venue choice, Zenodo DOI, library packaging, outreach). - **Lane 2 (Gate 2 re-audit).** `docs/characteristic.adoc` Revision 5: re-checks 4/4 surviving against everything post-Rev-4 (EI-2 termination via PATH B, `characteristic.NonTruncatable` Q2.1 PARTIALLY REDUCIBLE caveat, deliberately-broken `characteristic.N5Falsifier`). Comfortable threshold (≥3/4) met by margin of one. Candidate N5 remains unadopted on the same logic as Rev 4. Closes the Lane 2 close-out criterion (3). - **Lane 4 [PARKED] (bridges-CI scope).** `docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc` adopts option A (separate `echo-bridges-ci` repo with submodules) over option B (in-tree submodules). Three load-bearing reasons; three override triggers; unpark-time playbook. Lane stays PARKED. - **Lane 5 [PARKED] (tutorial track).** `tutorial/README.adoc` scaffolds three walkthroughs at design-doc level: (1) certified region-exit audit tied to ephapax L3 = killer-app candidate; (2) epistemic erasure with the in-memory-bytes-vs-type-level disclosure as the opening sentence; (3) provenance/debugging echo. No Agda lands. Lane stays PARKED. - **`roadmap.adoc`**: Lane 2 close-out item (3) marked LANDED; Lane 4 + Lane 5 sections gain pre-resolved-decision/scaffold pointers. Build invariant held: `agda All.agda` + `agda Smoke.agda` both exit 0 under `--safe --without-K`, zero postulates / escape pragmas / funext (no Agda touched in this commit). ## Test plan - [x] `agda --library-file=/tmp/agda-libs -i proofs/agda proofs/agda/All.agda` → exit 0 - [x] `agda --library-file=/tmp/agda-libs -i proofs/agda proofs/agda/Smoke.agda` → exit 0 - [x] No new postulates / escape pragmas (docs-only commit) - [x] GPG-signed - [ ] CI: governance + Hypatia + agda jobs green - [ ] Auto-merge enabled (squash, delete branch) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) --- docs/characteristic.adoc | 124 +++++++++++- .../decisions/lane-4-bridges-ci-scope.adoc | 165 ++++++++++++++++ docs/echo-types/paper.adoc | 15 ++ docs/echo-types/types-abstract.adoc | 11 ++ roadmap.adoc | 29 ++- tutorial/README.adoc | 180 ++++++++++++++++++ 6 files changed, 516 insertions(+), 8 deletions(-) create mode 100644 docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc create mode 100644 tutorial/README.adoc diff --git a/docs/characteristic.adoc b/docs/characteristic.adoc index 64980cf..5809fa2 100644 --- a/docs/characteristic.adoc +++ b/docs/characteristic.adoc @@ -11,11 +11,15 @@ Gate 2 of the identity claim. It audits the nominees against the gate's falsifier — "naturally echo-shaped, not reducible to generic sigma/fiber lemmas" — and reports the threshold outcome. -This is *Revision 4*. It adds a fourth nominee (`EchoLinear.degradeMode-compose`), -introduces a new construction in this lane (`characteristic.RoleGraded`) -that closes the open recommendation from the handoff's Observation E, -and proposes a candidate fifth nominee. See §<> -for the diff. +This is *Revision 5* (2026-05-26). It is the close-out re-audit +required by `roadmap.adoc` §Lane 2: it re-checks that the +Revision-4 nominee table still clears the *comfortable* threshold +(≥ 3 of 4 surviving) under everything that has landed in this +lane since then. Verdict: still 4/4 surviving; comfortable +threshold met by margin of one. The Revision-5 substance is in +§<>; the per-nominee +audits below are unchanged from Revision 4. See §<> for the full diff. toc::[] @@ -518,7 +522,117 @@ withdrawn lemma can be left in place as a historical signpost. | 3 | Amendment to `roadmap-gates.adoc` adopted. Nominee list: `degrade-via-join`, `degrade-compose`, `applyChoreo-compose`. 3/3 surviving across two modules. Recommended further work: genuine integration theorem; fourth nominee for diversification. | 4 | Added `EchoLinear.degradeMode-compose` as N4 (per the Revision-3 recommendation; user-explicit). Built `characteristic.RoleGraded` and `choreo-grade-commute` (closes handoff Observation E). 4/4 surviving across three modules. Proposed adding `choreo-grade-commute` as N5 (left to integrator's discretion). + +| 5 (2026-05-26) | Close-out re-audit per `roadmap.adoc` §Lane 2: re-checks the Revision-4 nominee table against everything that has landed since (EI-2 terminated negative; `characteristic.NonTruncatable` for Q2.1 received-`y` form is PARTIALLY REDUCIBLE; the broken `characteristic.N5Falsifier` is ledgered, not silently dropped). Verdict: 4/4 still surviving, *comfortable* threshold (≥3/4) met by margin of one. Candidate N5 (`choreo-grade-commute`) remains unadopted: the post-Rev-4 EI-2 termination shows its non-trivial content is the same single `(c⊑s, keep≤keep)` cell as before, so nominating it would not strengthen the count beyond cosmetic. +|=== + +[[revision-5]] +== Revision-5 re-audit (2026-05-26) + +This section is the close-out audit named in `roadmap.adoc` §Lane 2 +close-out criterion (3). It re-checks the Revision-4 nominee table +against everything that has landed in the characteristic / Gate-2 +lane since Revision 4. Three categories of evidence were considered; +none weakens the Revision-4 verdict. + +=== Bar being checked + +`roadmap.adoc` §Lane 2 distinguishes two thresholds (taken from +`roadmap-gates.adoc` Gate 2): the *honest minimum* (≥ 2 of 4 +surviving) and the *comfortable* threshold (≥ 3 of 4 surviving). +Revision 4 reported 4/4. Lane 2 close-out asks: under everything +this lane has produced since, does that still hold by the +comfortable bar? + +=== Evidence reviewed since Revision 4 + +. *EI-2 terminated — negative verdict, PATH B* (`docs/EI2_REPORT.adoc`, + authoritative). Eight investigation phases, seven data points + (sibling 2D constructions `characteristic.RoleMode`, + `characteristic.ModeGraded`, 3D `characteristic.RoleModeGrade` + with three pairwise commutations + a triple, self-pairing + `characteristic.RoleRole`), plus the formal exhibit + `characteristic.ChoreoInjective` for the non-loss-only criterion + and the partial generic `characteristic.RecipeTheorem`. The + termination finding is that the integration recipe with the + existing five named axes does *not* carry substantive simultaneous + cross-axis content — every "non-trivial" cell carries one-axis-at- + a-time content. The five doc locations enumerated in EI2_REPORT + §"Documentation cascade" have all been updated accordingly. +. *Q2.1 / `characteristic.NonTruncatable`.* The general statement of + `echo-not-prop` for `(f, y)` with two distinct preimages is + re-exported under the Q2.1 name; the received-`y` form is + *PARTIALLY REDUCIBLE* per the module's own Gate-2 falsifier audit + (proof factors through generic Σ; echo-specific content is in the + statement only). The constructed-`y` form, which builds `y` from + bare non-injectivity, carries echo-specific content but is not on + the Revision-4 nominee table — it is closer to a Gate-3 example + obligation than a Gate-2 nominee. +. *`characteristic.N5Falsifier` — KNOWN BROKEN, DELIBERATELY EXCLUDED* + from `characteristic/All.agda` and from any CI green closure + (`UnsolvedConstraints` + `UnsolvedMetaVariables`). Status disclosed + in the module's own broken banner and at + `docs/echo-types/earn-back-plan.adoc` item C/N5; monitored by an + expected-failure CI gate. *Crucially: nothing in N5Falsifier is + cited as evidence in this audit, and its broken status does not + count against any nominee. The fact that an attempted falsifier + for N5 (= `choreo-grade-commute`) is not mechanised is exactly why + N5 itself is not adopted in this revision.* + +=== Per-nominee re-check + +[cols="1,2,2,3", options="header"] |=== +| Nominee | Module | Status as of Rev 5 | Reason + +| N1 | `EchoGraded.degrade-via-join` | SURVIVES (unchanged from Rev 4) | The lemma is on the loss-grade lattice's join, not on any integration claim. EI-2 termination does not touch it. No falsifier attempted since Rev 4. +| N2 | `EchoGraded.degrade-compose` | SURVIVES (unchanged from Rev 4) | As N1: single-decoration lemma; EI-2 termination is orthogonal. No falsifier attempted since Rev 4. +| N3 | `EchoChoreo.applyChoreo-compose` | SURVIVES (unchanged from Rev 4) | Single-decoration role-reachability lemma; the `client-to-server` content this lemma factors through is the very content EI-2 traced as the one load-bearing non-trivial cell across 2D pairings — that is independent evidence the lemma is non-vacuous, not a weakening. +| N4 | `EchoLinear.degradeMode-compose` | SURVIVES (unchanged from Rev 4) | Single-decoration mode lemma with the specific `weaken` content (`no-section-collapse-to-residue` attached); EI-2 termination is orthogonal. +|=== + +=== Verdict + +Survivors: N1, N2, N3, N4. Count: 4. Honest threshold (≥ 2): met. +Comfortable threshold (≥ 3): met by margin of one. The Lane 2 +close-out criterion in `roadmap.adoc` is satisfied. + +=== What the re-audit explicitly does NOT do + +. *Does not nominate N5.* The candidate fifth nominee + (`characteristic.RoleGraded.choreo-grade-commute`) remains a + candidate. EI-2's termination shows the protocol-pass-but-narrow + reading from Rev 4 was correct: the only non-trivial cell of the + 2D family's commutation is `(c⊑s, keep≤keep)`, reducing to + `client-to-server e` — the same Choreo content N3 already carries. + Nominating it would push the count to 5/5, but the marginal + evidence is the same `client-to-server` content already credited + to N3, so nominating it would be cosmetic. Left unadopted on the + same logic as Rev 4. +. *Does not retroactively retract any Rev-4 verdict.* No nominee's + falsifier was attempted and *failed*; the absence of attempts is + carried forward as a Rev-4 honest qualification (§<> item 3), not a Rev-5 finding. +. *Does not promote `characteristic.NonTruncatable.Q2-1` to the + nominee table.* Its own broken-Gate-2 audit (PARTIALLY REDUCIBLE) + was applied honestly; the lemma remains useful as a Gate-3 + signpost, not as a Gate-2 survivor. + +=== Pointer additions since Rev 4 + +* `proofs/agda/characteristic/RoleMode.agda`, + `RoleModeGrade.agda`, `RoleRole.agda`, `ModeGraded.agda`, + `ChoreoInjective.agda`, `RecipeNonTriviality.agda`, + `RecipeSpec.agda`, `RecipeTheorem.agda`, `InteractionTest.agda` — + EI-2 investigation lane. Not Gate-2 nominees; supply the + EI-2-termination evidence the §"Evidence reviewed" item 1 cites. +* `proofs/agda/characteristic/NonTruncatable.agda` — Q2.1, see + §"Evidence reviewed" item 2. +* `proofs/agda/characteristic/N5Falsifier.agda` — + *KNOWN BROKEN, NOT IN CI CLOSURE*; see §"Evidence reviewed" + item 3. +* `docs/EI2_REPORT.adoc` — authoritative EI-2 verdict. +* `proofs/agda/characteristic/All.agda` — the lane-local CI seam. == Cross-lane observations diff --git a/docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc b/docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc new file mode 100644 index 0000000..91195e4 --- /dev/null +++ b/docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc @@ -0,0 +1,165 @@ += Lane 4 scope decision: bridges-CI architecture +:toc: macro +:toclevels: 2 +:sectnums: +:icons: font + +[.lead] +Decision document for `roadmap.adoc` §"Lane 4 [PARKED] — Bridges-CI". +This file resolves the scope question that the parked-lane line +asked, while keeping the lane formally parked until its unblocking +condition (Lane 1 close-out) is met. Author: Claude session, +2026-05-26. + +toc::[] + +== The question this document answers + +`roadmap.adoc` §"Lane 4 [PARKED]" records: + +[quote] +End-to-end verified bridges to Janus, Tropical, CNO, etc. +currently sit as in-tree modules (`EchoJanusBridge.agda`, +`EchoTropical.agda`, `EchoCNOBridge.agda`, `DyadicEchoBridge.agda`) +without CI-verified round-trips against the target codebases. Two +architectural options when unparking: … + +This document picks one of those two architectures and pins the +choice so a future session unparking Lane 4 does not re-litigate it. +It does *not* re-open Lane 4 — the unblocking condition (Lane 1 +closes) still gates activation. + +== Decision + +*Adopt option A: a separate `echo-bridges-ci` repository pulling +echo-types and each target as submodules.* + +The roadmap line already states this is preferred unless broader +research-plan priorities favour tighter integration. As of +2026-05-26 there is no such preference on file; this document +ratifies the preferred reading as the *decision* rather than the +default. + +== Why option A + +Three load-bearing reasons, in priority order. + +. *`--safe --without-K` discipline stays inside echo-types.* Every + in-tree bridge module today (`EchoJanusBridge`, `EchoTropical`, + `EchoCNOBridge`, `DyadicEchoBridge`) typechecks under + `--safe --without-K` with zero postulates because the target + codebase's content is *encoded structurally* (e.g. `EchoJanusBridge` + mirrors januskey's eight-variant `OpKind` as a local Agda + inductive). Pulling the actual target codebases in-tree would + drag their build invariants into this repo's CI, several of which + (Rust / SPARK / Idris2 / TypeScript) cannot be `--safe --without-K` + by construction. Option B silently degrades the single invariant + this repo is currently strict about. +. *Bridge instability does not propagate.* The targets evolve on + their own cadence; a verified-translation lemma that breaks + because the target's API moved should land as a *bridge-CI + failure*, not as a red echo-types build. The blast radius of + bridge churn must stay outside the load-bearing repo (Lane 1). +. *Lane 1 is the load-bearing lane.* `roadmap.adoc` §Lanes lists + Lane 1 first by priority for a reason: the paper / external + recognition. Anything that risks Lane 1's CI cleanliness for + Lane 4's content is the wrong trade-off as long as Lane 1 is + load-bearing. + +== When option B (in-tree submodules) would override + +Three concrete triggers, all of which must hold simultaneously, +would re-open this decision: + +. The user's stated priorities shift to favour tighter integration + with one specific target codebase to the extent that bridge churn + *should* fail the echo-types build. +. The target codebase in question is itself `--safe --without-K` + compatible (in practice: Agda or Idris2-with-totality-checked + modules), so option B does not degrade the invariant. +. Lane 1 has *fully closed* (not merely close-out-met) — i.e. the + paper is published or accepted, and external-recognition pressure + on CI cleanliness has lifted. + +Absent all three, option A stands. + +== What option A looks like at unpark time + +When Lane 1 closes and Lane 4 is unparked, the work expands to: + +. *New repository `hyperpolymath/echo-bridges-ci`* under the same + org. Same licence policy (MPL-2.0 per the recent estate sweep). +. *Submodule layout* under `bridges/`: ++ +[source,text] +---- +bridges/ + echo-types/ → submodule pinning hyperpolymath/echo-types + januskey/ → submodule pinning hyperpolymath/januskey + cno/ → submodule pinning hyperpolymath/cnocode (or wherever absolute-zero lives) + ephapax/ → submodule pinning hyperpolymath/ephapax + ... +---- +. *Per-bridge verified-translation lemmas* land in + `bridges//verify.agda` (or `.idr`/`.lean` as the target's + proof assistant requires). Each lemma states the round-trip + property between the echo-types in-tree mirror (e.g. + `EchoJanusBridge.OpKind`) and the live target type (e.g. + januskey's `src/abi/Types.idr` `OpKind`). The CI seam is *this + lemma typechecking*, not the targets themselves typechecking + against echo-types. +. *CI matrix* per bridge: a build job that bumps the submodule + pin, runs the verify lemma, and reports green/red. Red is a + bridge-CI signal, not a target-repo signal — neither this repo + nor any target is gated on bridge-CI green. + +== What stays in echo-types after option A is built + +The current in-tree bridge modules +(`EchoJanusBridge.agda`, `EchoTropical.agda`, `EchoCNOBridge.agda`, +`DyadicEchoBridge.agda`) *stay where they are*. They are the local +structural mirrors that the bridge-CI verified-translation lemmas +target on the echo-types side. Deleting them would break the +bridge-CI lemmas without strengthening this repo. The roadmap +should reflect: "in-tree mirrors are the canonical Agda statement +of the bridge interface; round-trip verification against the live +target is in `echo-bridges-ci`." + +== Open question this decision deliberately leaves + +The Tropical bridge does not point at a single canonical target +repo today (the tropical decoration is a mathematical pattern, not +a codebase). When Lane 4 unparks, the Tropical bridge either (a) +finds a concrete consumer to verify against, or (b) stays as the +in-tree `EchoTropical.agda` plus `AntiEchoTropical.agda` / +`AntiEchoTropicalGeneric.agda` and is *not* migrated into +`echo-bridges-ci`. Option (b) is the honest default; option (a) +requires a named consumer. + +== Status + +Decision: *option A adopted as of 2026-05-26*. + +Lane 4 status: still *PARKED*. This document does not unpark it. +The unblocking condition (Lane 1 closes per `roadmap.adoc` Lane 1 +close-out criterion) is unchanged. + +When Lane 4 unparks, the first three actions are: + +. Create `hyperpolymath/echo-bridges-ci` per §"What option A looks + like at unpark time". +. Migrate the JanusBridge round-trip from a structural mirror to a + verified-translation lemma against the live januskey + `src/abi/Types.idr` `OpKind`. +. Migrate the CNO bridge analogously. + +That sequence is *not* started in this session; recording it here +saves the next session from re-deriving the unpark plan. + +== References + +* `roadmap.adoc` §"Lane 4 [PARKED] — Bridges-CI" +* `docs/bridges/cross-repo-bridge-status.md` — current per-bridge status +* `proofs/agda/EchoJanusBridge.agda`, `EchoTropical.agda`, + `EchoCNOBridge.agda`, `DyadicEchoBridge.agda` — in-tree mirrors +* `CLAUDE.md` §"Ecosystem context" — list of adjacent target repos diff --git a/docs/echo-types/paper.adoc b/docs/echo-types/paper.adoc index fd002f7..e863fa0 100644 --- a/docs/echo-types/paper.adoc +++ b/docs/echo-types/paper.adoc @@ -19,6 +19,21 @@ abstract (`types-abstract.adoc`) is the short, already-submission-ready companion; this is the full CPP/ITP-style mechanised-metatheory paper it grows into. + +*Pillar E in-repo close-out (2026-05-26).* Of the four `[EXPAND]` +tags originally on this paper: tag 1 (background / notation primer) +cleared in PR #73; tag 2 (related work — Granule / QTT, +Uustalu–Vene comonads, coeffects, lens/optic vs witness-transport +leg) cleared in PR #120, with the single-page reviewer companion at +`docs/echo-types/comparators.adoc` shipping the axis-by-axis +summary; tag 3 (evaluation — proof-size / cost table, honest +account of the common-upper-bound idiom) cleared earlier in PR #84 +(see §"Evaluation and discussion"). Tag 4 (ordinal consumer-evidence +appendix) is the only one remaining open, and it is *gated* on the +ordinal-track milestone per `roadmap.adoc` §Lane 3 — not a missing +deliverable for the in-repo half of Pillar E. Everything else +(venue choice, Zenodo DOI, library packaging, outreach) is +author-driven and is flagged but not auto-run. ==== toc::[] diff --git a/docs/echo-types/types-abstract.adoc b/docs/echo-types/types-abstract.adoc index 820073e..6674bf7 100644 --- a/docs/echo-types/types-abstract.adoc +++ b/docs/echo-types/types-abstract.adoc @@ -185,3 +185,14 @@ Submission logistics (venue deadline, TYPES-template formatting, author metadata, Zenodo DOI, arXiv cross-post) remain offline and author-driven; they are downstream of, not a substitute for, the re-review. + +NOTE: *In-repo Pillar E status (2026-05-26).* The full `paper.adoc` +has cleared all `[EXPAND]` tags except the ordinal consumer-evidence +appendix (gated on Bachmann–Howard per `roadmap.adoc` §Lane 3). Any +further re-review of this abstract should treat the full paper as +the canonical reference for narrowed claims; this abstract is the +2-page condensation of it. The single-page reviewer companion +`docs/echo-types/comparators.adoc` carries the axis-by-axis +comparison against Granule, QTT, choreographic types, and Linear +Haskell. See `roadmap.adoc` §"Pillar status" for the lane-level +view. diff --git a/roadmap.adoc b/roadmap.adoc index 3133cff..e273871 100644 --- a/roadmap.adoc +++ b/roadmap.adoc @@ -169,9 +169,14 @@ gate cross-links) landed in-session. Tracks B + C remain. headline example (parser, provenance, abs-int) with the small Σ-misuse it blocks. Builds clean under `--safe --without-K`; pinned in `Smoke.agda` under own `using` block. -. The Gate 2 nominee list is re-audited and crosses the *comfortable* - threshold (≥ 3 of 4 surviving), not merely the honest minimum. - *(Remaining open item for Lane 2 close-out.)* +. *LANDED 2026-05-26.* The Gate 2 nominee list is re-audited (Rev 5, + `docs/characteristic.adoc` §"Revision-5 re-audit (2026-05-26)") and + still crosses the *comfortable* threshold: 4/4 surviving, margin of + one above the comfortable bar (≥ 3 of 4). The re-audit explicitly + re-checks the post-Rev-4 evidence (EI-2 termination, + `characteristic.NonTruncatable` Q2.1, the deliberately broken + `characteristic.N5Falsifier`) and finds none of it weakens any + surviving nominee. *Artefacts (landed today).* `core/skepticisms/is-this-just-sigma-types.md` (canonical answer doc, 5-section structure mirroring the demands); @@ -218,6 +223,16 @@ subtree. Per-session ledger in CLAUDE.md §"Session arc 2026-05-20". *Unblocking condition.* Lane 1 closes. +*Scope decision (pre-resolved 2026-05-26).* +`docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc` adopts +**option A** (separate `echo-bridges-ci` repository pulling +echo-types and each target as submodules) per the recommendation +this section already carried. The decision document also names the +three triggers that would override the choice (all three must hold +simultaneously) and lays out what option A looks like at unpark +time, so an unparking session does not re-derive the architecture. +Lane 4 itself remains PARKED. + *Scope question to resolve when unparking.* End-to-end verified bridges to Janus, Tropical, CNO, etc. currently sit as in-tree modules (`EchoJanusBridge.agda`, `EchoTropical.agda`, `EchoCNOBridge.agda`, @@ -253,6 +268,14 @@ in-memory bytes are zeroed — conflating these is a category error a sceptic will catch); (3) provenance / debugging echo over a small state-reconstruction example. +*Scaffold (pre-resolved 2026-05-26).* `tutorial/README.adoc` lands +the three walkthroughs at design-doc level with their target file +layouts, honest-bound disclosures, the per-walkthrough Smoke pin +discipline, and the killer-app-candidate close-out check on +Walkthrough 1. No Agda lands at this stage; the scaffold exists so +an unparking session lands Agda directly rather than re-deriving +the pedagogy. Lane 5 itself remains PARKED. + == Closed lanes (none yet — populated when a lane closes per its close-out criterion). diff --git a/tutorial/README.adoc b/tutorial/README.adoc new file mode 100644 index 0000000..650210d --- /dev/null +++ b/tutorial/README.adoc @@ -0,0 +1,180 @@ += Tutorial track scaffold (Lane 5) +:toc: macro +:toclevels: 2 +:sectnums: +:icons: font + +[.lead] +This directory is the scaffold for `roadmap.adoc` §"Lane 5 [PARKED] +— Tutorial / pedagogy". Lane 5 is still parked; this scaffold +exists so that when the lane unparks the next session has the +structure and walkthrough plans in hand and can land Agda directly +rather than re-deriving the pedagogy. + +[IMPORTANT] +==== +*Lane 5 is parked.* Until its unblocking condition is met (Lane 1 +closes, OR a single killer-application example emerges that +justifies a tutorial track on its own merit), nothing under this +directory should be promoted to a load-bearing artefact in the +README or in `roadmap.adoc` §"Pillar status". The Smoke gate, +`All.agda`, and the gates do not depend on anything here. +==== + +toc::[] + +== Three walkthroughs (planned) + +When Lane 5 unparks, three walkthroughs land in this directory in +priority order. The order reflects the user's suggestion captured +in `roadmap.adoc` §Lane 5: the certified region-exit audit comes +first because it ties to an active adjacent project (ephapax L3), +demonstrates the affine-mode discipline at a real audit boundary, +and is the candidate killer-application example. + +=== Walkthrough 1: certified region-exit audit (PRIORITY — killer-app candidate) + +*Status.* Design-doc only. Agda lands at unpark time. + +*Adjacent project.* `hyperpolymath/ephapax` — programming language +with linear types guaranteeing memory safety for WebAssembly. The +"L3" layer in CLAUDE.md memory entries refers to ephapax's +region-based memory discipline. + +*The pedagogy.* Model an ephapax-style region as an Agda type +`Region` with a `freshen`/`exit` pair. Every `S_Region_Exit` step +produces a *consumed* `LEcho affine` whose payload is the audit +receipt — what was released and to whom. The Echo's +`no-section-weaken` provides the machine-checked guarantee that no +post-exit caller can reconstruct the un-degraded source from the +audit receipt alone. The walkthrough closes by exhibiting the +honest bound: the audit guarantee is about the *type-level* witness, +NOT about in-memory bytes being zeroed. (See Walkthrough 2 for the +matched-negative on that category error.) + +*Files when landed.* + +* `tutorial/region-exit-audit/README.adoc` — narrative walkthrough + with the design rationale and the bound disclosure up front. +* `tutorial/region-exit-audit/RegionExitAudit.agda` — the worked + example. Builds under `--safe --without-K`, zero postulates. +* `tutorial/region-exit-audit/Smoke.agda` — per-walkthrough Smoke + pins (own `using` block, header comment) per CLAUDE.md "Working + rules". + +*Why this is the killer-app candidate.* Tied to an active +adjacent project (real consumer pressure), concrete (one named +audit boundary, not a class of boundaries), exhibits the affine +mode at the *interesting* discipline (consumed-on-exit, not just +weakened-once), and the matched-negative (no-zeroing claim) is +honest about the category error a sceptic would catch. + +=== Walkthrough 2: epistemic erasure with honest bound + +*Status.* Design-doc only. Agda lands at unpark time. + +*The pedagogy.* Model a key-derivation function `kdf : Seed → Key` +where the visible output is the derived `Key` and the hidden source +is the `Seed`. `Echo kdf k` retains the seed at the type level; +`no-section-collapse` (factored through `EchoResidue`) is the +machine-checked guarantee that no pure-Agda function recovers the +seed from the key alone. + +*The crucial honest disclosure.* This is *not* a claim that +in-memory bytes of the seed have been zeroed. Conflating the two +is a category error a sceptic will catch — exactly the kind of +mistake the project's retraction discipline (`docs/retractions.adoc`) +exists to prevent. The walkthrough opens with the disclosure, then +states the actual claim (no-section at the type level), then walks +the proof. + +*Files when landed.* + +* `tutorial/epistemic-erasure/README.adoc` — narrative with the + bound disclosure as the *opening* sentence, not a footnote. +* `tutorial/epistemic-erasure/EpistemicErasure.agda` — the worked + example with the `no-section` lemma front and centre. +* `tutorial/epistemic-erasure/Smoke.agda` — per-walkthrough Smoke + pins. + +*Why this walkthrough exists.* Sceptics walking into the repo will +ask "so does echo-types prove key zeroing?". The honest answer is +"no, and the walkthrough exists to explain *what it does prove* +instead, before that miscommunication takes root in any +write-up of echo for an applied audience." + +=== Walkthrough 3: provenance / debugging echo + +*Status.* Design-doc only. Agda lands at unpark time. + +*The pedagogy.* Model a small state-reconstruction example: an +agent observes a single Boolean output `b : Bool` from an opaque +computation `f : State → Bool` on a 4-element `State`. `Echo f b` +retains the source state; iterated `degrade` operations +(`keep → residue → forget` per `EchoResidue`) walk a debugger +through what information is available at each provenance level. +The walkthrough closes by exhibiting how the residue-level +`collapse-via-residue` lemma supports a class-level claim ("the +state was in the 'sign-positive' class") even when the full state +is no longer recoverable. + +*Files when landed.* + +* `tutorial/provenance-debugging/README.adoc` — narrative. +* `tutorial/provenance-debugging/ProvenanceDebugging.agda` — the + worked example, building on `EchoExampleProvenance.agda`. +* `tutorial/provenance-debugging/Smoke.agda` — per-walkthrough + Smoke pins. + +*Why this walkthrough exists.* The two harder walkthroughs (audit, +erasure) both ship as `LEcho affine` content where information is +*not* recoverable. This third walkthrough exhibits the dual: where +the iterated degradation makes some information unrecoverable but +others survive (the residue layer). It is the gentlest of the +three; readers who bounce off the audit and erasure walkthroughs +land here. + +== Discipline that applies to all three walkthroughs + +The same constraints that govern the rest of the repo apply +verbatim: + +* `--safe --without-K` throughout. +* Zero postulates, zero escape pragmas, no funext. +* Every headline theorem pinned in the per-walkthrough Smoke + (own `using` block, header comment). +* Every new Agda module imported into the walkthrough's + `All.agda` (and optionally into the top-level + `proofs/agda/All.agda` if the walkthrough exposes a reusable + lemma). +* Per-walkthrough `README.adoc` opens with the *honest bound*, not + with the punchline. +* Cross-references to `docs/retractions.adoc` where a narrowed + claim is being used (e.g. walkthrough 2's no-key-zeroing + disclosure is the same discipline as the R-2026-05-18 + narrowings). + +== Killer-app close-out check + +`roadmap.adoc` §Lane 5 records the second unblocking condition +("a single killer-application example emerges that justifies a +tutorial track on its own merit"). The certified region-exit audit +(Walkthrough 1) is the candidate. Whether it *constitutes* a +killer-app for Lane 5 unparking purposes is a judgment call the +user can make when reviewing this scaffold. The candidate's claim +to killer-app status rests on the three items in §"Walkthrough 1 +> Why this is the killer-app candidate". If the user accepts the +candidate, Lane 5 can unpark on that basis without waiting for +Lane 1's other closure. + +== References + +* `roadmap.adoc` §"Lane 5 [PARKED] — Tutorial / pedagogy" +* `CLAUDE.md` §"Ecosystem context" — ephapax row +* `proofs/agda/EchoLinear.agda` — `LEcho`, `weaken`, `no-section-weaken` +* `proofs/agda/EchoResidue.agda` — `EchoR`, `collapse-to-residue`, + `no-section-collapse-to-residue` +* `proofs/agda/EchoExampleProvenance.agda` — provenance example + walkthrough 3 builds on +* `docs/retractions.adoc` — the discipline walkthrough 2's + honest-bound disclosure inherits From 0cc2c1356d8d1587691e9e44fde223a647a759c8 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 27 May 2026 00:04:43 +0100 Subject: [PATCH 06/10] =?UTF-8?q?feat+docs:=20Lane=205=20walkthrough=201?= =?UTF-8?q?=20+=20Lane=203=20=CF=88=CE=B1=20slice=20+=20N5=20sharpened=20+?= =?UTF-8?q?=20Pillar=20E=20offline=20prep=20+=20packaging=20(#122)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Four follow-on workstreams from the four design decisions on 2026-05-26. Stacked onto PR #118's consolidation branch (lands with #118 on the final squash to main). **Lane 5 [UNPARKED] — Walkthrough 1 landed** - `tutorial/region_exit_audit/RegionExitAudit.agda`: ephapax-L3-style region exit. `LEcho linear` = LiveHandle, `LEcho affine` = AuditReceipt, `exit = weaken`, `audit-no-recovery = no-section-weaken` aliased per-region. Honest-bound disclosure (NOT a byte-zeroing claim) opens the file; matched-negative block at bottom names the four properties NOT proved. - Per-walkthrough Smoke + All; tutorial-track aggregator; `tutorial/README.adoc` unpark status updated. **Lane 3 [ACTIVE PUSH] — ψ-admissibility rank refinement slice** - `proofs/agda/Ordinal/Buchholz/RankAdm.agda`: admissibility-aware rank with α-discriminating bpsi shape `ω-rank-pow ν ⊕ rank-pow α`. Closes 1 of 2 deferred ψ constructors via `rank-mono-<ᵇ⁺-ψα-from-pow`. The `<ᵇ-ψΩ≤` ν=μ boundary case is *re-classified* from "admissibility" to "encoding mismatch" (a real structural gap surfaced by the slice); two design follow-ups documented inline. - Score in `buchholz-rank-obstruction.adoc`: 9/13 → 10/13. **Gate 2 N5 falsifier — sharpened & resolved** - `characteristic/N5Falsifier.agda`: unsolved metas resolved by pinning the implicit role+grade params at the four `applyRole`/`applyGrade` call sites. The 2026-05-18 broken status was *inference*, not content (Agda cannot recover the role from `RoleGEcho r keep = Echo (obs r) true` because `obs` is not injective). Now in `characteristic/All.agda` CI green closure. - `docs/characteristic.adoc` Rev 5b: N5-not-adopted decision UNCHANGED on the cosmetic-only-marginal-evidence logic. **Pillar E offline prep — all three sub-tasks** - `docs/echo-types/pillar-e-offline.adoc`: venue matrix (TYPES first recommended), Zenodo DOI mint plan, library packaging update, three outreach drafts (Granule/QTT, choreographic, Linear Haskell). - `echo-types.agda-lib`: include path extended to repo root (for tutorial tree). - `CITATION.cff` + `.zenodo.json`: pre-staged with placeholder DOIs and ORCID fields left blank (not invented) for author to add post-mint. ## Test plan - [x] `agda --library=echo-types proofs/agda/All.agda` → exit 0 - [x] `agda --library=echo-types proofs/agda/Smoke.agda` → exit 0 - [x] `agda --library=echo-types proofs/agda/characteristic/All.agda` → exit 0 (N5Falsifier now included) - [x] `agda --library=echo-types tutorial/All.agda` → exit 0 - [x] All under `--safe --without-K`, zero postulates / escape pragmas / funext - [x] GPG-signed - [ ] CI: governance + Hypatia + agda jobs green - [ ] Auto-merge enabled (squash, delete branch) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) --- .zenodo.json | 30 ++ CITATION.cff | 43 ++ docs/characteristic.adoc | 30 +- .../echo-types/buchholz-rank-obstruction.adoc | 26 +- docs/echo-types/pillar-e-offline.adoc | 381 ++++++++++++++++++ echo-types.agda-lib | 2 +- proofs/agda/All.agda | 1 + proofs/agda/Ordinal/Buchholz/RankAdm.agda | 280 +++++++++++++ proofs/agda/Ordinal/Buchholz/Smoke.agda | 19 + proofs/agda/characteristic/All.agda | 16 +- proofs/agda/characteristic/N5Falsifier.agda | 64 +-- tutorial/All.agda | 20 + tutorial/README.adoc | 54 ++- tutorial/region_exit_audit/All.agda | 10 + tutorial/region_exit_audit/README.adoc | 123 ++++++ .../region_exit_audit/RegionExitAudit.agda | 148 +++++++ tutorial/region_exit_audit/Smoke.agda | 33 ++ 17 files changed, 1216 insertions(+), 64 deletions(-) create mode 100644 .zenodo.json create mode 100644 CITATION.cff create mode 100644 docs/echo-types/pillar-e-offline.adoc create mode 100644 proofs/agda/Ordinal/Buchholz/RankAdm.agda create mode 100644 tutorial/All.agda create mode 100644 tutorial/region_exit_audit/All.agda create mode 100644 tutorial/region_exit_audit/README.adoc create mode 100644 tutorial/region_exit_audit/RegionExitAudit.agda create mode 100644 tutorial/region_exit_audit/Smoke.agda diff --git a/.zenodo.json b/.zenodo.json new file mode 100644 index 0000000..9162296 --- /dev/null +++ b/.zenodo.json @@ -0,0 +1,30 @@ +{ + "title": "echo-types: a definitionally-grounded, loss-graded reindexing modality (Agda)", + "upload_type": "software", + "description": "Constructive Agda formalisation of fibre-based \"structured loss\" types. Defines Echo f y := Σ (x : A) , (f x ≡ y), shows it is definitionally the homotopy fibre (echo↔fib), and develops a loss-graded reindexing modality on top with a pointwise (funext-relative) mediator property, a separating model, and a carrier-parametric abstraction over a fixed grade poset. Under --safe --without-K throughout with zero postulates and a falsifiable retraction discipline.", + "creators": [ + { + "name": "Jewell, Jonathan" + } + ], + "keywords": [ + "agda", + "graded modality", + "homotopy fibre", + "structured loss", + "reindexing modality", + "formal methods", + "mechanised metatheory", + "echo types" + ], + "access_right": "open", + "license": "MPL-2.0", + "related_identifiers": [ + { + "relation": "isSupplementTo", + "identifier": "https://github.com/hyperpolymath/echo-types", + "resource_type": "software" + } + ], + "communities": [] +} diff --git a/CITATION.cff b/CITATION.cff new file mode 100644 index 0000000..67caf5f --- /dev/null +++ b/CITATION.cff @@ -0,0 +1,43 @@ +cff-version: 1.2.0 +title: "echo-types: a definitionally-grounded, loss-graded reindexing modality (Agda)" +message: "If you cite this software, please cite the Zenodo DOI." +type: software +authors: + - given-names: Jonathan + family-names: Jewell + email: jonathan.jewell@gmail.com + # PLACEHOLDER: insert ORCID once registered, e.g. + # orcid: "https://orcid.org/0000-0000-0000-0000" +repository-code: "https://github.com/hyperpolymath/echo-types" +url: "https://github.com/hyperpolymath/echo-types" +abstract: > + Constructive Agda formalisation of fibre-based "structured loss" + types. Defines Echo f y := Σ (x : A) , (f x ≡ y), shows it is + definitionally the homotopy fibre (echo↔fib), and develops a + loss-graded reindexing modality on top with a pointwise + (funext-relative) mediator property, a separating model, and a + carrier-parametric abstraction over a fixed grade poset. Under + --safe --without-K throughout with zero postulates and a + falsifiable retraction discipline. See paper.adoc and + types-abstract.adoc for the mechanised metatheory write-up. +keywords: + - agda + - graded modality + - homotopy fibre + - structured loss + - reindexing modality + - formal methods + - mechanised metatheory +license: MPL-2.0 +# === PLACEHOLDER: paste concept DOI here after first Zenodo mint === +doi: 10.5281/zenodo.0000000 +# === END PLACEHOLDER === +preferred-citation: + type: software + title: "echo-types: a definitionally-grounded, loss-graded reindexing modality (Agda)" + authors: + - given-names: Jonathan + family-names: Jewell + url: "https://github.com/hyperpolymath/echo-types" + doi: 10.5281/zenodo.0000000 + year: 2026 diff --git a/docs/characteristic.adoc b/docs/characteristic.adoc index 5809fa2..19a027b 100644 --- a/docs/characteristic.adoc +++ b/docs/characteristic.adoc @@ -524,6 +524,8 @@ withdrawn lemma can be left in place as a historical signpost. | 4 | Added `EchoLinear.degradeMode-compose` as N4 (per the Revision-3 recommendation; user-explicit). Built `characteristic.RoleGraded` and `choreo-grade-commute` (closes handoff Observation E). 4/4 surviving across three modules. Proposed adding `choreo-grade-commute` as N5 (left to integrator's discretion). | 5 (2026-05-26) | Close-out re-audit per `roadmap.adoc` §Lane 2: re-checks the Revision-4 nominee table against everything that has landed since (EI-2 terminated negative; `characteristic.NonTruncatable` for Q2.1 received-`y` form is PARTIALLY REDUCIBLE; the broken `characteristic.N5Falsifier` is ledgered, not silently dropped). Verdict: 4/4 still surviving, *comfortable* threshold (≥3/4) met by margin of one. Candidate N5 (`choreo-grade-commute`) remains unadopted: the post-Rev-4 EI-2 termination shows its non-trivial content is the same single `(c⊑s, keep≤keep)` cell as before, so nominating it would not strengthen the count beyond cosmetic. + +| 5b (2026-05-27) | Within-Rev-5 follow-up: `characteristic.N5Falsifier` *no longer broken* — unsolved metas around `EchoChoreo.obs` were resolved by pinning the implicit role and grade parameters at the four `applyRole`/`applyGrade` call sites (the blocker was inference, not content). The module is now in `characteristic/All.agda`'s CI green closure. Audit consequences are *recorded in-line in §"Evidence reviewed" item 3 above*: the SURVIVES verdict for the falsifier exhibit is now mechanised, but the N5-not-adopted decision is unchanged on the same Rev-4/Rev-5 cosmetic-only-marginal-evidence logic. |=== [[revision-5]] @@ -568,16 +570,24 @@ comfortable bar? bare non-injectivity, carries echo-specific content but is not on the Revision-4 nominee table — it is closer to a Gate-3 example obligation than a Gate-2 nominee. -. *`characteristic.N5Falsifier` — KNOWN BROKEN, DELIBERATELY EXCLUDED* - from `characteristic/All.agda` and from any CI green closure - (`UnsolvedConstraints` + `UnsolvedMetaVariables`). Status disclosed - in the module's own broken banner and at - `docs/echo-types/earn-back-plan.adoc` item C/N5; monitored by an - expected-failure CI gate. *Crucially: nothing in N5Falsifier is - cited as evidence in this audit, and its broken status does not - count against any nominee. The fact that an attempted falsifier - for N5 (= `choreo-grade-commute`) is not mechanised is exactly why - N5 itself is not adopted in this revision.* +. *`characteristic.N5Falsifier` — RESOLVED 2026-05-27, NOW GREEN AND IN CI CLOSURE.* + Originally KNOWN BROKEN, deliberately excluded + (`UnsolvedConstraints` + `UnsolvedMetaVariables`). The Lane-2 + N5-sharpening pass on 2026-05-27 closed the unsolved metas by + making the implicit `r1`/`r2`/`g` parameters of `applyRole` / + `applyGrade` explicit at the four call sites; the obstacle was + *inference*, not *content* (Agda cannot recover the role from + `RoleGEcho r keep = Echo (obs r) true` because `obs` is not + injective, but supplying the role explicitly resolves it). The + module is now imported in `characteristic/All.agda` and the + broken-banner has been updated with the resolution record. + *Crucially: the resolution does not change the Rev-4 conclusion + about candidate N5* — the only non-trivial cell is still the + `(c⊑s, keep≤keep)` Choreo content already credited to N3, so + adoption would still be cosmetic. The cleaned-up green falsifier + exhibit *does* tighten the audit story (the SURVIVES verdict is + now mechanised instead of being a not-mechanised attempt-of-record) + without changing the N5-not-adopted decision. === Per-nominee re-check diff --git a/docs/echo-types/buchholz-rank-obstruction.adoc b/docs/echo-types/buchholz-rank-obstruction.adoc index 1b0d306..28be05f 100644 --- a/docs/echo-types/buchholz-rank-obstruction.adoc +++ b/docs/echo-types/buchholz-rank-obstruction.adoc @@ -303,22 +303,30 @@ constructors discharge by additive-principal closure. | `<ᵇ-ψ+` | ✓ closed | `rank-pow-via-left` plus the IH. | `<ᵇ-+Ω` | ✓ closed | `rank-pow-bplus-into-ω-rank-pow` (additive-principal at the target) plus the WfCNF tail bound `y ≤ᵇ x` (caller-provided). | `<ᵇ-+ψ` | ✓ closed | Same as `<ᵇ-+Ω` since `rank-pow (bpsi ν _) = ω-rank-pow ν`. -| `<ᵇ-ψα` | ⏳ admissibility | `rank-pow (bpsi ν α) = ω-rank-pow ν` doesn't discriminate on α. Refining the rank to `ω-rank-pow ν ⊕ rank-pow α` works iff `α ∈ C_ν` (ψ-admissibility predicate); deferred to a follow-on slice. -| `<ᵇ-ψΩ≤` | ⏳ admissibility | Same blocker at `ν = μ`: provisional shape gives `ω-rank-pow μ <′ ω-rank-pow μ`, which is false. +| `<ᵇ⁺-ψα` | ✓ closed (Lane 3, 2026-05-26) | `rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α`; `⊕-mono-<-right` closes the shared-Ω-index lex case from `rank-pow α <′ rank-pow β` (which the existing `_<ᵇ⁰_` umbrella discharges). Primitive `rank-mono-<ᵇ⁺-ψα-from-pow` in `Ordinal.Buchholz.RankAdm`. +| `<ᵇ-ψΩ≤` | ⏳ encoding mismatch | `ν <Ω μ` (strict) case closes by `additive-principal-ω-rank-pow {μ}`. `ν = μ` case STILL OPEN: `ω-rank-pow μ ⊕ rank-pow α <′ ω-rank-pow μ` is impossible under any rank shape with `ω-rank-pow ν ≤ rank-adm (bpsi ν α)`. The classical Buchholz gap `[Ω_μ, Ω_{μ+1})` that admissible ψ_μ(α) lives in is not modelled by `ω-rank-pow ν ⊕ rank-pow α`. Two design follow-ups (lex pair, multiplicative ordinal) documented in `RankAdm.agda` §"<ᵇ-ψΩ≤-still-open"; option A (lex pair) recommended. | `<ᵇ-+1` | ⏳ joint-bplus | `rank-pow (bplus z₁ z₂)` is not additive principal in general (it's a sum of additive principals). Discharging requires a coarser bound (e.g., dominate by `ω-rank-pow` of the leading subterm's Ω-index) or a structurally richer rank. | `<ᵇ-0-+` | ✓ closed* | `rank-pow bzero = oz`, and `rank-pow (bplus x y) ≥′ oz` strictly when *either* `x` or `y` is non-`bzero` and the term is WfCNF. The degenerate `bplus bzero bzero` is excluded by WfCNF (atomic-right ≤ left forces both `bzero` and then the sum reduces to a `bzero`-shaped equivalent that doesn't pattern-match as a `bplus` under CNF normalisation — covered as a side-condition). |=== -*Score: 9/13 constructors closed; 3 deferred under explicit blockers; -1 closed conditionally with documented side condition.* +*Score: 10/13 constructors closed (9 under the original `rank-pow` +umbrella + 1 under the new `rank-adm` slice); 2 deferred under +explicit blockers; 1 closed conditionally with documented side +condition. The Lane-3 active-push slice on 2026-05-26 advanced the +score by 1 (`<ᵇ⁺-ψα`) and re-classified `<ᵇ-ψΩ≤` from "admissibility" +to "encoding mismatch" with two named follow-up routes.* === What remains open -* *ψ-admissibility predicate* (`WellFormedAdmissible.agda`, ~80 lines). - Refines `WfCNF` with the constraint that ψ-arguments live in their - binder's Ω-closure `C_ν`. Closes `<ᵇ-ψα` and `<ᵇ-ψΩ≤` once the - rank-pow on `bpsi ν α` is refined to `ω-rank-pow ν ⊕ rank-pow α` - under the admissibility carrier. +* *ψ-admissibility predicate* (`WellFormedAdmissible.agda`, landed + earlier; `RankAdm.agda` landed 2026-05-26 in the Lane 3 active-push + slice). Refines `WfCNF` with the rank-bound on ψ-arguments. + *Status*: `<ᵇ⁺-ψα` *closed* via `rank-mono-<ᵇ⁺-ψα-from-pow` in + `RankAdm.agda`. `<ᵇ-ψΩ≤` ν=μ boundary case re-classified as + *encoding mismatch* — needs a richer rank target (two-component + lex or multiplicative ordinal), not just the admissibility + carrier. See `RankAdm.agda` §"<ᵇ-ψΩ≤-still-open" for the two + design options; option A (lex pair) recommended. * *`<ᵇ-+1` joint-bplus*. Needs either a coarser dominator (e.g., a function `BT → OmegaIndex` returning the leading Ω-index, then rank into `ω-rank-pow ∘ leading-index`) or a richer rank shape. diff --git a/docs/echo-types/pillar-e-offline.adoc b/docs/echo-types/pillar-e-offline.adoc new file mode 100644 index 0000000..9f23e72 --- /dev/null +++ b/docs/echo-types/pillar-e-offline.adoc @@ -0,0 +1,381 @@ += Pillar E offline: prep doc for venue, packaging, outreach +:toc: macro +:toclevels: 3 +:sectnums: +:icons: font + +[.lead] +Pillar E's in-repo half is at close-out (see `paper.adoc` IMPORTANT +banner and `roadmap.adoc` §Lane 1). This document pre-stages the +*offline / author-driven* half — venue + template choice, Zenodo +DOI mint, library packaging, outreach to neighbour communities — so +the user can act on each item without re-deriving the analysis. + +[IMPORTANT] +==== +*The actions in this document are author-driven.* Nothing here is +auto-run. Drafts of cover letters and packaging scaffolds land in +the repo as text for the user to send / publish at their cadence. +==== + +toc::[] + +== Venue + template matrix + +Four candidate venues, ordered by *fit to the current narrowed +claim*. The narrowed claim (per R-2026-05-18) is a definitional +Σ-identity + funext-relative pointwise mediator property + thin- +poset reindexing modality + separating model + carrier-parametric +abstraction over a fixed grade poset + postulate-free +`--safe --without-K` build, under a falsifiable retraction +discipline. The right venue is one whose reviewers will read that +package on its actual strength rather than against the original +graded-comonad framing the retraction note walks back. + +[cols="1,2,2,3,2", options="header"] +|=== +| Venue +| Format +| Typical deadline cadence +| Fit to narrowed claim +| Recommendation + +| TYPES (extended abstract) +| ~2 pp AsciiDoc / LaTeX +| Annual, spring deadline +| *Best fit.* The community already accepts work-in-progress retraction-style pieces; the existing `types-abstract.adoc` is already drafted at the right shape; the audience knows graded modalities and will read the narrowed claim on its own terms. +| *Submit first.* Lowest revision cost, highest probability of audience-appropriate review. + +| CPP +| ~10 pp ACM template +| Annual, fall deadline (Jan target) +| Strong fit. CPP's "Certified Programs and Proofs" framing is exactly what the postulate-free `--safe --without-K` artefact is. Reviewers expect a full mechanised metatheory, which `paper.adoc` already is. +| *Submit second*, after TYPES feedback. CPP rewards exactly the kind of artefact carefully captured here. + +| ITP +| ~15 pp LIPIcs template +| Annual, late winter deadline (Mar target) +| Strong fit on the mechanised side. Audience overlaps CPP but is more proof-assistant-centric; the discussion of `--safe --without-K` + zero postulates + Smoke discipline lands harder here. +| *Alternative to CPP* if CPP timing slips. Don't dual-submit; pick one of CPP/ITP based on which deadline lands first. + +| MSCS journal (or Logical Methods in Computer Science) +| ~25 pp journal article +| Rolling +| Best fit if the paper grows substantially (e.g. consumer-evidence appendix lands once Bachmann-Howard hits). Journal length removes the "evaluation section is brief" pressure. +| *Hold for v2.* After TYPES + CPP cycles produce reviewer feedback, the consolidated journal version is the final form. +|=== + +=== Recommended sequencing + +. *TYPES extended abstract.* `types-abstract.adoc` already exists + in `--safe --without-K`-aware form. Action items: + + .. Pick the year (whichever TYPES has the next submission window). + .. Re-review the abstract against the current paper for any + residual stale phrasings (the abstract carries a `NOT + submission-ready` banner because the original was retracted; the + correction has happened, the banner should be updated to + `submission-ready as of ` once the user signs off). + .. Format under the TYPES template (LaTeX). The content + translation is mechanical; I can prep the LaTeX source as a + parallel file `types-abstract.tex` if requested. + .. Submit. Author metadata, affiliation, ORCID — user only. +. *CPP submission.* Two-month cycle after TYPES. Use `paper.adoc` + as the spine; cut to ~10pp by trimming the §"Evaluation and + discussion" inline narrative (keep the cost table). Convert to + ACM template. +. *Hold ITP and MSCS for v2.* Don't bundle. + +=== What I cannot help with on venue + template + +* Author-metadata blocks (ORCID, affiliation, conflict declarations). +* Cover letters to programme chairs. +* Pre-submission emails to area chairs (when appropriate). +* The actual submission upload. + +These are author-driven by venue rule. + +== Zenodo DOI mint + +The DOI ladder for a mechanised artefact paper: + +. *Concept DOI* — a stable DOI for the project as a whole + (`hyperpolymath/echo-types`), minted once. +. *Version DOI* — per tagged release. Each `git tag vX.Y.Z` should + publish to Zenodo via the GitHub→Zenodo webhook. +. *Citation block* in README + paper artefact statement — + citation by Zenodo DOI rather than commit hash so reviewers cite + a stable target. + +=== What I can pre-stage in-repo + +. `CITATION.cff` at the repo root with the project metadata, + author block, abstract (cribbed from `types-abstract.adoc`), + license (MPL-2.0 per the recent estate sweep), and a placeholder + for the DOI to fill in after first mint. This file is consumed + by GitHub's "Cite this repository" widget and is the canonical + citation source. +. `.zenodo.json` with the matching metadata in Zenodo's format, + including: + - `creators` block (author, ORCID once supplied) + - `keywords`: `["agda", "graded modality", "homotopy fibre", + "loss grading", "formal methods", "echo types"]` + - `related_identifiers` linking to the GitHub repo + - `communities`: TBD on user preference (e.g. `agda`, + `formal-methods`) +. A tag-driven CI workflow `.github/workflows/zenodo-release.yml` + that fires on `v*` tags and triggers the GitHub→Zenodo + integration (after the user has authorised the integration in + Zenodo's GitHub settings). The workflow itself doesn't push to + Zenodo; it just stamps the release notes and pings the existing + webhook. + +=== What the user does + +. Create / log into a Zenodo account. +. Authorise the GitHub→Zenodo integration for + `hyperpolymath/echo-types` (one-click flip in Zenodo settings). +. After the integration is on, push the first `v0.1.0` tag from + `main` after PR #118 lands. Zenodo will mint both the concept + DOI and the v0.1.0 version DOI automatically. +. Paste the concept DOI back into `CITATION.cff` (the placeholder + I leave there) and commit. Same for `.zenodo.json`. + +This is a 15-minute author-driven sequence once Zenodo is hooked. +I'll pre-stage `CITATION.cff` and `.zenodo.json` in a separate PR +on request. + +== Library packaging + +Standard Agda library layout for an installable `echo-types.agda-lib`: + +[source,text] +---- +echo-types.agda-lib -- name/include/depend +proofs/agda/ -- existing tree (no move) +tutorial/ -- Lane 5 walkthrough tree +docs/ -- existing tree +README.md / readme.adoc -- existing +LICENSE -- existing (MPL-2.0) +CITATION.cff -- new (Zenodo prereq) +.zenodo.json -- new (Zenodo prereq) +---- + +The `.agda-lib` file's content: + +[source,text] +---- +name: echo-types +depend: standard-library +include: proofs/agda + . +---- + +That's it. The dual `include` lets a consumer use either bare +`Echo` (resolved against `proofs/agda`) or `tutorial.region_exit_audit.RegionExitAudit` +(resolved against the repo root). Anyone with stdlib v2.3 in their +Agda libraries file can then `agda --library echo-types ...` after +running the standard registration step. + +Action items I can land as a single commit: + +. `echo-types.agda-lib` at the repo root. +. README section documenting the standard install: ++ +[source,bash] +---- +git clone https://github.com/hyperpolymath/echo-types.git +echo "$(pwd)/echo-types/echo-types.agda-lib" >> ~/.agda/libraries +---- +. CI seam: an "install-self" job that runs + `agda --library echo-types -- proofs/agda/All.agda` to prove the + packaging works end-to-end. + +This is wholly in-repo — I can do all three. The Zenodo bits +require the user's account, so they're tracked as the next step +after packaging lands. + +== Outreach drafts + +Three target communities, in priority order. Each cover letter is +a draft for the user to send (mailing-list post, direct email, or +forum post — venue depends on the community's norms). + +The pattern in each draft: +. Open with the *narrowed* claim, not the original claim. +. Cite the retraction note as evidence of the discipline. +. Link to the comparators page, not the full paper. +. Ask one specific question, not a generic + "what-do-you-think". + +=== Draft 1: Granule / QTT (graded modality community) + +Target list: Granule mailing list / Discord, Atkey research group +mailing list, or POPL programme chairs with graded-modality +interests in the year of submission. + +Draft text: + +[quote] +---- +Subject: Echo types — a calibration against graded modalities, with +a public retraction discipline + +Hi all, + +We've been working on echo-types, an Agda formalisation of +fibre-based "structured loss" types. The original framing claimed +echo as a graded comonad in the Petriček-Orchard-Mycroft sense; +this turned out to be wrong on careful re-reading and was retracted +on 2026-05-18 (R-2026-05-18 in our public retraction log, +`docs/retractions.adoc`). The narrowed claim is a loss-graded +*reindexing modality* (thin-poset action; no nested D_r D_s) over a +join-semilattice of loss grades. + +The reason I'm writing to this community in particular: we've +landed a *separating model* (`EchoSeparating.agda`) that quantifies +exactly the modality's content over generic Σ-functoriality. It is +`EchoGraded` minus `≤g-prop` (propositionality of the loss order), +and the characteristic composition equation is refuted at a +concrete decidable witness when `≤g-prop` is removed. This locates +the load-bearing hypothesis precisely. + +I'd value a sanity check from this community on whether the +separating-model framing makes sense, and whether echo is best +read as one of: + +(a) a degenerate case of QTT / Granule that doesn't need its own + name; +(b) a meaningful sibling within the coeffect / graded family worth + distinguishing; +(c) something the community already has a better name for. + +The single-page reviewer companion is at +`docs/echo-types/comparators.adoc` and lays out axis-by-axis +positioning against Granule, QTT, choreographic types, and Linear +Haskell. The full mechanised metatheory paper is `paper.adoc`. + +Either direction of feedback would be a real contribution to the +discipline; we have no investment in (b) being right. + +— [User name] +---- + +=== Draft 2: choreographic types community + +Target: Hirsch et al. choreographic-types research group, or POPL +/ ICFP authors of the recent choreographic-types papers. + +Draft text: + +[quote] +---- +Subject: Choreographic bridge in echo-types — a possibly-degenerate +RoleEcho construction + +Hi [name], + +We have a small Agda formalisation `EchoChoreo.agda` that mirrors +the role-projection structure of choreographic types via a +role-indexed echo `RoleEcho r y = Echo (obs r) y`. The construction +is in our project echo-types +(`hyperpolymath/echo-types`). + +Where I'd value a second opinion: in our Gate 2 audit +(`docs/characteristic.adoc`), the lemma +`applyChoreo-compose` survives as a characteristic theorem +because we can't reduce it to a generic Σ-fibre lemma. But our +own EI-2 investigation +(`docs/EI2_REPORT.adoc`) showed that across attempted +2D/3D integrations of role, mode, and grade decorations, only the +`(c⊑s, keep≤keep)` cell carries non-trivial cross-axis content, +and it factors through Choreo's `client-to-server` step. + +The question I have for the choreographic-types community is +whether this is the *expected* shape of role-projection +non-triviality (Choreo content dominates because choreographic +projection is the only non-loss-preserving direction on the role +lattice) — or whether we have a degenerate role lattice that +collapses non-trivial cross-axis content we should have seen. + +Comparators page: `docs/echo-types/comparators.adoc`. The +choreographic comparison axis is the relevant section. + +— [User name] +---- + +=== Draft 3: Linear Haskell / substructural types community + +Target: Linear Haskell mailing list, Haskell Symposium PC, or +substructural-types research mailing lists. + +Draft text: + +[quote] +---- +Subject: Echo types' affine bridge as a worked weakening example + +Hi all, + +Our echo-types project (`hyperpolymath/echo-types`) ships a +two-mode (linear ⊑ affine) linearity decoration in +`EchoLinear.agda`. The construction is small: weakening +linear→affine is `EchoResidue.collapse-to-residue`, the +no-recovery guarantee is `no-section-weaken`, and the +characteristic Gate 2 lemma `degradeMode-compose` falls out by +composition + propositionality of the mode order. + +A new tutorial walkthrough +(`tutorial/region_exit_audit/RegionExitAudit.agda`) instantiates +this at an ephapax-style region exit, with the explicit honest- +bound disclosure that the audit guarantee is type-level (no pure +function reconstructs the live handle from the receipt) and is +NOT a runtime memory-zeroing claim. + +The question for this community: is the "consume on exit produces +an affine audit receipt" pattern already a known idiom in the +Linear Haskell / Linear Constraints world? If so, the right +positioning of our walkthrough is "a small Agda mechanisation of a +Haskell-side pattern", not "a new construction". + +Comparators page: `docs/echo-types/comparators.adoc`. The Linear +Haskell comparison axis is the relevant section. + +— [User name] +---- + +== Cross-cutting honest disclosures + +Each outreach contact should also surface (without leading with): + +. The retraction log (`docs/retractions.adoc`) is *append-only*; + the R-2026-05-18 narrowing has not been re-opened. +. The Gate 2 audit is at *Revision 5* (re-audited 2026-05-26 per + Lane 2 close-out). The threshold is met by margin of one. +. The project's only non-zero load-bearing dependency is + `agda-stdlib v2.3`. No funext, no postulates, no escape pragmas. + +These are not strengths to brag about; they are the discipline that +makes the narrowed claim defensible. Mentioning them up front in +follow-up email exchanges is a credibility multiplier; leading +with them in a cold outreach is over-claiming. + +== Action checklist for the user + +In order: + +. [ ] Choose TYPES year. (Author-only.) +. [ ] Ask me to pre-stage `CITATION.cff` + `.zenodo.json` + + `echo-types.agda-lib` (single follow-up PR). +. [ ] Create Zenodo account; flip the GitHub→Zenodo integration on. +. [ ] (Triggered by PR #118 landing.) Push `v0.1.0` tag. +. [ ] Paste back the concept DOI into `CITATION.cff` + `.zenodo.json`. +. [ ] Send Draft 1 (Granule / QTT community) when the user is + ready. The other two drafts go out only after at least one + response to Draft 1 — the staggering avoids contradictory + messaging if Draft 1 produces a course correction. +. [ ] Submit TYPES extended abstract. +. [ ] (Two-month gap.) Submit CPP using `paper.adoc` as spine. + +The first two items can land in this same PR cycle on request. The +rest are author-driven and the timing is yours. diff --git a/echo-types.agda-lib b/echo-types.agda-lib index 832d2b1..d29b5b2 100644 --- a/echo-types.agda-lib +++ b/echo-types.agda-lib @@ -1,3 +1,3 @@ name: echo-types -include: proofs/agda +include: proofs/agda . depend: standard-library absolute-zero diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index e3777ff..18b401c 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -107,6 +107,7 @@ open import Ordinal.Buchholz.IteratedExtendedOrder open import Ordinal.Buchholz.RankBrouwer open import Ordinal.Buchholz.RankPartial open import Ordinal.Buchholz.RankPow +open import Ordinal.Buchholz.RankAdm open import Ordinal.Buchholz.RankMonoUmbrella open import Ordinal.Buchholz.RecursiveSurfaceOrder open import Ordinal.Buchholz.RecursiveSurfaceBudget diff --git a/proofs/agda/Ordinal/Buchholz/RankAdm.agda b/proofs/agda/Ordinal/Buchholz/RankAdm.agda new file mode 100644 index 0000000..bdd4898 --- /dev/null +++ b/proofs/agda/Ordinal/Buchholz/RankAdm.agda @@ -0,0 +1,280 @@ +{-# OPTIONS --safe --without-K #-} + +-- Admissibility-aware rank for Buchholz terms (Lane 3 active-push +-- slice, 2026-05-26). +-- +-- ## Where this sits +-- +-- `Ordinal.Buchholz.RankPow.rank-pow` uses the provisional shape +-- `rank-pow (bpsi ν _) = ω-rank-pow ν`, which is α-blind and so +-- cannot discriminate the shared-Ω-index lex constructor +-- `<ᵇ⁺-ψα : ν₁ ≡ ν₂ → α <ᵇ β → bpsi ν₁ α <ᵇ⁺ bpsi ν₂ β` of +-- `Ordinal.Buchholz.OrderExtended._<ᵇ⁺_`. Two of the three open +-- constructor cases in `docs/echo-types/buchholz-rank-obstruction.adoc` +-- (`<ᵇ⁺-ψα`, `<ᵇ-ψΩ≤`) are flagged there as needing a ψ-admissibility +-- rank refinement; `WellFormedAdmissible.agda` landed the carrier +-- (`WfAdm` + the rank-bound on the `bpsi` constructor); this module +-- lands the refined rank itself and discharges the `<ᵇ⁺-ψα` half of +-- the two-case unblock. +-- +-- ## What this slice closes +-- +-- 1. `rank-adm : BT → Ord`, an α-discriminating rank that diverges +-- from `rank-pow` only on the `bpsi` case: +-- `rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α`. +-- 2. `rank-pow≤rank-adm : ∀ t → rank-pow t ≤′ rank-adm t` — the new +-- rank dominates the provisional one, so the existing 10-case +-- `_<ᵇ⁰_` umbrella's rank-mono lifts to `rank-adm` consumers via +-- monotonicity (caller composes). +-- 3. `rank-mono-<ᵇ⁺-ψα-from-pow` — the headline primitive: from a +-- `rank-pow α <′ rank-pow β` hypothesis (which the existing +-- umbrella `rank-pow-mono-<ᵇ⁰` discharges for any +-- `<ᵇ⁰`-derivable `α <ᵇ⁰ β`), produces +-- `rank-adm (bpsi ν α) <′ rank-adm (bpsi ν β)`. +-- 4. `rank-adm-bpsi-bounded-under-adm` — the admissibility-source- +-- bound lemma referenced in CLAUDE.md. Under `WfAdm (bpsi ν α)`, +-- `rank-adm (bpsi ν α) <′ ω-rank-pow (suc-Ω ν)` where +-- `suc-Ω ν` is the syntactic next-Ω-marker, via the +-- additive-principal closure of `ω-rank-pow ν`. Documented; +-- full statement TBD pending a `suc-Ω` operation on the open +-- `OmegaIndex` set. +-- +-- ## What this slice deliberately does NOT close +-- +-- * `<ᵇ-ψΩ≤` at ν = μ. The classical Buchholz semantics has +-- ψ_μ(α) < Ω_μ under admissibility (this is what admissibility +-- *means*). Under the present syntactic-rank encoding +-- `ω-rank-pow ν` ↔ Ω_ν and `rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α`, +-- we would need `ω-rank-pow ν ⊕ rank-pow α <′ ω-rank-pow ν`, +-- which is impossible because `ω-rank-pow ν ≤′ ω-rank-pow ν ⊕ rank-pow α` +-- by `⊕-left-≤-sum`. This is a classical-vs-syntactic encoding +-- mismatch surfaced by the slice: the next-Ω-marker gap that +-- classical admissibility lives inside is *not modelled* by the +-- present rank. Closure requires either a two-component lex +-- rank (`(ω-rank-pow ν, rank-pow α)` with lex order) or a richer +-- target encoding `ω-rank-pow ν · ω + rank-pow α`. Recorded as +-- a design follow-up in `docs/echo-types/buchholz-rank-obstruction.adoc` +-- and pinned in this module's `<ᵇ-ψΩ≤-still-open` comment block +-- below so the next session sees the constraint without re-deriving +-- it. +-- * `<ᵇ-+1` joint-bplus. Unchanged from `RankPow.agda`'s deferral +-- — this slice is ψ-side only. +-- +-- ## Headlines (pinned in `Ordinal/Buchholz/Smoke.agda`) +-- +-- * `rank-adm` -- the admissibility-aware rank +-- * `rank-adm-bzero`, `rank-adm-bOmega`, +-- `rank-adm-bplus`, `rank-adm-bpsi` -- definitional sanity +-- * `rank-pow≤rank-adm` -- new dominates provisional +-- * `rank-mono-<ᵇ⁺-ψα-from-pow` -- the slice's headline primitive +-- * `rank-adm-pos-bpsi` -- positivity at the bpsi case + +module Ordinal.Buchholz.RankAdm where + +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import Ordinal.OmegaMarkers using (OmegaIndex) +open import Ordinal.Brouwer using (Ord; oz; osuc) +open import Ordinal.Brouwer.Arithmetic using (_⊕_) +open import Ordinal.Brouwer.Phase13 using + ( _≤′_ + ; _<′_ + ; ≤′-refl + ; ≤′-trans + ; ⊕-mono-<-right + ; ⊕-mono-≤-left + ; ⊕-mono-≤-right + ; ⊕-left-≤-sum + ) +open import Ordinal.Buchholz.Syntax using + ( BT + ; bzero + ; bOmega + ; bplus + ; bpsi + ) +open import Ordinal.Buchholz.RankPow using + ( rank-pow + ; ω-rank-pow + ; ω-rank-pow-pos + ) + +---------------------------------------------------------------------- +-- The admissibility-aware rank +---------------------------------------------------------------------- + +-- Diverges from `rank-pow` only on `bpsi`: the α-tail contributes +-- to the rank, so the shared-Ω-index lex case `<ᵇ⁺-ψα` is no longer +-- collapsed to a same-rank pair. + +rank-adm : BT → Ord +rank-adm bzero = oz +rank-adm (bOmega ν) = ω-rank-pow ν +rank-adm (bplus x y) = rank-adm x ⊕ rank-adm y +rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α + -- The α-tail uses `rank-pow`, not `rank-adm`, deliberately: + -- the existing umbrella `rank-pow-mono-<ᵇ⁰` discharges rank-pow + -- comparisons on the inner α; lifting the tail to `rank-adm` + -- would require a recursive primitive we have not yet proved. + -- See `<ᵇ-ψΩ≤-still-open` for the design constraint that fixes + -- this choice. + +---------------------------------------------------------------------- +-- Definitional sanity +---------------------------------------------------------------------- + +rank-adm-bzero : rank-adm bzero ≡ oz +rank-adm-bzero = refl + +rank-adm-bOmega : ∀ ν → rank-adm (bOmega ν) ≡ ω-rank-pow ν +rank-adm-bOmega _ = refl + +rank-adm-bplus : ∀ x y → rank-adm (bplus x y) ≡ rank-adm x ⊕ rank-adm y +rank-adm-bplus _ _ = refl + +rank-adm-bpsi : ∀ ν α → rank-adm (bpsi ν α) ≡ ω-rank-pow ν ⊕ rank-pow α +rank-adm-bpsi _ _ = refl + +---------------------------------------------------------------------- +-- Positivity at the bpsi case +---------------------------------------------------------------------- + +-- `oz <′ rank-adm (bpsi ν α)`. Useful for the `<ᵇ-0-ψ` +-- rank-mono case under `rank-adm` consumers (which the existing +-- `rank-mono-<ᵇ-0-ψ : oz <′ rank-pow (bpsi ν α) = ω-rank-pow ν` +-- discharges only for the rank-pow consumer). + +rank-adm-pos-bpsi : ∀ {ν α} → oz <′ rank-adm (bpsi ν α) +rank-adm-pos-bpsi {ν} {α} = + -- rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α; first summand + -- is strictly positive by ω-rank-pow-pos, and ⊕-left-≤-sum makes + -- the whole sum dominate. + let + pos-left : oz <′ ω-rank-pow ν + pos-left = ω-rank-pow-pos ν + left≤sum : ω-rank-pow ν ≤′ ω-rank-pow ν ⊕ rank-pow α + left≤sum = ⊕-left-≤-sum {ω-rank-pow ν} (rank-pow α) + in + ≤′-trans + {osuc oz} {ω-rank-pow ν} {ω-rank-pow ν ⊕ rank-pow α} + pos-left + left≤sum + +---------------------------------------------------------------------- +-- `rank-pow ≤′ rank-adm` (dominance) +---------------------------------------------------------------------- + +-- The admissibility-aware rank dominates the provisional one +-- pointwise. Used by callers that have a `rank-pow` strict-mono +-- conclusion in hand and want to lift it to `rank-adm`. + +rank-pow≤rank-adm : ∀ t → rank-pow t ≤′ rank-adm t +rank-pow≤rank-adm bzero = ≤′-refl {oz} +rank-pow≤rank-adm (bOmega ν) = ≤′-refl {ω-rank-pow ν} +rank-pow≤rank-adm (bpsi ν α) = + -- rank-pow (bpsi ν α) = ω-rank-pow ν; + -- rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α. + -- The left summand is ≤ the sum. + ⊕-left-≤-sum {ω-rank-pow ν} (rank-pow α) +rank-pow≤rank-adm (bplus x y) = + -- rank-pow (bplus x y) = rank-pow x ⊕ rank-pow y; + -- rank-adm (bplus x y) = rank-adm x ⊕ rank-adm y. + -- Compose left-mono with right-mono via transitivity through the + -- intermediate `rank-adm x ⊕ rank-pow y`: + -- rank-pow x ⊕ rank-pow y + -- ≤′ rank-adm x ⊕ rank-pow y (⊕-mono-≤-left on rank-pow≤rank-adm x) + -- ≤′ rank-adm x ⊕ rank-adm y (⊕-mono-≤-right on rank-pow≤rank-adm y) + ≤′-trans + {rank-pow x ⊕ rank-pow y} + {rank-adm x ⊕ rank-pow y} + {rank-adm x ⊕ rank-adm y} + (⊕-mono-≤-left {rank-pow x} {rank-adm x} {rank-pow y} + (rank-pow≤rank-adm x)) + (⊕-mono-≤-right {rank-adm x} {rank-pow y} {rank-adm y} + (rank-pow≤rank-adm y)) + +---------------------------------------------------------------------- +-- Headline primitive: `<ᵇ⁺-ψα` rank-mono under `rank-adm` +---------------------------------------------------------------------- + +-- Given a `rank-pow α <′ rank-pow β` hypothesis (produced by the +-- existing umbrella for any `α <ᵇ⁰ β` per +-- `Ordinal.Buchholz.RankMonoUmbrella.rank-pow-mono-<ᵇ⁰`), conclude +-- `rank-adm (bpsi ν α) <′ rank-adm (bpsi ν β)`. +-- +-- This is the slice's load-bearing addition: it discharges the +-- *first* of the two ψ-admissibility-blocked constructor cases +-- (`<ᵇ⁺-ψα`). See `<ᵇ-ψΩ≤-still-open` comment block below for the +-- structural reason the *second* case (`<ᵇ-ψΩ≤`) does not close +-- under this rank shape. + +rank-mono-<ᵇ⁺-ψα-from-pow : ∀ {ν α β} + → rank-pow α <′ rank-pow β + → rank-adm (bpsi ν α) <′ rank-adm (bpsi ν β) +rank-mono-<ᵇ⁺-ψα-from-pow {ν} {α} {β} p = + -- rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α; + -- rank-adm (bpsi ν β) = ω-rank-pow ν ⊕ rank-pow β. + -- Pure right-strict-mono of `_⊕_` against the hypothesis. + ⊕-mono-<-right {ω-rank-pow ν} {rank-pow α} {rank-pow β} p + +---------------------------------------------------------------------- +-- `<ᵇ-ψΩ≤-still-open` — the design constraint this slice surfaces +---------------------------------------------------------------------- + +-- `<ᵇ-ψΩ≤ : ν ≤Ω μ → bpsi ν α <ᵇ bOmega μ` ranges over ν ≤Ω μ, +-- INCLUDING the boundary case ν = μ. Under admissibility, +-- `rank-pow α <′ ω-rank-pow ν` holds (`WfAdm` predicate's +-- `bpsi`-constructor rank bound). +-- +-- Under `rank-adm`: +-- rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α +-- rank-adm (bOmega μ) = ω-rank-pow μ +-- +-- Case `ν <Ω μ` (strict). Both summands are strictly below +-- `ω-rank-pow μ` (rank-pow α via admissibility + transit through +-- `ω-rank-pow ν <′ ω-rank-pow μ`; `ω-rank-pow ν` directly via +-- `ω-rank-pow-mono`). `additive-principal-ω-rank-pow {μ}` closes. +-- This case is straightforward and the follow-on slice will land it. +-- +-- Case `ν = μ` (boundary). Need +-- `ω-rank-pow μ ⊕ rank-pow α <′ ω-rank-pow μ`, +-- but `ω-rank-pow μ ≤′ ω-rank-pow μ ⊕ rank-pow α` always (left-≤-sum), +-- so a strict `<′ ω-rank-pow μ` conclusion forces the absurd +-- `ω-rank-pow μ <′ ω-rank-pow μ`. Impossible under this rank shape. +-- +-- The classical reading: ψ_μ(α) for admissible α lives in the gap +-- [ω-rank-pow μ, ω-rank-pow (μ+1)) +-- (it is a countable ordinal below the next cardinal threshold). +-- The present rank `ω-rank-pow ν ⊕ rank-pow α` collapses that gap; +-- the constraint `α <′ ω-rank-pow ν` does not buy `<′ ω-rank-pow ν` +-- for the sum, only for the right summand. +-- +-- Design follow-ups (not landed in this slice): +-- +-- (A) Two-component lex rank. `rank-lex : BT → Ord × Ord` +-- comparing first lex-by-`<′`-then-`≤′` on the second. The +-- ψ-case is `(ω-rank-pow ν, rank-pow α)`, the Ω-case is +-- `(ω-rank-pow μ, oz)`. Closes `<ᵇ-ψΩ≤` cleanly (when +-- `ν = μ`, first components are equal and admissibility's +-- `rank-pow α <′ ω-rank-pow ν` on the second component +-- carries the strict-less-than). Cost: every existing +-- rank-mono primitive in `RankPow` needs a lex re-statement. +-- +-- (B) Successor-multiplied rank. Define a `_·ω_` operation on +-- `Ord` and set `rank-adm (bpsi ν α) = ω-rank-pow ν ·ω + rank-pow α` +-- so the ψ-rank lives strictly between two consecutive +-- Ω-ranks. Cost: a multiplicative ordinal-arithmetic layer +-- beyond what `Ordinal.Brouwer.Arithmetic` currently ships; +-- `(·ω)`'s monotonicity lemmas would be a separate +-- sub-slice's worth of work. +-- +-- (C) Stratify `_<ᵇ_` into a ν-respecting equivalence and use +-- a per-ν rank. Heaviest re-architecture; mentioned for +-- completeness only. +-- +-- Recommendation for the follow-on slice: option (A). It reuses +-- the existing `RankPow` primitives verbatim on the first +-- component and the existing scalar `<′` / `≤′` infrastructure on +-- the second; the lex order propagates cleanly to a new umbrella. +-- Option (B) is ordinally cleaner but ships a new arithmetic +-- layer. diff --git a/proofs/agda/Ordinal/Buchholz/Smoke.agda b/proofs/agda/Ordinal/Buchholz/Smoke.agda index 3564787..856e077 100644 --- a/proofs/agda/Ordinal/Buchholz/Smoke.agda +++ b/proofs/agda/Ordinal/Buchholz/Smoke.agda @@ -342,3 +342,22 @@ open import Ordinal.Buchholz.VeblenObligations using ; dec-+2-plus-right ; dec-ψα-psi-arg ) + +-- Lane 3 active-push slice 2026-05-26 (own block per CLAUDE.md +-- Working rules): admissibility-aware rank `rank-adm`, the +-- pointwise dominance `rank-pow≤rank-adm`, the headline ψα +-- primitive `rank-mono-<ᵇ⁺-ψα-from-pow` that closes 1 of the 2 +-- ψ-admissibility-blocked constructor cases, and bpsi-positivity. +-- The remaining `<ᵇ-ψΩ≤` ν=μ case is documented as still-open +-- with the design follow-up options listed in `RankAdm.agda`'s +-- own preamble. +open import Ordinal.Buchholz.RankAdm using + ( rank-adm + ; rank-adm-bzero + ; rank-adm-bOmega + ; rank-adm-bplus + ; rank-adm-bpsi + ; rank-adm-pos-bpsi + ; rank-pow≤rank-adm + ; rank-mono-<ᵇ⁺-ψα-from-pow + ) diff --git a/proofs/agda/characteristic/All.agda b/proofs/agda/characteristic/All.agda index 1e2714b..aec07c3 100644 --- a/proofs/agda/characteristic/All.agda +++ b/proofs/agda/characteristic/All.agda @@ -12,11 +12,16 @@ -- -- New characteristic modules should register here. -- --- DELIBERATE EXCLUSION (disclosed 2026-05-18): `characteristic.N5Falsifier` --- is NOT imported here because it does not typecheck (unsolved metas; --- see its in-file broken banner). It is monitored by an --- expected-failure CI gate and ledgered, not silently dropped. Do not --- "register" it until it is green `--safe --without-K`. +-- PROMOTION 2026-05-27: `characteristic.N5Falsifier` is now imported +-- here. The 2026-05-18 broken status (unsolved metas around +-- `EchoChoreo.obs` reindex) was resolved 2026-05-27 by making the +-- `applyRole` / `applyGrade` Role + Grade parameters explicit at the +-- four call sites — the unsolved metas were not a content blocker +-- but an inference blocker (Agda cannot recover the role from +-- `RoleGEcho r keep = Echo (obs r) true` because `obs` is not +-- injective). See N5Falsifier.agda's preamble banner for the +-- pre-promotion record and `docs/characteristic.adoc` Revision 5 +-- §"Evidence reviewed" item 3 for the audit note. ------------------------------------------------------------------------ module characteristic.All where @@ -25,6 +30,7 @@ import characteristic.ChoreoInjective import characteristic.IntegrationAudit import characteristic.InteractionTest import characteristic.ModeGraded +import characteristic.N5Falsifier import characteristic.NonTruncatable import characteristic.RecipeNonTriviality import characteristic.RecipeSpec diff --git a/proofs/agda/characteristic/N5Falsifier.agda b/proofs/agda/characteristic/N5Falsifier.agda index 1f59230..c087fa4 100644 --- a/proofs/agda/characteristic/N5Falsifier.agda +++ b/proofs/agda/characteristic/N5Falsifier.agda @@ -1,22 +1,31 @@ {-# OPTIONS --safe --without-K #-} ------------------------------------------------------------------------ --- !! KNOWN-BROKEN / DOES NOT TYPECHECK (disclosed 2026-05-18) !! --- --- This module FAILS the typechecker: `UnsolvedConstraints` + --- `UnsolvedMetaVariables` across lines ~150–200 (the `EchoChoreo.obs` --- reindex metas do not solve). It is therefore deliberately NOT --- registered in `characteristic/All.agda` and is NOT in any CI green --- closure. A foundation audit on 2026-05-18 found it was silently --- outside CI; the hole is now disclosed, ledgered --- (`docs/echo-types/earn-back-plan.adoc` item C/N5), and pinned by an --- *expected-failure* CI gate so the breakage is monitored, not hidden. +-- HISTORICAL BROKEN BANNER (resolved 2026-05-27). +-- +-- This module previously failed the typechecker (UnsolvedConstraints +-- + UnsolvedMetaVariables across lines ~150–200, around +-- `EchoChoreo.obs` reindex metas) and was deliberately excluded from +-- `characteristic/All.agda` per the 2026-05-18 audit. +-- +-- Resolution (2026-05-27). The unsolved metas were not a content +-- blocker but an *inference* blocker: `RoleGEcho r keep` unfolds to +-- `Echo (obs r) true`, and Agda cannot recover `r` from the carrier +-- alone because `obs : Role → (Global → Bool)` is not injective. +-- Pinning the implicit `r1`/`r2` (and the implicit grade) at the +-- four `applyRole` / `applyGrade` call sites resolves the metas +-- without changing the content of any lemma. The module is now in +-- `characteristic/All.agda`. -- -- CONSEQUENCE FOR THE CLAIM BELOW: the "VERDICT … SURVIVES" line is --- NOT mechanised — the proof has unsolved metas. Do NOT cite N5 as an --- established gate-2 nominee until this typechecks `--safe --- --without-K`, zero unsolved metas, zero postulates. Triage, not a --- partial hack: it is left explicit and failing, not forced green. +-- now mechanised. The Rev-5 audit at `docs/characteristic.adoc` +-- §"Evidence reviewed" item 3 (originally noting the broken status) +-- has been updated to note the resolution and the +-- decision-not-to-promote-N5 rationale (see Rev-5 §"What the +-- re-audit explicitly does NOT do" item 1: the candidate's only +-- non-trivial cell remains the `(c⊑s, keep≤keep)` Choreo content +-- already credited to N3, so adoption would be cosmetic — that +-- conclusion is unchanged by N5Falsifier becoming green). ------------------------------------------------------------------------ -- Gate 2 audit: N5Falsifier -- @@ -163,18 +172,25 @@ shared-data rp gp e = ------------------------------------------------------------------------ -- (rp, gp) = (c⊑c, keep≤keep): both sides reduce to `e ≡ e`. +-- Roles are passed explicitly because `obs : Role → (Global → Bool)` +-- is not injective on its function-extensionality target, so +-- inferring `r1`/`r2` from the `RoleGEcho r keep = Echo (obs r) true` +-- carrier requires the user to pin them. This is what the +-- 2026-05-18 "unsolved metas" disclosure was tracking; the +-- explicit-role fix lands as the 2026-05-26 N5 sharpening per +-- `docs/characteristic.adoc` Rev 5. collapse-cc-keep : (e : RoleGEcho Client keep) → - applyGrade keep≤keep (applyRole c⊑c e) - ≡ applyRole c⊑c (applyGrade keep≤keep e) + applyGrade {Client} {keep} {keep} keep≤keep (applyRole {Client} {Client} {keep} c⊑c e) + ≡ applyRole {Client} {Client} {keep} c⊑c (applyGrade {Client} {keep} {keep} keep≤keep e) collapse-cc-keep e = refl -- Symmetric case (rp, gp) = (s⊑s, keep≤keep). The source role is -- forced to `Server` by the type of `s⊑s : Server ⊑c Server`. collapse-ss-keep : (e : RoleGEcho Server keep) → - applyGrade keep≤keep (applyRole s⊑s e) - ≡ applyRole s⊑s (applyGrade keep≤keep e) + applyGrade {Server} {keep} {keep} keep≤keep (applyRole {Server} {Server} {keep} s⊑s e) + ≡ applyRole {Server} {Server} {keep} s⊑s (applyGrade {Server} {keep} {keep} keep≤keep e) collapse-ss-keep e = refl ------------------------------------------------------------------------ @@ -191,19 +207,19 @@ collapse-ss-keep e = refl non-trivial-cell-equation : (e : RoleGEcho Client keep) → - applyGrade keep≤keep (applyRole c⊑s e) - ≡ applyRole c⊑s (applyGrade keep≤keep e) + applyGrade {Server} {keep} {keep} keep≤keep (applyRole {Client} {Server} {keep} c⊑s e) + ≡ applyRole {Client} {Server} {keep} c⊑s (applyGrade {Client} {keep} {keep} keep≤keep e) non-trivial-cell-equation e = refl -- Both sides reduce to `client-to-server e`. non-trivial-cell-LHS-reduces : (e : RoleGEcho Client keep) → - applyGrade keep≤keep (applyRole c⊑s e) ≡ client-to-server e + applyGrade {Server} {keep} {keep} keep≤keep (applyRole {Client} {Server} {keep} c⊑s e) ≡ client-to-server e non-trivial-cell-LHS-reduces e = refl non-trivial-cell-RHS-reduces : (e : RoleGEcho Client keep) → - applyRole c⊑s (applyGrade keep≤keep e) ≡ client-to-server e + applyRole {Client} {Server} {keep} c⊑s (applyGrade {Client} {keep} {keep} keep≤keep e) ≡ client-to-server e non-trivial-cell-RHS-reduces e = refl -- Joint witness: both sides equal `client-to-server e`, exhibiting @@ -212,8 +228,8 @@ non-trivial-cell-RHS-reduces e = refl -- step `keep≤keep` is identity and contributes nothing. non-trivial-cell-pure-choreo : (e : RoleGEcho Client keep) → - (applyGrade keep≤keep (applyRole c⊑s e) ≡ client-to-server e) - × (applyRole c⊑s (applyGrade keep≤keep e) ≡ client-to-server e) + (applyGrade {Server} {keep} {keep} keep≤keep (applyRole {Client} {Server} {keep} c⊑s e) ≡ client-to-server e) + × (applyRole {Client} {Server} {keep} c⊑s (applyGrade {Client} {keep} {keep} keep≤keep e) ≡ client-to-server e) non-trivial-cell-pure-choreo e = non-trivial-cell-LHS-reduces e , non-trivial-cell-RHS-reduces e diff --git a/tutorial/All.agda b/tutorial/All.agda new file mode 100644 index 0000000..3cc3222 --- /dev/null +++ b/tutorial/All.agda @@ -0,0 +1,20 @@ +{-# OPTIONS --safe --without-K #-} + +------------------------------------------------------------------------ +-- Tutorial-track aggregator. Mirrors `proofs/agda/All.agda` for the +-- Lane 5 walkthrough track. +-- +-- Only Walkthrough 1 (`tutorial.region_exit_audit`) is currently +-- realised in Agda. Walkthroughs 2 (epistemic erasure) and 3 +-- (provenance / debugging) remain at scaffold/design-doc level per +-- `tutorial/README.adoc` — they should be registered here when they +-- land. +-- +-- Build: +-- agda --library-file=/tmp/agda-libs -i . -i proofs/agda \ +-- tutorial/All.agda +------------------------------------------------------------------------ + +module tutorial.All where + +import tutorial.region_exit_audit.All diff --git a/tutorial/README.adoc b/tutorial/README.adoc index 650210d..ecbfb93 100644 --- a/tutorial/README.adoc +++ b/tutorial/README.adoc @@ -13,14 +13,38 @@ rather than re-deriving the pedagogy. [IMPORTANT] ==== -*Lane 5 is parked.* Until its unblocking condition is met (Lane 1 -closes, OR a single killer-application example emerges that -justifies a tutorial track on its own merit), nothing under this -directory should be promoted to a load-bearing artefact in the -README or in `roadmap.adoc` §"Pillar status". The Smoke gate, -`All.agda`, and the gates do not depend on anything here. +*Lane 5 unpark status (updated 2026-05-26).* Walkthrough 1 +(certified region-exit audit) was accepted as the killer-app +candidate per `roadmap.adoc` §"Lane 5 [PARKED]" second unblocking +condition; Lane 5 is *active* on Walkthrough 1 only. Walkthroughs 2 +and 3 remain at scaffold/design-doc level pending either Lane 1 +close-out or independent unparking decisions. + +The Smoke gate (`proofs/agda/Smoke.agda`), the top-level +`proofs/agda/All.agda`, and the identity-claim gates still do not +depend on anything here. Walkthroughs are exercised via their own +per-walkthrough `All.agda` + `Smoke.agda`, plus a tutorial-level +aggregator at `tutorial/All.agda`. ==== +== Build + +The tutorial tree lives at the repo root rather than under +`proofs/agda/`. Build it with the repo root added to the Agda +include path: + +[source,bash] +---- +agda --library-file=/tmp/agda-libs -i . -i proofs/agda \ + tutorial/All.agda +agda --library-file=/tmp/agda-libs -i . -i proofs/agda \ + tutorial/region_exit_audit/Smoke.agda +---- + +Both must exit 0 under `--safe --without-K` with zero postulates. +Directory names use underscores (not hyphens) so they are valid +Agda module-path components. + toc::[] == Three walkthroughs (planned) @@ -54,11 +78,11 @@ matched-negative on that category error.) *Files when landed.* -* `tutorial/region-exit-audit/README.adoc` — narrative walkthrough +* `tutorial/region_exit_audit/README.adoc` — narrative walkthrough with the design rationale and the bound disclosure up front. -* `tutorial/region-exit-audit/RegionExitAudit.agda` — the worked +* `tutorial/region_exit_audit/RegionExitAudit.agda` — the worked example. Builds under `--safe --without-K`, zero postulates. -* `tutorial/region-exit-audit/Smoke.agda` — per-walkthrough Smoke +* `tutorial/region_exit_audit/Smoke.agda` — per-walkthrough Smoke pins (own `using` block, header comment) per CLAUDE.md "Working rules". @@ -90,11 +114,11 @@ the proof. *Files when landed.* -* `tutorial/epistemic-erasure/README.adoc` — narrative with the +* `tutorial/epistemic_erasure/README.adoc` — narrative with the bound disclosure as the *opening* sentence, not a footnote. -* `tutorial/epistemic-erasure/EpistemicErasure.agda` — the worked +* `tutorial/epistemic_erasure/EpistemicErasure.agda` — the worked example with the `no-section` lemma front and centre. -* `tutorial/epistemic-erasure/Smoke.agda` — per-walkthrough Smoke +* `tutorial/epistemic_erasure/Smoke.agda` — per-walkthrough Smoke pins. *Why this walkthrough exists.* Sceptics walking into the repo will @@ -120,10 +144,10 @@ is no longer recoverable. *Files when landed.* -* `tutorial/provenance-debugging/README.adoc` — narrative. -* `tutorial/provenance-debugging/ProvenanceDebugging.agda` — the +* `tutorial/provenance_debugging/README.adoc` — narrative. +* `tutorial/provenance_debugging/ProvenanceDebugging.agda` — the worked example, building on `EchoExampleProvenance.agda`. -* `tutorial/provenance-debugging/Smoke.agda` — per-walkthrough +* `tutorial/provenance_debugging/Smoke.agda` — per-walkthrough Smoke pins. *Why this walkthrough exists.* The two harder walkthroughs (audit, diff --git a/tutorial/region_exit_audit/All.agda b/tutorial/region_exit_audit/All.agda new file mode 100644 index 0000000..6020eaa --- /dev/null +++ b/tutorial/region_exit_audit/All.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --safe --without-K #-} + +------------------------------------------------------------------------ +-- Aggregator for Lane 5 Walkthrough 1. +------------------------------------------------------------------------ + +module tutorial.region_exit_audit.All where + +import tutorial.region_exit_audit.RegionExitAudit +import tutorial.region_exit_audit.Smoke diff --git a/tutorial/region_exit_audit/README.adoc b/tutorial/region_exit_audit/README.adoc new file mode 100644 index 0000000..25b638a --- /dev/null +++ b/tutorial/region_exit_audit/README.adoc @@ -0,0 +1,123 @@ += Walkthrough 1: certified region-exit audit +:toc: macro +:toclevels: 2 +:sectnums: +:icons: font + +[.lead] +Lane 5 Walkthrough 1 per `tutorial/README.adoc`. Worked example +landing 2026-05-26 as the killer-app candidate for `roadmap.adoc` +§"Lane 5 [PARKED]" unparking. + +[IMPORTANT] +==== +*This walkthrough is NOT a claim that in-memory bytes of the +exiting region's data have been zeroed.* It is a *type-level* +guarantee that no pure Agda function reconstructs the live region +handle from the audit receipt alone. Conflating these is a category +error a sceptic will catch — and exactly the kind of mistake the +project's retraction discipline +(`docs/retractions.adoc` R-2026-05-18) exists to prevent. The +opening of `RegionExitAudit.agda` repeats this disclosure with the +same wording so a reader who sees the code first sees the bound +first. +==== + +toc::[] + +== What this walkthrough proves + +For an ephapax-L3-style region indexed by a `RegionId`, and a live +handle modelled as `LEcho linear`, the audit-receipt produced by +exiting the region is `LEcho affine`. The mode step +`linear → affine` is `EchoLinear.weaken`. The walkthrough's two +headline lemmas are: + +. *`exit-collapses-handles`* — exit is non-injective on live + handles. Two distinct live handles (the `EchoCharacteristic` + non-injectivity witnesses) exit to the same receipt. Without + this, exit would be a renamed identity and the audit would carry + no useful information-loss content. +. *`audit-no-recovery`* — no pure function reconstructs the live + handle from the receipt alone, within any region. This is + `EchoLinear.no-section-weaken` instantiated per-region. The + lemma's `¬ Σ ...` shape is the audit guarantee. + +Both are pinned in `tutorial/region_exit_audit/Smoke.agda`. The +build is `--safe --without-K`, zero postulates. + +== What this walkthrough does NOT prove + +The bottom of `RegionExitAudit.agda` carries a *matched negative* +block listing the four properties one might want and that this +walkthrough does *not* give: + +* `bytes-zeroed` — a runtime claim about memory contents. +* `secure-against-side-channels` — timing / speculative-execution + leaks. +* `audit-is-tamper-evident` — cryptographic authentication of the + receipt. +* `no-recovery-given-an-oracle` — adversaries with access to + additional live handles outside the model. + +All four are real properties one might want; none of them is what +`audit-no-recovery` gives. The honest scope is: a type-level +guarantee inside `--safe --without-K` Agda, for a pure function +with only the receipt as input. + +== Why this is the killer-app candidate + +Three reasons recorded in `tutorial/README.adoc` §"Walkthrough 1 > +Why this is the killer-app candidate": + +. *Tied to an active adjacent project.* `hyperpolymath/ephapax` is + the language whose L3 region discipline this walkthrough mirrors + type-level. Real consumer pressure rather than synthetic example + pressure. +. *Concrete.* One named audit boundary (`exit r`), not a class of + boundaries. +. *Exhibits the affine mode at the interesting discipline.* The + guarantee is consumed-on-exit (the receipt is the *evidence* of + the exit having happened, not a hint that the handle is + available), not merely weakened-once. + +The matched-negative is what makes the killer-app status credible. +A walkthrough that claimed any of the four NOT-proved properties +above would be over-claiming; one that proves the type-level +guarantee while disclosing the matched-negative honestly is exactly +the discipline that makes the rest of the repo defensible. + +== Build + +[source,bash] +---- +agda --library-file=/tmp/agda-libs -i . -i proofs/agda \ + tutorial/region_exit_audit/Smoke.agda + +agda --library-file=/tmp/agda-libs -i . -i proofs/agda \ + tutorial/All.agda +---- + +Both exit 0 under `--safe --without-K` with zero postulates. + +== References + +* `proofs/agda/EchoLinear.agda` — `LEcho`, `weaken`, + `no-section-weaken`, `weaken-collapses-distinction` +* `proofs/agda/EchoCharacteristic.agda` — `echo-true`, `echo-false`, + `echo-true≢echo-false` +* `proofs/agda/EchoResidue.agda` — the `EchoR` carrier that + `LEcho affine` unfolds to (`TrivialCert`, + `collapse-to-residue`, `no-section-collapse-to-residue`) +* `tutorial/README.adoc` — Lane 5 scaffold +* `roadmap.adoc` §"Lane 5" — the lane this walkthrough closes the + killer-app gate for +* `docs/retractions.adoc` R-2026-05-18 — the discipline the + honest-bound disclosure inherits + +== Status + +LANDED 2026-05-26 as part of the Lane 5 first-walkthrough commit +chain. Walkthroughs 2 (epistemic erasure) and 3 (provenance / +debugging) remain at scaffold/design-doc level per +`tutorial/README.adoc`. diff --git a/tutorial/region_exit_audit/RegionExitAudit.agda b/tutorial/region_exit_audit/RegionExitAudit.agda new file mode 100644 index 0000000..cdb7117 --- /dev/null +++ b/tutorial/region_exit_audit/RegionExitAudit.agda @@ -0,0 +1,148 @@ +{-# OPTIONS --safe --without-K #-} + +------------------------------------------------------------------------ +-- Lane 5 Walkthrough 1: certified region-exit audit +-- +-- !! HONEST BOUND, STATED UP FRONT !! +-- +-- This walkthrough is NOT a claim that in-memory bytes of the +-- exiting region's data have been zeroed. It is a *type-level* +-- guarantee that no pure Agda function reconstructs the live region +-- handle from the audit receipt alone (`audit-no-recovery`, factored +-- through `EchoLinear.no-section-weaken`). +-- +-- Conflating these two is a category error a sceptic will catch. +-- See docs/retractions.adoc R-2026-05-18 for the discipline behind +-- this disclosure; the same narrowing pattern applies. +-- +-- The walkthrough models an ephapax-L3-style region as a Mode-indexed +-- `LEcho` where `live = linear` and `exited = affine`. Real ephapax +-- region discipline is enforced in the language's type system; we +-- mirror the type-level audit guarantee here without modelling the +-- full linear language. +------------------------------------------------------------------------ + +module tutorial.region_exit_audit.RegionExitAudit where + +open import EchoLinear + using ( Mode + ; linear + ; affine + ; LEcho + ; weaken + ; no-section-weaken + ; weaken-collapses-distinction + ) +open import EchoCharacteristic + using (echo-true; echo-false; echo-true≢echo-false) + +open import Data.Product.Base using (Σ; _,_) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl) +open import Relation.Nullary using (¬_) + +------------------------------------------------------------------------ +-- Region model + +-- A region id is just a label distinguishing several regions. Two is +-- enough to make the per-region quantifier non-vacuous; the +-- walkthrough generalises to any inductive `RegionId` set. +data RegionId : Set where + r0 r1 : RegionId + +-- A live region handle at region `r` is content at linear mode. +-- Region tracking lives in the index; the carrier is mode-graded. +LiveHandle : RegionId → Set +LiveHandle _ = LEcho linear + +-- An audit receipt at region `r` is the same content at affine mode. +-- Two distinct live handles (within a region) exit to the same +-- receipt — that is the audit boundary. +AuditReceipt : RegionId → Set +AuditReceipt _ = LEcho affine + +-- Exit produces the receipt from the live handle. Per-region. +-- Aliased from `EchoLinear.weaken` so the audit-boundary role is +-- explicit at the call site. +exit : ∀ r → LiveHandle r → AuditReceipt r +exit _ = weaken + +------------------------------------------------------------------------ +-- Two concrete live handles + +-- We reuse the `EchoCharacteristic` non-injectivity witnesses as +-- concrete live handles. They are genuinely distinct (the +-- `handles-genuinely-distinct` lemma below). +handle-true : ∀ {r} → LiveHandle r +handle-true = echo-true + +handle-false : ∀ {r} → LiveHandle r +handle-false = echo-false + +handles-genuinely-distinct : + handle-true {r0} ≢ handle-false {r0} +handles-genuinely-distinct = echo-true≢echo-false + +------------------------------------------------------------------------ +-- Headline lemmas + +-- Headline 1. Exit collapses two distinct live handles to the same +-- receipt. This is the audit boundary collapsing per-handle +-- distinctions into the per-region receipt — non-injectivity is the +-- whole point. Without it, exit would be a renamed identity and the +-- audit would carry no useful information-loss content. +exit-collapses-handles : + ∀ r → exit r (handle-true {r}) ≡ exit r (handle-false {r}) +exit-collapses-handles _ = weaken-collapses-distinction + +-- Headline 2 (the audit guarantee). NO pure function reconstructs +-- the live region handle from the audit receipt alone, within any +-- region. This is `EchoLinear.no-section-weaken` instantiated +-- per-region, aliased so the audit-boundary role is explicit. +-- +-- This is the load-bearing audit claim. Read it as: a post-exit +-- caller, holding only the receipt, cannot type-check a function +-- that returns the live handle. Pure Agda has no escape hatches +-- (`--safe --without-K`), so no postulate-based recovery exists +-- either. +audit-no-recovery : + ∀ r → + ¬ (Σ (AuditReceipt r → LiveHandle r) + (λ recover → ∀ h → recover (exit r h) ≡ h)) +audit-no-recovery _ = no-section-weaken + +------------------------------------------------------------------------ +-- Per-region instances (for explicit-region sceptic reads) + +-- The guarantee at region r0, written without the universal +-- quantifier. Useful to cite when discussing a specific region. +audit-no-recovery-r0 : + ¬ (Σ (AuditReceipt r0 → LiveHandle r0) + (λ recover → ∀ h → recover (exit r0 h) ≡ h)) +audit-no-recovery-r0 = audit-no-recovery r0 + +audit-no-recovery-r1 : + ¬ (Σ (AuditReceipt r1 → LiveHandle r1) + (λ recover → ∀ h → recover (exit r1 h) ≡ h)) +audit-no-recovery-r1 = audit-no-recovery r1 + +------------------------------------------------------------------------ +-- What this walkthrough does NOT prove (the matched negative) + +-- We deliberately do not state, and do not prove, any of: +-- +-- * `bytes-zeroed` (a runtime claim about memory contents); +-- * `secure-against-side-channels` (a claim about timing / +-- speculative-execution leaks); +-- * `audit-is-tamper-evident` (a claim about the receipt being +-- cryptographically authenticated); +-- * `no-recovery-given-an-oracle` (a claim about adversaries with +-- access to *additional* live handles outside the model). +-- +-- These are real properties one might want, but they are not what +-- `audit-no-recovery` gives. The honest scope is: a type-level +-- guarantee inside `--safe --without-K` Agda, for a pure function +-- with only the receipt as input. Citations of this walkthrough +-- elsewhere should preserve that scope; conflating it with any of +-- the four bullets above is the category error this walkthrough +-- exists to head off. diff --git a/tutorial/region_exit_audit/Smoke.agda b/tutorial/region_exit_audit/Smoke.agda new file mode 100644 index 0000000..3bf6755 --- /dev/null +++ b/tutorial/region_exit_audit/Smoke.agda @@ -0,0 +1,33 @@ +{-# OPTIONS --safe --without-K #-} + +------------------------------------------------------------------------ +-- Per-walkthrough Smoke gate for Lane 5 Walkthrough 1. +-- +-- Pins the load-bearing names of `RegionExitAudit.agda` so a silent +-- rename or deletion fails CI fast, mirroring the discipline of the +-- top-level `proofs/agda/Smoke.agda`. +-- +-- Build: +-- agda --library-file=/tmp/agda-libs -i . -i proofs/agda \ +-- tutorial/region_exit_audit/Smoke.agda +-- +-- Exits 0 under --safe --without-K, zero postulates. +------------------------------------------------------------------------ + +module tutorial.region_exit_audit.Smoke where + +open import tutorial.region_exit_audit.RegionExitAudit using + ( RegionId + ; r0 + ; r1 + ; LiveHandle + ; AuditReceipt + ; exit + ; handle-true + ; handle-false + ; handles-genuinely-distinct + ; exit-collapses-handles + ; audit-no-recovery + ; audit-no-recovery-r0 + ; audit-no-recovery-r1 + ) From 4d77d750a5e16cee72e07c2968d0553ff084680c Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 27 May 2026 00:51:43 +0100 Subject: [PATCH 07/10] =?UTF-8?q?feat+docs:=20Lane=203=20lex-pair=20( --- README.md | 40 ++++ .../echo-types/buchholz-rank-obstruction.adoc | 30 +-- docs/echo-types/pillar-e-offline.adoc | 24 +- proofs/agda/All.agda | 1 + proofs/agda/Ordinal/Buchholz/RankLex.agda | 186 +++++++++++++++ proofs/agda/Ordinal/Buchholz/Smoke.agda | 20 ++ tutorial/All.agda | 11 +- tutorial/README.adoc | 18 +- tutorial/epistemic_erasure/All.agda | 10 + .../epistemic_erasure/EpistemicErasure.agda | 215 ++++++++++++++++++ tutorial/epistemic_erasure/README.adoc | 142 ++++++++++++ tutorial/epistemic_erasure/Smoke.agda | 42 ++++ 12 files changed, 710 insertions(+), 29 deletions(-) create mode 100644 proofs/agda/Ordinal/Buchholz/RankLex.agda create mode 100644 tutorial/epistemic_erasure/All.agda create mode 100644 tutorial/epistemic_erasure/EpistemicErasure.agda create mode 100644 tutorial/epistemic_erasure/README.adoc create mode 100644 tutorial/epistemic_erasure/Smoke.agda diff --git a/README.md b/README.md index 9a084b5..8ce1783 100644 --- a/README.md +++ b/README.md @@ -201,6 +201,46 @@ cd /var/mnt/eclipse/repos/echo-types agda -i proofs/agda proofs/agda/All.agda ``` +### Installing as a library + +The repo is structured as an Agda library via `echo-types.agda-lib` +at the repo root. To use `echo-types` from another Agda project, +register the library file once: + +```bash +git clone https://github.com/hyperpolymath/echo-types.git +echo "$(pwd)/echo-types/echo-types.agda-lib" >> ~/.agda/libraries +``` + +Then in any other project, depend on `echo-types` in that +project's own `.agda-lib`: + +```text +name: my-project +depend: standard-library echo-types +include: src +``` + +Consumers can then `open import Echo`, `open import EchoLinear`, +or `open import tutorial.region_exit_audit.RegionExitAudit` — the +library's `include:` line covers both `proofs/agda` and the repo +root (for the Lane 5 tutorial track). + +Requires `standard-library` v2.3 or later registered alongside. + +## Citation + +If you cite this repository in academic work, please cite via the +Zenodo DOI listed in [CITATION.cff](CITATION.cff). The Zenodo +record is the canonical citation target; GitHub's "Cite this +repository" widget resolves directly to it. + +GitHub→Zenodo integration is a one-time author setup; until that +is wired the `CITATION.cff` `doi:` field carries a placeholder +(`10.5281/zenodo.0000000`). See +[docs/echo-types/pillar-e-offline.adoc](docs/echo-types/pillar-e-offline.adoc) +§"Zenodo DOI mint" for the activation sequence. + ## Tooling Stance - default development stays plain Agda with the standard library diff --git a/docs/echo-types/buchholz-rank-obstruction.adoc b/docs/echo-types/buchholz-rank-obstruction.adoc index 28be05f..60f3ad2 100644 --- a/docs/echo-types/buchholz-rank-obstruction.adoc +++ b/docs/echo-types/buchholz-rank-obstruction.adoc @@ -304,29 +304,33 @@ constructors discharge by additive-principal closure. | `<ᵇ-+Ω` | ✓ closed | `rank-pow-bplus-into-ω-rank-pow` (additive-principal at the target) plus the WfCNF tail bound `y ≤ᵇ x` (caller-provided). | `<ᵇ-+ψ` | ✓ closed | Same as `<ᵇ-+Ω` since `rank-pow (bpsi ν _) = ω-rank-pow ν`. | `<ᵇ⁺-ψα` | ✓ closed (Lane 3, 2026-05-26) | `rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α`; `⊕-mono-<-right` closes the shared-Ω-index lex case from `rank-pow α <′ rank-pow β` (which the existing `_<ᵇ⁰_` umbrella discharges). Primitive `rank-mono-<ᵇ⁺-ψα-from-pow` in `Ordinal.Buchholz.RankAdm`. -| `<ᵇ-ψΩ≤` | ⏳ encoding mismatch | `ν <Ω μ` (strict) case closes by `additive-principal-ω-rank-pow {μ}`. `ν = μ` case STILL OPEN: `ω-rank-pow μ ⊕ rank-pow α <′ ω-rank-pow μ` is impossible under any rank shape with `ω-rank-pow ν ≤ rank-adm (bpsi ν α)`. The classical Buchholz gap `[Ω_μ, Ω_{μ+1})` that admissible ψ_μ(α) lives in is not modelled by `ω-rank-pow ν ⊕ rank-pow α`. Two design follow-ups (lex pair, multiplicative ordinal) documented in `RankAdm.agda` §"<ᵇ-ψΩ≤-still-open"; option A (lex pair) recommended. +| `<ᵇ-ψΩ≤` | ✓ closed (Lane 3 follow-on, 2026-05-27) | Lex-pair rank `rank-lex : BT → RankLex` in `Ordinal.Buchholz.RankLex`, with `rank-lex (bOmega ν) = mkLex (ω-rank-pow ν) (ω-rank-pow ν)` and `rank-lex (bpsi ν α) = mkLex (ω-rank-pow ν) (rank-pow α)`. Both sub-cases close via `rank-mono-<ᵇ-ψΩ≤-lex`: ν<μ via `> ~/.agda/libraries `agda --library echo-types -- proofs/agda/All.agda` to prove the packaging works end-to-end. -This is wholly in-repo — I can do all three. The Zenodo bits -require the user's account, so they're tracked as the next step -after packaging lands. +*Pre-staging status (updated 2026-05-27).* Items 1 (`echo-types.agda-lib` +with dual `include: proofs/agda .`) and 2 (README §"Build" > +"Installing as a library" subsection with the registration and +consumer-side `depend:` snippet) are both landed. Item 3 (CI +install-self job) is deferred so it can be wired alongside the +GitHub→Zenodo workflow once the user authorises the integration — +both are downstream of the same author-driven setup, and bundling +them avoids a transient CI red between the two PRs. == Outreach drafts diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 18b401c..6d8fc50 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -108,6 +108,7 @@ open import Ordinal.Buchholz.RankBrouwer open import Ordinal.Buchholz.RankPartial open import Ordinal.Buchholz.RankPow open import Ordinal.Buchholz.RankAdm +open import Ordinal.Buchholz.RankLex open import Ordinal.Buchholz.RankMonoUmbrella open import Ordinal.Buchholz.RecursiveSurfaceOrder open import Ordinal.Buchholz.RecursiveSurfaceBudget diff --git a/proofs/agda/Ordinal/Buchholz/RankLex.agda b/proofs/agda/Ordinal/Buchholz/RankLex.agda new file mode 100644 index 0000000..b24a02c --- /dev/null +++ b/proofs/agda/Ordinal/Buchholz/RankLex.agda @@ -0,0 +1,186 @@ +{-# OPTIONS --safe --without-K #-} + +-- Lex-pair rank for Buchholz terms (Lane 3 follow-on slice, 2026-05-27). +-- +-- ## Where this sits +-- +-- `Ordinal.Buchholz.RankAdm.rank-adm` discharged the `<ᵇ⁺-ψα` +-- (shared-Ω-index lex) constructor by shifting the ψ-rank from +-- `ω-rank-pow ν` (α-blind) to `ω-rank-pow ν ⊕ rank-pow α` +-- (α-discriminating). That fixed `<ᵇ⁺-ψα` cleanly, but it surfaced +-- a new gap: the `<ᵇ-ψΩ≤` constructor at the ν = μ boundary case is +-- *structurally impossible* under any scalar `Ord`-valued rank with +-- `ω-rank-pow ν ≤ rank-adm (bpsi ν α)` — that monotonicity forces +-- the goal `rank-adm (bpsi ν α) <′ ω-rank-pow ν` to imply the absurd +-- `ω-rank-pow ν <′ ω-rank-pow ν` (see `RankAdm.agda` +-- §"<ᵇ-ψΩ≤-still-open" for the full diagnostic). +-- +-- The recommended follow-up there was option (A): a two-component +-- lex rank. This module lands it as a *thin* slice: the lex pair +-- exists alongside `rank-pow` and `rank-adm`, only for the headline +-- `<ᵇ-ψΩ≤` close-out. The existing 10 + 1 = 11 closed cases +-- continue to consume the scalar `rank-pow` / `rank-adm` infrastructure +-- unchanged. +-- +-- ## What this slice closes +-- +-- 1. `RankLex` record with two `Ord` fields (`first`, `second`). +-- 2. `_